DPLL Satisfiability Search

Worked example: Propagating to SAT

Consider the formula: p,q,r;-p,q;-q,r;-r,p. Let's trace DPLL.

1. Start with empty assignment. No unit clauses exist. Branch on p = true.
2. Under p = true, the clause -p,q becomes the unit clause q. Unit propagation forces q = true.
3. Now q = true. The clause -q,r becomes the unit clause r. Unit propagation forces r = true.
4. Now r = true. The remaining clause -r,p evaluates to true because p = true.
5. All clauses are satisfied. The formula is SAT.

Witness = { p: true, q: true, r: true }

The algorithm deterministically finds the satisfying assignment by first branching on p and then using unit propagation to force the remaining variables, avoiding a full search of the 2³ = 8 possible assignments.

Experiment with the native controls

Open the interactive DPLL Satisfiability Search module.

1. Examine the default Formula which contains clauses separated by semicolons.
2. Click Step to reveal one recursive call after source-order unit propagation. Observe how DPLL selects the first unassigned variable and branches on it (trying true first).
3. Notice when a branch leads to a conflict (a clause evaluates to false), the algorithm backtracks to try the alternative assignment (false).
4. If a unit clause is formed, observe how unit propagation immediately forces the assignment of the remaining literal without branching.
5. Click Finish to immediately find the terminal SAT/UNSAT state and the witness assignment.

Assumptions, boundaries and costs

This visualization uses a simplified, deterministic version of DPLL for educational clarity.

• Variable Selection: The algorithm branches on variables in alphabetical order (p, q, r) rather than using advanced heuristics like VSIDS or MOM.
• Pure Literals: Pure-literal elimination is omitted to focus on branching and unit propagation.
• Bounded Size: The input is restricted to 3 variables and 6 clauses to keep the trace visually manageable and avoid exponential explosion in the browser.

References

The DPLL algorithm forms the basis of modern SAT solvers.

• MIT 16.412J Cognitive Robotics (Spring 2016): Slides 11, 18-21 on propagation and backtrack search.