DPLL algorithm

DPLL algorithm

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.

Contents

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 
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, 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 clause 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 diagrams have also been used for SAT solving.

Relation to other notions

Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.[1]

See also

References

General

Specific

  1. ^ Peter Van Beek (2006). "Backtracking search algorithms". In Francesca Rossi, Peter Van Beek, Toby Walsh. Handbook of constraint programming. Elsevier. p. 122. ISBN 9780444527264. http://books.google.com/books?id=Kjap9ZWcKOoC&pg=PA122. 

Further reading

  • Malay Ganai; Aarti Gupta; Dr. Aarti Gupta (2007). SAT-based scalable formal verification solutions. Springer. pp. 23–32. ISBN 9780387691664. 
  • Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart Selman (2008). "Satisfiability Solvers". In Frank Van Harmelen, Vladimir Lifschitz, Bruce Porter. Handbook of knowledge representation. Foundations of Artificial Intelligence. 3. Elsevier. pp. 89–134. doi:10.1016/S1574-6526(07)03002-7. ISBN 9780444522115. 

Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • DPLL — stands for: DPLL algorithm, for solving the boolean satisfiability problem Digital phase locked loop, an electronic feedback system that generates a signal This disambiguation page lists articles associated with the same title. If an internal li …   Wikipedia

  • DPLL — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. DPLL est un sigle pouvant désigner : en informatique théorique, l algorithme de Davis Putnam Logemann Loveland (en) est utilisé pour résoudre… …   Wikipédia en Français

  • 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… …   Wikipedia

  • Chaff algorithm — Chaff is an algorithm for solving instances of the Boolean satisfiability problem in programming. It was designed by researchers at Princeton University, USA. The algorithm is an instance of the DPLL algorithm with a number of enhancements for… …   Wikipedia

  • Boolean satisfiability problem — For the concept in mathematical logic, see Satisfiability. 3SAT redirects here. For the Central European television network, see 3sat. In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of… …   Wikipedia

  • Martin Davis — This page is on the mathematician. For the former tennis player see Martin Davis (tennis). Martin Davis Photo courtesy George M. Bergman Born …   Wikipedia

  • List of mathematics articles (D) — NOTOC D D distribution D module D D Agostino s K squared test D Alembert Euler condition D Alembert operator D Alembert s formula D Alembert s paradox D Alembert s principle Dagger category Dagger compact category Dagger symmetric monoidal… …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • Hilary Putnam — Infobox Philosopher region = Western Philosophy era = 20th century philosophy color = #B0C4DE name = Hilary Whitehall Putnam birth = July 31, 1926 flagicon|USA|size=20px Chicago, Illinois school tradition = Analytic main interests = Philosophy of …   Wikipedia

  • Decision problem — A decision problem has only two possible outputs, yes or no (or alternately 1 or 0) on any input. In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes or no answer,… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”