Home

DPLL Interactive Lab

Davis–Putnam–Logemann–Loveland algorithm — step by step exploration

Formula Input (CNF)
Syntax: variables = any word (x1, p, alpha…)  |  negation = - or ¬ or !  |  OR within clause = | or ∨  |  AND between clauses = , or & or newline
Examples:
DPLL Actions
What can I do?
Load a formula to begin.
Formula Clauses (F)
Load a formula to see clauses here.
Variable Assignments
—
Assignment Trail (M)
Decision Propagated
M = ∅
Rule Explanation

Apply an action to see a detailed explanation of the DPLL rule that was used.

Step History
Choose a Literal to Decide
Select any unassigned variable and a value (TRUE or FALSE).
A decision is a free choice — no rule forces it. It will be added to both M and D (decision set).
— or pick manually —
Choose a Unit to Propagate
Decision Heuristics
Each heuristic analyzes the current formula to suggest which literal to decide. Click Decide → to use the suggestion, or go back to pick manually.