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$