The Standard Algorithm

Davis-Putnam-Logeman-Loveland

The algorithm which is the most popular solution to the satisfiability problem was originally developed by Martin Davis, Hillary Putnam, George Logemann and Donald W. Loveland in 1962. Below I will try to give a simple outline of how this algorithm works which will, hopefully, clarify the design decisions made later.

Satisfaction a Clause at a Time

The search for satisfiability is essentially a search for values assigned to variables in the formula which make the entire formula true. Since we know that our formula is in CNF (see previous post) we can exploit some convenient properties to make it easier to find good assignments.

1. Only one literal needs to be true in a clause for the entire clause to be true
2. When every clause in a formula is true the entire formula is true

Assigning Values

Given the formula:

1: (pV~q)&(~pVqVr)

We can assign the values true or false to either p, q or r.

If we assigned p to true then the literal p is true and ~p is false.

If we assign both r and p to be true then the first clause, (pV~q), is true because p is true. The second clause, (~pVqVr), is true because r is true. Thus the entire formula is true and we know don't even need to try out any assignments for q.

A Two Step Search

The search procedure can be divided into two easy steps. There is actually an extra step described in the original algorithm but is not employed commonly in real world solvers.

1. Unit Propogation - If any clause in the formula contains a single literal whose variable has not been assigned (and all other literals are false) then we know that in order to make that clause true we must make that literal true. These literals are called unit literals. In this step we repeatedly assign values to variables to make any unit literals true.
2. Variable Selection - At this step we select a variable which has not yet been assigned a value and our search tree branches on assigning it true or false.