DPLL algorithm definition

I am having some problems understanding the DPLL algorithm and I was wondering if anyone could explain it to me because I think my understanding is incorrect.

The way I understand it is, I take some set of literals and if some every clause is true the model is true but if some clause is false then the model is false.

I recursively check the model by looking for 开发者_如何学Goa unit clause, if there is one I set the value for that unit clause to make it true, then update the model. Removing all clauses that are now true and remove all literals which are now false.

When there are no unit clauses left, I chose any other literal and assign values for that literal which make it true and make it false, then again remove all clauses which are now true and all literals which are now false.

DPLL requires a problem to be stated in disjunctive normal form, that is, as a set of clauses, each of which must be satisfied.

Each clause is a set of literals {l1, l2, ..., ln}, representing the disjunction of those literals (i.e., at least one literal must be true for the clause to be satisfied).

Each literal l asserts that some variable is true (x) or that it is false (~x).

If any literal is true in a clause, then the clause is satisfied.

If all literals in a clause are false, then the clause is unsatisfiable and hence the problem is unsatisfiable.

A solution is an assignment of true/false values to the variables such that every clause is satisfied. The DPLL algorithm is an optimised search for such a solution.

DPLL is essentially a depth first search that alternates between three tactics. At any stage in the search there is a partial assignment (i.e., an assignment of values to some subset of the variables) and a set of undecided clauses (i.e., those clauses that have not yet been satisfied).

(1) The first tactic is Pure Literal Elimination: if an unassigned variable x only appears in its positive form in the set of undecided clauses (i.e., the literal ~x doesn't appear anywhere) then we can just add x = true to our assignment and satisfy all the clauses containing the literal x (similarly if x only appears in its negative form, ~x, we can just add x = false to our assignment).

(2) The second tactic is Unit Propagation: if all but one of the literals in an undecided clause are false, then the remaining one must be true. If the remaining literal is x, we add x = true to our assignment; if the remaining literal is ~x, we add x = false to our assignment. This assignment can lead to further opportunities for unit propagation.

(3) The third tactic is to simply choose an unassigned variable x and branch the search: one side trying x = true, the other trying x = false.

If at any point we end up with an unsatisfiable clause then we have reached a dead end and have to backtrack.

There are all sorts of clever further optimisations, but this is the core of almost all SAT solvers.

Hope this helps.

The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form also known as satisfiability problem or SAT.

Any boolean formula can be expressed in conjunctive normal form (CNF) which means a conjunction of clauses i.e. ( … ) ^ ( … ) ^ ( … )

where a clause is a disjunction of boolean variables i.e. ( A v B v C’ v D)

an example of boolean formula expressed in CNF is

(A v B v C) ^ (C’ v D) ^ (D’ v A)

and solving the SAT problem means finding the combination of values for the variables in the formula that satisfy it like A=1, B=0, C=0, D=0

This is a NP-Complete problem. Actually it is the first problem which has been proven to be NP-Complete by Stepehn Cook and Leonid Levin

A particular type of SAT problem is the 3-SAT which is a SAT in which all clauses have three variables.

The DPLL algorithm is way to solve SAT problem (which practically depends on the hardness of the input) that recursively creates a tree of potential solution

Suppose you want to solve a 3-SAT problem like this

(A v B v C) ^ (C’ v D v B) ^ (B v A’ v C) ^ (C’ v A’ v B’)

if we enumerate the variables like A=1 B=2 C=3 D=4 and se negative numbers for negated variables like A’ = -1 then the same formula can be written in Python like this

[[1,2,3],[-3,4,2],[2,-1,3],[-3,-1,-2]]

now imagine to create a tree in which each node consists of a partial solution. In our example we also depicted a vector of the clauses satisfied by the solution

the root node is [-1,-1,-1,-1] which means no values have been yet assigned to the variables neither 0 nor 1

at each iteration:

1. we take the first unsatisfied clause then

2. if there are no more unassigned variables we can use to satisfy that clause then there can’t be valid solutions in this branch of the search tree and the algorithm shall return None

3. otherwise we take the first unassigned variable and set it such it satisfies the clause and start recursively from step 1. If the inner invocation of the algorithm returns None we flip the value of the variable so that it does not satisfy the clause and set the next unassigned variable in order to satisfy the clause. If all the three variables have been tried or there are no more unassigned variable for that clause it means there are no valid solutions in this branch and the algorithm shall return None

See the following example:

from the root node we choose the first variable (A) of the first clause (A v B v C) and set it such it satisfies the clause then A=1 (second node of the search tree)

the continue with the second clause and we pick the first unassigned variable (C) and set it such it satisfies the clause which means C=0 (third node on the left)

we do the same thing for the fourth clause (B v A’ v C) and set B to 1

we try to do the same thing for the last clause we realize we no longer have unassigned variables and the clause is always false. We then have to backtrack to the previous position in the search tree. We change the value we assigned to B and set B to 0. Then we look for another unassigned value that can satisfy the third clause but there are not. Then we have to backtrack again to the second node

Once there we have to flip the assignment of the first variable (C) so that it won’t satisfy the clause and set the next unassigned variable (D) in order to satisfy it (i.e. C=1 and D=1). This also satisfies the third clause which contains C.

The last clause to satisfy (C’ v A’ v B’) has one unassigned variable B which can be then set to 0 in order to satisfy the clause.

In this link http://lowcoupling.com/post/72424308422/a-simple-3-sat-solver-using-dpll you can find also the python code implementing it