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:

propositional satisfiability (The DPLL procedure is an algorithm for SAT.)

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.

Location: Lecture "Propositional satisfiability"

[external website]

Author: Michael Genesereth

Other notes:

Click on "Preview" to see the videos.

-Paid-

→ Artificial Intelligence: a Modern Approach

A textbook giving a broad overview of all of AI.

Location: Section 7.6, "Effective propositional inference," subsection "A complete backtracking algorithm," pages 221-222