Satisfiability (DPLL)
3-SAT (8 vars)
Pigeonhole (hard)
Simple AND chain
Step
Run
Reset
Ready
Variables
Clauses
Decision Stack
DPLL algorithm: unit propagation → decide → backtrack on conflict