DPLL procedure

(30 minutes to learn)


The DPLL procedure is a backtracking-based algorithm for solving SAT instances. It is complete, in the sense that it will eventually return a satisfying assignment or prove that none exists.


This concept has the prerequisites:


  • Know what the DPLL algorithm is
  • Be able to simulate the algorithm on simple examples
  • Understand the motivations for the unit clause and pure symbol heuristics
  • Understand why the algorithm is complete.

Core resources (read/watch one of the following)


Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Author: Michael Genesereth
Other notes:
  • Click on "Preview" to see the videos.


See also

-No Additional Notes-