DPLL: The Core of Modern Satisfiability Solvers

DOI10.1007/978-3-319-41842-1_12zbMath1439.68026OpenAlexW2583500337MaRDI QIDQ3305326

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 provingBoolean satisfiabilitySAT solversDPLLDavis-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)

Related Items (2)

Seventy Years of Computer Science ⋮ Preface

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• Backdoor sets for DLL subsolvers
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• Solving propositional satisfiability problems
• A fast parallel SAT-solver -- efficient workload balancing
• BerkMin: A fast and robust SAT-solver
• Some pitfalls for experimenters with random SAT
• A Proof Method for Quantification Theory: Its Justification and Realization
• Proving theorems by pattern recognition I
• Solving SAT and SAT Modulo Theories
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures

This page was built for publication: DPLL: The Core of Modern Satisfiability Solvers