DPLL procedure

(30 minutes to learn)

Summary

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.

Context

This concept has the prerequisites:

Goals

  • 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)

-Free-

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.

-Paid-

See also

-No Additional Notes-