Assessing progress in SAT solvers through the Lens of incremental SAT

DOI10.1007/978-3-030-80223-3_20OpenAlexW3186784740MaRDI QIDQ2118309

Alexey Ignatiev, Stepan Kochemazov, João P. Marques-Silva

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_20

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Uses Software

• MiniSat
• Siege
• Chaff
• Glucose
• COMiniSatPS
• PySAT
• MapleCOMSPS
• MapleCOMSPS_LRB
• RC2

Cites Work

• Unnamed Item
• Optimal speedup of Las Vegas algorithms
• Chronological backtracking
• PySAT: a Python toolkit for prototyping with SAT oracles
• Conflict-driven answer set solving: from theory to practice
• Speeding up assumption-based SAT
• Backing backtracking
• Propagation via lazy clause generation
• Clause vivification by unit propagation in CDCL SAT solvers
• Iterative and core-guided maxsat solving: a survey and assessment
• Learning Rate Based Branching Heuristic for SAT Solvers
• Inprocessing Rules
• On Improving MUS Extraction Algorithms
• Empirical Study of the Anatomy of Modern Sat Solvers
• Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
• GRASP: a search algorithm for propositional satisfiability
• RC2: an Efficient MaxSAT Solver
• Theory and Applications of Satisfiability Testing
• Factoring Out Assumptions to Speed Up MUS Extraction
• Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures

This page was built for publication: Assessing progress in SAT solvers through the Lens of incremental SAT