(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.
Location: Lecture "Propositional satisfiability"
- Click on "Preview" to see the videos.
→ 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
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation