Between SAT and UNSAT: The Fundamental Difference in CDCL SAT

DOI10.1007/978-3-319-24318-4_23zbMath1471.68260OpenAlexW2286662631MaRDI QIDQ3453235

Chanseok Oh

Publication date: 20 November 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_23

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

SAT race 2015, SAT competition 2020, Supercharging plant configurations using Z3, Deep cooperation of CDCL and local search for SAT, Assessing progress in SAT solvers through the Lens of incremental SAT, The \textsc{MergeSat} solver, A model of random industrial SAT

Uses Software

• MiniSat
• Chaff
• Plingeling
• Glucose
• Treengeling
• COMiniSatPS
• satUZK
• Lingeling

Cites Work

• On the power of clause-learning SAT solvers as resolution engines
• Optimal speedup of Las Vegas algorithms
• The intractability of resolution
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• On Freezing and Reactivating Learnt Clauses
• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• Local Restarts
• GRASP: a search algorithm for propositional satisfiability
• Theory and Applications of Satisfiability Testing
• Unnamed Item
• Unnamed Item