Assessing progress in SAT solvers through the Lens of incremental SAT

DOI10.1007/978-3-030-80223-3_20MaRDI QIDQ2118309zbMATH OpenOpenAlexFDO

Authors Stepan Kochemazov, A. A. Ignatiev, Joao 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) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Backing backtracking
• Between SAT and UNSAT: the fundamental difference in CDCL SAT
• Chronological backtracking
• Clause vivification by unit propagation in CDCL SAT solvers
• Conflict-driven answer set solving: from theory to practice
• Empirical study of the anatomy of modern SAT solvers
• Factoring Out Assumptions to Speed Up MUS Extraction
• GRASP: a search algorithm for propositional satisfiability
• Handbook of satisfiability. In 2 parts
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Inprocessing rules
• Iterative and core-guided maxsat solving: a survey and assessment
• Learning rate based branching heuristic for SAT solvers
• On improving MUS extraction algorithms
• Optimal speedup of Las Vegas algorithms
• Propagation via lazy clause generation
• PySAT: a Python toolkit for prototyping with SAT oracles
• RC2: an efficient MaxSAT solver
• Speeding up assumption-based SAT
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing

Cited in

(3)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• scientific article; zbMATH DE number 5139172 (Why is no real title available?)
• A MaxSAT approach for solving a new dynamic discretization discovery model for train rescheduling problems

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2118309)