Exponential separations in a hierarchy of clause learning proof systems

DOI10.1007/978-3-642-39071-5_5MaRDI QIDQ5326452zbMATH OpenOpenAlexFDO

Authors Jan Johannsen

Publication date 5 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39071-5_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Improved separations of regular resolution from clause learning proof systems
• Exponential separation between Res(k) and Res(k+1) for k n
• An improved separation of regular resolution from pool resolution and clause learning
• An Exponential Lower Bound for Width-Restricted Clause Learning

Cited in

(2)

• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Improved separations of regular resolution from clause learning proof systems

This page was built for publication: Exponential separations in a hierarchy of clause learning proof systems

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