Computational logic · SAT
Learn the Davis‑Putnam algorithm, step by step
Write a set of clauses and watch every propagation, every choice and every conflict until the answer.
What you can do
Solve
Answer and valuationStep by step
DLL event by event, with the treeLearn
Short lesson, interactive examples and quiz- Propagatewhat is forced
- Choosewhen there are no unit clauses
- Conflictand go back
- Satisfiablewhen S becomes empty
What is DPLL?
DPLL (Davis–Putnam–Logemann–Loveland), which we call DLL here, is the classic computational logic algorithm for deciding the satisfiability (SAT) of a set of clauses: it combines unit propagation with branching, and it remains the basis of modern SAT solvers.