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:
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:
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.