Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
From MaRDI portal
Publication:3623009
DOI10.2168/LMCS-4(4:13)2008zbMath1159.03009OpenAlexW3100513773WikidataQ124817153 ScholiaQ124817153MaRDI QIDQ3623009
Jan Johannsen, Jan Hoffmann, Samuel R. Buss
Publication date: 29 April 2009
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2168/lmcs-4(4:13)2008
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Space Complexity in Polynomial Calculus ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ A resolution proof system for dependency stochastic Boolean satisfiability ⋮ Extended clause learning ⋮ Towards NP-P via proof complexity and search ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ Satisfiability via Smooth Pictures ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ An Exponential Lower Bound for Width-Restricted Clause Learning ⋮ Pool resolution is NP-hard to recognize ⋮ On Linear Resolution ⋮ Davis and Putnam meet Henkin: solving DQBF with resolution
Uses Software
This page was built for publication: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
