A machine program for theorem-proving

By Martin D. Davis, G. Logemann, D. Loveland. CACM, 2011

3,650 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/feca806dc20be4a72a57b45b9ce7ebfcded08038

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Instance-Specific Algorithm Configuration (2014, background): “• problem size features: number of clauses c, number of variables v, and their ratio c=v, • variable-clause graph features: degree statistics for variable and clause nodes, • variable graph features: node degree statistics, • balance features: ratio of positive to negative literals per clause, ratio”
Computational Intelligence and Feature Selection - Rough and Fuzzy Approaches (2008, methodology): “In recent years search algorithms based on the well-known Davis–Logemann–Loveland algorithm (DPLL) [71] are emerging as some of the most efficient methods for complete SAT solvers.”
Answer Set Solving in Practice (2012, neutral): “[16] M.”
The Quest for Efficient Boolean Satisfiability Solvers (2002, methodology): “In recent years search-based algorithms based on the well-known Davis- Logemann-Loveland algorithm [6] (sometimes called the DPLL algorithm for historical reasons) are emerging as some of the most efficient methods for complete SAT solvers.”
Performing Bayesian Inference by Weighted Model Counting (2005, methodology): “Although these solvers are all based on the original DPLL backtracking SAT procedure (Davis et al. 1962), they incorporate a number of techniques — in particular, non-chronological backtracking (Dechter 1990), clause learning (Bayardo Jr. and Schrag 1997; Marques-Silva and Sakallah 1996) and…”
Resolve and Expand (2004, methodology): “DPLL also forms the basis of most state-of-the-art SAT solvers, and therefore it was most natural to use it for QBF as well.”
Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications (2003, methodology): “However, this algorithm is hard to use in practice due to prohibitive space requirements, and over the years has given way to search algorithms based on the Davis-LogemannLoveland (DLL) algorithm [9].”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, methodology): “A group of systems which we call automated theorem provers attempt to use automated procedures to determine the validity of conjectures (e.g., the DPLL algorithm [Davis et al., 1962] for SAT problems [Tarski, 1969]).”
Complexity Theoretic Limitations on Learning DNF's (2014, background): “Haken (1985); Beame and Pitassi (1996); Beame et al.”
Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure (2006, background): “All of them are enhanced variants of the classical backtrack search DPLL procedure [8].”
Splitting on Demand in SAT Modulo Theories (2006, methodology): “The performance of propositional SAT solvers based on the Davis-Putnam-Logemann-Loveland (DPLL) procedure [8, 7 ] has importantly improved during the last years, and DPLL-based solvers are becoming the tool of choice for attacking more and more practical problems.”
Learning to Solve QBF (2007, methodology): “Search-based QBF solvers are based on a modification of the Davis-Putnam-Longman algorithm (DPLL, ( Davis, Logemann, & Loveland 1962 )).”
Effective Preprocessing in SAT Through Variable and Clause Elimination (2005, methodology): “Modern SAT solvers use unit propagation and the pure literal rule in a preprocessing phase, as already described in the original DPLL algorithm [6].”
Hypertableau Reasoning for Description Logics (2009, methodology): “A hypertableau inference thus combines hyperresolution with splitting from the DPLL calculus for the propositional logic [9] and it can be written as”
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints (2007, background): “Other important optimizations are a subroutine that immediately includes the clauses in any single-element MCSes (similar to unit-clause propagation in Boolean satisfiability solvers [12, 13]) when they appear as a result of modifications made by PropagateChoice; explicitly removing a clause from th”
Robust Boolean reasoning for equivalence checking and functional property verification (2002, methodology): “Many of the published approaches are based on the Davis-Putnam procedure [5], [6], which executes a systematic case split to exhaustively search the solution space.”