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.03009WikidataQ124817153 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
resolution; satisfiability; SAT solving; propositional proof complexity; weakening; proof search algorithms
03B35: Mechanization of proofs and logical operations
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
03F20: Complexity of proofs
Related Items
On Linear Resolution, On CDCL-Based Proof Systems with the Ordered Decision Strategy, A resolution proof system for dependency stochastic Boolean satisfiability, Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Towards NP-P via proof complexity and search, On the power of clause-learning SAT solvers as resolution engines, Extended clause learning, Finding a tree structure in a resolution proof is NP-complete, Pool resolution is NP-hard to recognize, Davis and Putnam meet Henkin: solving DQBF with resolution, Satisfiability via Smooth Pictures, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, Space Complexity in Polynomial Calculus, An Exponential Lower Bound for Width-Restricted Clause Learning
Uses Software