An improved separation of regular resolution from pool resolution and clause learning
From MaRDI portal
Abstract: We prove that the graph tautology principles 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 principles can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search.
Recommendations
- Improved separations of regular resolution from clause learning proof systems
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Regular and General Resolution: An Improved Separation
- Small Stone in pool
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Cited in
(9)- Pool resolution is NP-hard to recognize
- Towards NP-P via proof complexity and search
- A note on SAT algorithms and proof complexity
- On linear resolution
- Exponential separations in a hierarchy of clause learning proof systems
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Improved separations of regular resolution from clause learning proof systems
- Small Stone in pool
- Producing and verifying extremely large propositional refutations
This page was built for publication: An improved separation of regular resolution from pool resolution and clause learning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843321)
