DPLL algorithm
Encyclopedia
The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking
-based algorithm
for deciding the satisfiability
of propositional logic formulae in conjunctive normal form
, i.e. for solving the CNF-SAT
problem.
It was introduced in 1962 by Martin Davis
, Hilary Putnam
, George Logemann and Donald W. Loveland
and is a refinement of the earlier Davis–Putnam algorithm
, which is a resolution
-based procedure developed by Davis and Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the “Davis–Putnam method” or the “DP algorithm”. Other common names that maintain the distinction are DLL and DPLL.
DPLL is a highly efficient procedure and after almost 50 years still forms the basis for most efficient complete SAT solvers, as well as for many theorem provers
for fragments of first-order logic
.
The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step:
Unit propagation
: If a clause is a unit clause, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.
Pure literal elimination : If a propositional variable
occurs with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses do not constrain the search anymore and can be deleted.
Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.
The DPLL algorithm can be summarized in the following pseudocode, where Φ is the CNF formula:
function DPLL(Φ)
if Φ is a consistent set of literals
then return true;
if Φ contains an empty clause
then return false;
for every unit clause l in Φ
Φ=unit-propagate(l, Φ);
for every literal l that occurs pure in Φ
Φ=pure-literal-assign(l, Φ);
l := choose-literal(Φ);
return DPLL(ΦΛl) OR DPLL(ΦΛnot(l));
In this pseudocode,
The Davis–Logemann–Loveland algorithm depends on the choice of branching literal, which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals.
learning. These refinements describe a method of backtracking after reaching a conflict clause which "learns" the root causes (assignments to variables) of the conflict in order to avoid reaching the same conflict again.
A newer algorithm from 1990 is Stålmarck's method. Also since 1986 (reduced ordered) binary decision diagram
s have also been used for SAT solving.
refutation proofs.
Backtracking
Backtracking is a general algorithm for finding all solutions to some computational problem, that incrementally builds candidates to the solutions, and abandons each partial candidate c as soon as it determines that c cannot possibly be completed to a valid solution.The classic textbook example...
-based algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
for deciding the satisfiability
Boolean satisfiability problem
In computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
of propositional logic formulae in conjunctive normal form
Conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
, i.e. for solving the CNF-SAT
Boolean satisfiability problem
In computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
problem.
It was introduced in 1962 by Martin Davis
Martin Davis
Martin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
, Hilary Putnam
Hilary Putnam
Hilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
, George Logemann and Donald W. Loveland
Donald W. Loveland
Donald W. Loveland was a professor emeritus of computer science at Duke University who specialized in artificial intelligence....
and is a refinement of the earlier Davis–Putnam algorithm
Davis–Putnam algorithm
The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there...
, which is a resolution
Resolution (logic)
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
-based procedure developed by Davis and Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the “Davis–Putnam method” or the “DP algorithm”. Other common names that maintain the distinction are DLL and DPLL.
DPLL is a highly efficient procedure and after almost 50 years still forms the basis for most efficient complete SAT solvers, as well as for many theorem provers
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
for fragments of first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
.
The algorithm
The basic backtracking algorithm runs by choosing a literal, assigning a truth value to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the splitting rule, as it splits the problem into two simpler sub-problems. The simplification step essentially removes all clauses which become true under the assignment from the formula, and all literals that become false from the remaining clauses.The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step:
Unit propagation
Unit propagation
Unit propagation or the one-literal rule is a procedure of automated theorem proving that can simplify a set of clauses.-Definition:...
: If a clause is a unit clause, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.
Pure literal elimination : If a propositional variable
Propositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
occurs with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses do not constrain the search anymore and can be deleted.
Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.
The DPLL algorithm can be summarized in the following pseudocode, where Φ is the CNF formula:
function DPLL(Φ)
if Φ is a consistent set of literals
then return true;
if Φ contains an empty clause
then return false;
for every unit clause l in Φ
Φ=unit-propagate(l, Φ);
for every literal l that occurs pure in Φ
Φ=pure-literal-assign(l, Φ);
l := choose-literal(Φ);
return DPLL(ΦΛl) OR DPLL(ΦΛnot(l));
In this pseudocode,
unit-propagate(l, Φ) and pure-literal-assign(l, Φ) are functions that return the result of applying unit propagation and the pure literal rule, respectively, to the literal l and the formula Φ. In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula. The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not. In a real implementation, the partial satisfying assignment typically is also returned on success; this can be derived from the consistent set of literals of the first if statement of the function.The Davis–Logemann–Loveland algorithm depends on the choice of branching literal, which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals.
Current work
Current work on improving the algorithm has been done on three directions: defining different policies for choosing the branching literals; defining new data structures to make the algorithm faster, especially the part on unit propagation; and defining variants of the basic backtracking algorithm. The latter direction include non-chronological backtracking and clauseClause (logic)
In logic, a clause is a finite disjunction ofliterals. Clausesare usually written as follows, where the symbols l_i areliterals:l_1 \vee \cdots \vee l_nIn some cases, clauses are written as sets of literals, so that clause above...
learning. These refinements describe a method of backtracking after reaching a conflict clause which "learns" the root causes (assignments to variables) of the conflict in order to avoid reaching the same conflict again.
A newer algorithm from 1990 is Stålmarck's method. Also since 1986 (reduced ordered) binary decision diagram
Binary decision diagram
In the field of computer science, a binary decision diagram or branching program, like a negation normal form or a propositional directed acyclic graph , is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed...
s have also been used for SAT solving.
Relation to other notions
Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolutionResolution (logic)
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
refutation proofs.
See also
- Davis–Putnam algorithmDavis–Putnam algorithmThe Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there...
- Chaff algorithmChaff algorithmChaff is an algorithm for solving instances of the Boolean satisfiability problem in programming. It was designed by researchers at Princeton University, USA...
- Proof complexityProof complexityIn computer science, proof complexity is a measure of efficiency of automated theorem proving methods that is based on the size of the proofs they produce. The methods for proving contradiction in propositional logic are the most analyzed...
- HerbrandizationHerbrandizationThe Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem...