On the power of clause-learning SAT solvers as resolution engines
From MaRDI portal
Publication:543613
DOI10.1016/j.artint.2010.10.002zbMath1216.68235OpenAlexW2121015471MaRDI QIDQ543613
Knot Pipatsrisawat, Adnan Darwiche
Publication date: 17 June 2011
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.artint.2010.10.002
Related Items
Knowledge Compilation with Empowerment ⋮ Proof complexity of modal resolution ⋮ Between SAT and UNSAT: The Fundamental Difference in CDCL SAT ⋮ A note about \(k\)-DNF resolution ⋮ Generalising and Unifying SLUR and Unit-Refutation Completeness ⋮ A simple proof of QBF hardness ⋮ Learning a propagation complete formula ⋮ Strong ETH and resolution via games and the multiplicity of strategies ⋮ Oblivious bounds on the probability of boolean functions ⋮ Space Complexity in Polynomial Calculus ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Symmetry in Gardens of Eden ⋮ Machine learning and logic: a new frontier in artificial intelligence ⋮ The impact of heterogeneity and geometry on the proof complexity of random satisfiability ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Are hitting formulas hard for resolution? ⋮ What is answer set programming to propositional satisfiability ⋮ The complexity of proving that a graph is Ramsey ⋮ Algorithms for computing minimal equivalent subformulas ⋮ New stochastic local search approaches for computing preferred extensions of abstract argumentation ⋮ Bounds on the size of PC and URC formulas ⋮ An overview of parallel SAT solving ⋮ DPLL: The Core of Modern Satisfiability Solvers ⋮ On the empirical time complexity of finding optimal solutions vs proving optimality for Euclidean TSP instances ⋮ Propositional proof systems based on maximum satisfiability ⋮ Conflict-driven answer set solving: from theory to practice ⋮ Lower bounds for QCDCL via formula gauge ⋮ Satisfiability via Smooth Pictures ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Incremental Determinization ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Short Proofs Are Hard to Find ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ On Linear Resolution ⋮ Implementing Efficient All Solutions SAT Solvers ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ On dedicated CDCL strategies for PB solvers
Uses Software
Cites Work
- Unnamed Item
- Optimal speedup of Las Vegas algorithms
- BerkMin: A fast and robust SAT-solver
- A Generalized Framework for Conflict Analysis
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- The relative efficiency of propositional proof systems
- Short proofs are narrow—resolution made simple
- Theory and Applications of Satisfiability Testing
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- A Machine-Oriented Logic Based on the Resolution Principle
- A machine program for theorem-proving
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
