Boolean SAT Visualizer

DPLL algorithm on 3-CNF formulas with unit propagation and backtracking

FORMULA (3-CNF)

Variables (for random) 5

Clauses (for random) 18 (ratio≈3.6)

RESULT

—

Decisions—

Backtracks—

Unit props—

Clause ratio—

CLAUSE-VARIABLE BIPARTITE GRAPH

DPLL TRACE

Press "Solve Formula" or generate a random formula.

About: 3-SAT asks whether a conjunction of 3-literal clauses can be satisfied — it is the canonical NP-complete problem (Cook-Levin 1971). The DPLL algorithm (Davis-Putnam-Logemann-Loveland, 1962) uses unit propagation (if a clause has one unassigned literal, force it) and pure literal elimination, then makes a decision and backtracks on contradiction. The phase transition near clause-to-variable ratio α≈4.27 (for 3-SAT) marks where instances shift from almost-always-satisfiable to almost-always-unsatisfiable — and hardest instances cluster at this boundary.