Search code examples
algorithmlogicartificial-intelligence

How does the DPLL algorithm work?

I'm having trouble understanding the DPLL algorithm for checking satisfiability of a sentence in propositional logic. http://books.google.co.in/books?id=4fyShrIFXg4C&pg=PA250&lpg=PA250&dq=DPLL+algorithm+from+artificial+intelligence+A+modern+approach&source=bl&ots=oOoZsT8KFd&sig=pdmyUsQZZWw76guWY9eFJKyNsH0&hl=en&sa=X&ei=vBFeUOf1EMLrrQeanoG4DQ&ved=0CD0Q6AEwAw#v=onepage&q&f=false
enter image description here

This algorithm is taken from the book Artificial Intelligence A modern approach. I'm finding it really confusing with those many function recursions. In particular, what does the EXTEND() function do, and what's the purpose behind the recursive calls to DPLL() ?

Solution

  • The DPLL is essentially a backtracking algorithm, and that's the main idea behind the recursive calls.

    The algorithm is building solution while trying assignments, you have a partial solution which might prove successful or not-successful as you go on. The geniusity of the algorithm is how to build the partial solution.

    First, let's define what a unit clause is:

    A unit clause is a clause which has exactly one literal which is still unassigned, and the other (assigned) literals - are all assigned to false.
    The importance of this clause is that if the current assignment is valid - you can determine what is the value of the variable which is in the unassigned literal - because the literal must be true.

    For example: If we have a formula:

    (x1 \/ x2 \/ x3) /\ (~x1 \/ ~x4 \/ x5) /\ ( ~x1 \/ x4)

    And we already assigned:

    x1=true, x4=true

    Then (~x1 \/ ~x4 \/ x5) is a unit clause, because you must assign x5=true in order to satisfy this clause in the current partial assignment.

    The basic idea of the algorithm is:

    1. "Guess" a variable
    2. Find all unit clauses created from the last assignment and assign the needed value
    3. Iteratively retry step 2 until there is no change (found transitive closure)
    4. If the current assignment cannot yield true for all clauses - fold back from recursion and retry a different assignment
    5. If it can - "guess" another variable (recursively invoke and return to 1)

    Termination:

    1. There is nowhere to go "back to" and change a "guess" (no solution)
    2. All clauses are satisfied (there is a solution, and the algorithm found it)

    You can also have a look at these lecture slides for more information and an example.

    Usage example and importance:
    The DPLL, though 50 years old - is still the basis for most SAT solvers.
    SAT Solvers are very useful for solving hard problems, one example in software verification - where you represent your model as a set of formulas, and the condition you want to verify - and invoke the SAT solver over it. Although exponential worst case - the average case is fast enough and is widely used in the industry (mainly for verifying Hardware components)