DPLL: the core of modern satisfiability solvers

DOI10.1007/978-3-319-41842-1_12MaRDI QIDQ3305326zbMATH OpenOpenAlexFDO

Authors Donald W. Loveland, Ashish Sabharwal, Bart Selman

Publication date 6 August 2020

Published in Outstanding Contributions to Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41842-1_12

zbMATH Keywords

theorem provingSAT solversBoolean satisfiabilityDPLLDavis-Putnam procedure

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• scientific article; zbMATH DE number 1903342
• scientific article; zbMATH DE number 2090309
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Propositional SAT solving
• SAT 2005. Satisfiability Research in the Year 2005.

Cites work

• scientific article; zbMATH DE number 3172714 (Why is no real title available?)
• scientific article; zbMATH DE number 3904557 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• scientific article; zbMATH DE number 3185223 (Why is no real title available?)
• scientific article; zbMATH DE number 3187982 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Proof Method for Quantification Theory: Its Justification and Realization
• A fast parallel SAT-solver -- efficient workload balancing
• A machine program for theorem-proving
• Backdoor sets for DLL subsolvers
• BerkMin: A fast and robust SAT-solver
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• Handbook of knowledge representation.
• ManySAT: a parallel SAT solver
• On the power of clause-learning SAT solvers as resolution engines
• Proving theorems by pattern recognition I
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving propositional satisfiability problems
• Some pitfalls for experimenters with random SAT
• The complexity of theorem-proving procedures

Cited in

(9)

• Scaling up DPLL(T) string solvers using context-dependent simplification
• Learning to select branching rules in the DPLL procedure for satisfiability
• SAT 2005. Satisfiability Research in the Year 2005.
• Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
• Martin Davis: an overview of his work in logic, computer science, and philosophy
• Preface
• Seventy Years of Computer Science
• The CDSAT method for satisfiability modulo theories and assignment: an exposition
• New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability

Describes a project that uses

Uses Software

• CUD@SAT
• RSat
• DIMACS
• BerkMin
• Chaff
• Walksat
• ManySAT

This page was built for publication: DPLL: the core of modern satisfiability solvers

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