DPLL algorithm definition

Question

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 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 a unit clause, if there is the 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 literally 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.

Answer 1

The DPLL algorithm is based on the backtracking search algorithm for determining the satisfiability of propositional logic equations in conjunctive normal form, i.e. for solving the CNF-SAT problem.

DPLL algorithm consists of three processes:

• backtracking 

• unit propagation 

• pure literal rule

The primary backtracking algorithm works by accepting a real value, assigning a truth value to it, simplifying the formula and then recursively checking if the simplified equation is satisfiable; if this is the case, the original equation 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 query into two simpler sub-queries. The simplification step removes all clauses that become true under the assignment from the formula and all literals that become false from the remaining clauses.

The DPLL algorithm improves 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 comprises only a single unassigned real value, this clause can only be satisfied by assigning the necessary value to make this real value true. Thus, no choice is necessary. In practice, this often guides to deterministic cascades of units, thus avoiding a large part of the simple search space.

Pure literal elimination 

If a propositional variable happens with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses holding them true. Thus, these clauses do not restrain the search anymore and can be deleted.

if one clause becomes empty then the unsatisfiability of a given partial assignment is detected, which means that if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected unless when all variables are allotted without generating the empty clause, or, in modern implementations if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after an exhaustive search.