Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning

DOI10.1007/11591191_40zbMath1143.68582OpenAlexW1583139177MaRDI QIDQ5387867

Allen van Gelder

Publication date: 27 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11591191_40

Mathematics Subject Classification ID

Related Items

On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Towards NP-P via proof complexity and search ⋮ Producing and verifying extremely large propositional refutations ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ An Exponential Lower Bound for Width-Restricted Clause Learning ⋮ Pool resolution is NP-hard to recognize ⋮ On Linear Resolution

Uses Software

• Chaff
• BerkMin

This page was built for publication: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning