Improved separations of regular resolution from clause learning proof systems

DOI10.1613/JAIR.4260MaRDI QIDQ5415765zbMATH OpenOpenAlexFDO

Authors Maria Luisa Bonet, Jan Johannsen, Samuel R. Buss

Publication date 16 May 2014

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Abstract: We prove that the graph tautology formulas of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses and without degenerate resolution inferences. We also prove that these graph tautology formulas can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search. We prove similar results for the guarded, xor-fied pebbling tautologies which Urquhart proved are hard for regular resolution.

Recommendations

• An improved separation of regular resolution from pool resolution and clause learning
• On the power of clause-learning SAT solvers as resolution engines
• Exponential separations in a hierarchy of clause learning proof systems
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Regular and General Resolution: An Improved Separation

Cited in

(13)

• Pool resolution is NP-hard to recognize
• Trade-offs between time and memory in a tighter model of CDCL SAT solvers
• An improved separation of regular resolution from pool resolution and clause learning
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• On linear resolution
• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• New stochastic local search approaches for computing preferred extensions of abstract argumentation
• Exponential separations in a hierarchy of clause learning proof systems
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Small Stone in pool
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• A simple supercritical tradeoff between size and height in resolution
• Understanding the relative strength of QBF CDCL solvers and QBF resolution

This page was built for publication: Improved separations of regular resolution from clause learning proof systems

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