In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
and
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a
complete,
backtracking
Backtracking is a class of algorithms for finding solutions to some computational problems, notably constraint satisfaction problems, that incrementally builds candidates to the solutions, and abandons a candidate ("backtracks") as soon as it de ...
-based
search algorithm
In computer science, a search algorithm is an algorithm designed to solve a search problem. Search algorithms work to retrieve information stored within particular data structure, or calculated in the Feasible region, search space of a problem do ...
for
deciding the satisfiability of
propositional logic formulae in
conjunctive normal form
In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.
In au ...
, i.e. for solving the
CNF-SAT problem.
It was introduced in 1961 by
Martin Davis,
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
Hilary Putnam
Hilary Whitehall Putnam (; July 31, 1926 – March 13, 2016) was an American philosopher, mathematician, computer scientist, and figure in analytic philosophy in the second half of the 20th century. He contributed to the studies of philosophy of ...
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.
Implementations and applications
The
SAT problem is important both from theoretical and practical points of view. In
complexity theory it was the first problem proved to be
NP-complete
In computational complexity theory, NP-complete problems are the hardest of the problems to which ''solutions'' can be verified ''quickly''.
Somewhat more precisely, a problem is NP-complete when:
# It is a decision problem, meaning that for any ...
, and can appear in a broad variety of applications such as ''
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software syst ...
'',
automated planning and scheduling
Automated planning and scheduling, sometimes denoted as simply AI planning, is a branch of artificial intelligence that concerns the realization of strategies or action sequences, typically for execution by intelligent agents, autonomous robots ...
, and
diagnosis in artificial intelligence.
As such, writing efficient
SAT solver
In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem (SAT). On input a formula over Boolean data type, Boolean variables, such as "(''x'' or ''y'') and (''x'' or not ''y'' ...
s has been a research topic for many years.
GRASP
A grasp is an act of taking, holding or seizing firmly with (or as if with) the hand. An example of a grasp is the handshake, wherein two people grasp one of each other's like hands.
In zoology
Zoology ( , ) is the scientific study of an ...
(1996-1999) was an early implementation using DPLL.
[ In the international SAT competitions, implementations based around DPLL such as zChaff and MiniSat were in the first places of the competitions in 2004 and 2005.][
]
Another application that often involves DPLL is automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
or satisfiability modulo theories
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involv ...
(SMT), which is a SAT problem in which propositional variable
In mathematical logic, a propositional variable (also called a sentence letter, sentential variable, or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building ...
s are replaced with formulas of another mathematical theory
A theory is a systematic and rational form of abstract thinking about a phenomenon, or the conclusions derived from such thinking. It involves contemplative and logical reasoning, often supported by processes such as observation, experimentation, ...
.
The algorithm
The basic backtracking algorithm runs by choosing a literal, assigning a truth value
In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values ('' true'' or '' false''). Truth values are used in ...
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 that 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 (UP) or boolean constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.
Definition
The procedure is based on unit clause ...
: 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. Unit propagation consists in removing every clause containing a unit clause's literal and in discarding the complement of a unit clause's literal from every clause containing that complement. 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
In mathematical logic, a propositional variable (also called a sentence letter, sentential variable, or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building ...
occurs with only one polarity in the formula, it is called ''pure''. A pure literal can always be assigned in a way that makes all clauses containing it true. Thus, when it is assigned in such a way, 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:
Input: A set of clauses Φ.
Output: A truth value indicating whether Φ is satisfiable.
function ''DPLL''(Φ)
// unit propagation:
while there is a unit clause in Φ do
Φ ← ''unit-propagate''(''l'', Φ);
// pure literal elimination:
while there is a literal ''l'' that occurs pure in Φ do
Φ ← ''pure-literal-assign''(''l'', Φ);
// stopping conditions:
if Φ is empty then
return true;
if Φ contains an empty clause then
return false;
// DPLL procedure:
''l'' ← ''choose-literal''(Φ);
return ''DPLL''(Φ ∧ ) or ''DPLL''(Φ ∧ );
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 or
in the return
statement is a short-circuiting operator. Φ ∧
denotes the simplified result of substituting "true" for l
in Φ
.
The algorithm terminates in one of two cases. Either the CNF formula Φ
is empty, i.e., it contains no clause. Then it is satisfied by any assignment, as all its clauses are vacuously true. Otherwise, when the formula contains an empty clause, the clause is vacuously false because a disjunction requires at least one member that is true for the overall set to be true. In this case, the existence of such a clause implies that the formula (evaluated as a ''conjunction'' of all clauses) cannot evaluate to true and must be unsatisfiable.
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 by keeping track of branching literals and of the literal assignments made during unit propagation and pure literal elimination.
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. Such choice functions are also called heuristic function
A heuristic or heuristic technique (''problem solving'', '' mental shortcut'', ''rule of thumb'') is any approach to problem solving that employs a pragmatic method that is not fully optimized, perfected, or rationalized, but is nevertheless ...
s or branching heuristics.
Formalization
The sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautolog ...
-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail to find a satisfying assignment, i.e. .
If a clause in the formula has exactly one unassigned literal in , with all other literals in the clause appearing negatively, extend with . ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''If a literal appears in the formula but its negation does not, and and are not in , extend with . ''This rule represents the idea that if a variable appears only purely positively or purely negatively in a formula, all the instances can be set to true or false to make their corresponding clauses true.''If a literal is in the set of literals of and neither nor is in , then decide on the truth value of and extend with the decision literal . ''This rule represents the idea that if you aren't forced to do an assignment, you must choose a variable to assign and make note which assignment was a choice so you can go back if the choice didn't result in a satisfying assignment.''If a clause is in , and their negations are in , and can be represented as where , then backtrack by setting to . ''This rule represents the idea that if you reach a contradiction in trying to find a valid assignment, you need to go back to where you previously did a decision between two assignments and pick the other one.''If a clause is in , and their negations are in , and there is no conflict marker in , then the DPLL algorithm fails. ''This rule represents the idea that if you reach a contradiction but there wasn't anything you could have done differently on the way there, the formula is unsatisfiable.''
Visualization
Davis, Logemann, Loveland (1961) had developed this algorithm.
Some properties of this original algorithm are:
* It is based on search.
* It is the basis for almost all modern SAT solvers.
* It ''does not'' use learning or non-chronological backtracking (introduced in 1996).
An example with visualization of a DPLL algorithm having chronological backtracking:
Image:Dpll1.png, All clauses making a CNF formula
Image:Dpll2.png, Pick a variable
Image:Dpll3.png, Make a decision, variable a = False (0), thus green clauses becomes True
Image:Dpll4.png, After making several decisions, we find an implication graph
In mathematical logic and graph theory, an implication graph is a skew-symmetric, directed graph composed of vertex set and directed edge set . Each vertex in represents the truth status of a Boolean literal, and each directed edge from ve ...
that leads to a conflict.
Image:Dpll5.png, Now backtrack to immediate level and by force assign opposite value to that variable
Image:Dpll6.png, But a forced decision still leads to another conflict
Image:Dpll7.png, Backtrack to previous level and make a forced decision
Image:Dpll8.png, Make a new decision, but it leads to a conflict
Image:Dpll9.png, Make a forced decision, but again it leads to a conflict
Image:Dpll10.png, Backtrack to previous level
Image:Dpll11.png, Continue in this way and the final implication graph
Related algorithms
Since 1986, (Reduced ordered) binary decision diagrams have also been used for SAT solving.
In 1989-1990, Stålmarck's method for formula verification was presented and patented. It has found some use in industrial applications.
DPLL has been extended for automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
for fragments of first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
by way of the DPLL(T) algorithm.[
]
In the 2010-2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on ''unit propagation''. However, the main improvement has been a more powerful algorithm, Conflict-Driven Clause Learning
In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to ...
(CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform ''non-chronological backtracking'' (aka ''backjumping
In constraint programming and SAT solving, backjumping (also known as non-chronological backtracking or intelligent backtracking) is an enhancement for backtracking algorithms which reduces the search space. While backtracking always goes up one ...
'') in order to avoid reaching the same conflict again. Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.
Relation to other notions
Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.
See also
*Proof complexity In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. ...
* Herbrandization
References
General
*
*
*
*
Specific
Further reading
*
* {{cite book, editor1-first=Frank, editor1-last=Van Harmelen, editor2-first=Vladimir, editor2-last=Lifschitz, editor3-first=Bruce, editor3-last=Porter, title=Handbook of knowledge representation, year=2008, publisher=Elsevier, isbn=978-0-444-52211-5, pages=89–134, first1=Carla P., last1=Gomes, first2=Henry, last2=Kautz, first3= Ashish, last3=Sabharwal, first4=Bart, last4=Selman, chapter=Satisfiability Solvers, doi=10.1016/S1574-6526(07)03002-7, series=Foundations of Artificial Intelligence, volume=3
Constraint programming
Automated theorem proving
SAT solvers
Articles with example pseudocode