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"
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
See also
-No Additional Notes-