Relativization makes contradictions harder for resolution

DOI10.1016/J.APAL.2013.10.009MaRDI QIDQ386151zbMATH OpenOpenAlexFDO

Authors Barnaby Martin, Stephan Stoyanov Danchev

Publication date 16 December 2013

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

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)

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

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

Cites work

• scientific article; zbMATH DE number 1948187 (Why is no real title available?)
• scientific article; zbMATH DE number 1507224 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 819814 (Why is no real title available?)
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• A characterization of tree-like resolution size
• A complexity gap for tree resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• Combinatorics of first order structures and propositional proof systems
• Computer Science Logic
• Generating hard tautologies using predicate logic and the symmetric group
• Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
• Parameterized bounded-depth Frege is not optimal
• Parameterized complexity of DPLL search procedures
• Parameterized proof complexity
• Parameterized resolution with bounded conjunction
• Parametrized complexity theory.
• Proofs as Games
• Relativisation Provides Natural Separations for Resolution-Based Proof Systems
• The intractability of resolution
• The relative efficiency of propositional proof systems

Cited in

(7)

• 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
• The treewidth of proofs
• Tight size-degree bounds for sums-of-squares proofs
• Narrow proofs may be maximally long
• Relativisation Provides Natural Separations for Resolution-Based 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)