Relativization makes contradictions harder for resolution

DOI10.1016/J.APAL.2013.10.009zbMATH Open1277.68093arXiv1304.4287OpenAlexW2089789793MaRDI QIDQ386151FDOQ386151

Stephan Stoyanov Danchev, Barnaby Martin

Publication date: 16 December 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d), as well as their tree-like versions, Res*(d). The contradictions we use are natural combinatorial principles: the Least number principle, LNP_n and an ordered variant thereof, the Induction principle, IP_n. LNP_n is known to be easy for Resolution. We prove that its relativisation is hard for Resolution, and more generally, the relativisation of LNP_n iterated d times provides a separation between Res(d) and Res(d+1). We prove the same result for the iterated relativisation of IP_n, where the tree-like variant Res*(d) is considered instead of Res(d). We go on to provide separations between the parameterized versions of Res(1) and Res(2). Here we are able again to use the relativisation of the LNP_n, but the classical proof breaks down and we are forced to use an alternative. Finally, we separate the parameterized versions of Res*(1) and Res*(2). Here, the relativisation of IP_n will not work as it is, and so we make a vectorising amendment to it in order to address this shortcoming

Full work available at URL: https://arxiv.org/abs/1304.4287

zbMATH Keywords

lower boundsproof complexityparameterized proof complexityresolution-with-bounded-conjunction

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40) Complexity of proofs (03F20)

Cites Work

• Title not available (Why is that?)
• Parametrized complexity theory.
• Combinatorics of first order structures and propositional proof systems
• Title not available (Why is that?)
• The relative efficiency of propositional proof systems
• Title not available (Why is that?)
• The intractability of resolution
• A complexity gap for tree resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• A characterization of tree-like resolution size
• Proofs as Games
• Parameterized Bounded-Depth Frege Is not Optimal
• Relativisation Provides Natural Separations for Resolution-Based Proof Systems
• Title not available (Why is that?)
• Parameterized proof complexity
• Generating hard tautologies using predicate logic and the symmetric group
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• Parameterized Resolution with Bounded Conjunction
• Computer Science Logic
• LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE
• Parameterized Complexity of DPLL Search Procedures

Cited In (3)

• The treewidth of proofs
• Narrow Proofs May Be Maximally Long
• Tight size-degree bounds for sums-of-squares proofs

   Recommendations

• Relativisation Provides Natural Separations for Resolution-Based Proof Systems 👍 👎
• Parameterized resolution with bounded conjunction 👍 👎
• The limits of tractability in resolution-based propositional proof systems 👍 👎
• The limits of tractability in resolution-based propositional proof systems 👍 👎
• On the relative complexity of resolution refinements and cutting planes proof systems 👍 👎

This page was built for publication: Relativization makes contradictions harder for resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q386151)