StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>DPLL requires a problem to be stated in disjunctive normal form, that is, as a set of clauses, each of which must be satisfied.</p> <p>Each clause is a set of literals <code>{l1, l2, ..., ln}</code>, representing the disjunction of those literals (i.e., at least one literal must be true for the clause to be satisfied).</p> <p>Each literal <code>l</code> asserts that some variable is true (<code>x</code>) or that it is false (<code>~x</code>).</p> <p>If any literal is true in a clause, then the clause is satisfied.</p> <p>If all literals in a clause are false, then the clause is unsatisfiable and hence the problem is unsatisfiable.</p> <p>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.</p> <p>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).</p> <p>(1) The first tactic is Pure Literal Elimination: if an unassigned variable <code>x</code> only appears in its positive form in the set of undecided clauses (i.e., the literal <code>~x</code> doesn't appear anywhere) then we can just add <code>x = true</code> to our assignment and satisfy all the clauses containing the literal <code>x</code> (similarly if <code>x</code> only appears in its negative form, <code>~x</code>, we can just add <code>x = false</code> to our assignment).</p> <p>(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 <code>x</code>, we add <code>x = true</code> to our assignment; if the remaining literal is <code>~x</code>, we add <code>x = false</code> to our assignment. This assignment can lead to further opportunities for unit propagation.</p> <p>(3) The third tactic is to simply choose an unassigned variable <code>x</code> and branch the search: one side trying <code>x = true</code>, the other trying <code>x = false</code>.</p> <p>If at any point we end up with an unsatisfiable clause then we have reached a dead end and have to backtrack.</p> <p>There are all sorts of clever further optimisations, but this is the core of almost all SAT solvers.</p> <p>Hope this helps.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload