Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

DOI10.1007/978-3-642-02777-2_13zbMath1247.68245arXiv1401.3868OpenAlexW2158442970MaRDI QIDQ5902141

Albert Atserias, Marc Thurley, Johannes K. Fichte

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1401.3868

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Machine learning and logic: a new frontier in artificial intelligence ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ Bounded treewidth as a key to tractability of knowledge representation and reasoning

Uses Software

• MiniSat
• Siege
• Chaff
• BerkMin
• RSat

Cites Work

• Unnamed Item
• Satisfiability, branch-width and Tseitin tautologies
• A combinatorial characterization of resolution width
• BerkMin: A fast and robust SAT-solver
• Short proofs are narrow—resolution made simple
• Solving SAT and SAT Modulo Theories
• Hard examples for resolution
• Theory and Applications of Satisfiability Testing

This page was built for publication: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution