# 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-