2. The DPLL Algorithm

DPLL Algorithm

The Davis-Putnam-Logemann-Loveland (DPPL) algorithm was proposed in the 1962. It is a divide-and-conquer backtrack-search type algorithm, it works as follows:

• Run pure literal elimination and unit clause propagation.
• If any clauses remain unsatisfied, we branch on any remaining variable $P$:
  • Choose to make $P:=\perp$ by adding $\neg P$ to $U$
  • Choose to make $P:=\top$ by adding $P$ to $U$
• We can achieve this by recursively calling the DPLL Algorithm until either:
  • all clauses are satisfied and $C=\varnothing$
  • a conflict is detected in the partial assignment $U$

Link to original

greedy sat algo

unit clause

A unit clause is any clause that contains only a single literal:

$$\neg Q,(P\vee Q),(\neg P\vee \neg R\vee S),(\neg P\vee Q\vee \neg S),(\neg P\vee \neg Q),R,(Q\vee R\vee S)$$

We have no choice in the assignment of unit clauses:

$$Q:=\perp ,R:=\top$$

We can now eliminate these literals:

$$\cancel{\neg Q},(P\vee Q),(\neg P\vee \neg R\vee S),(\neg P\vee Q\vee \neg S),\cancel{(\neg P\vee \neg Q)},\cancel{R},\cancel{(Q\vee R\vee S)}$$

Furthermore, we can simplify the remaining clauses:

$$P,(\neg P\vee S),(\neg P\vee \neg S)$$

We may find this leads to further assignments, repeating the process, we find:

$$\begin{array}{c}P=\top \\ \cancel{P},(\neg P\vee S),(\neg P\vee \neg S)\\ S,\neg S\end{array}$$Link to original