DPLL search · 3-SAT

n = 3 · m = 2

Formula φ — conjunction of clauses

c1(x₁∨x₂∨x₃)∧c2(¬x₁∨x₂∨¬x₃)

Partial assignment

x₁ = ?x₂ = ?x₃ = ?

Current node

Ready.

verdict = idle

DPLL search tree · depth = 0

open / unexploredexploredconflictSAT

P vs NP

The biggest open question in computer science

P is the class of problems a computer solves quickly. NP is the class where, given an answer, you can verify it quickly. Is every NP problem secretly in P? Decades of research, a $1 million Clay prize, no proof either way. If P = NP, every cryptographic system would crack and every shortest-route problem would melt. Most computer scientists bet P ≠ NP — but nobody knows.

Preset 3-SAT instance

Random 3-SAT

Variables n = 5

Clauses m = 20

Seed = 1

m / n = 4.00 · phase transition ≈ 4.26

Speed · 8 steps/s

Solver stats

elapsed0.0 ms

branches0

unit-prop0

pure-lit0

conflicts0

depth0

verdictidle

Mode

Solve runs DPLL (potentially exponential). Verify just plugs an assignment into m clauses — that's the O(m) certificate that makes 3-SAT lie in NP.

← Back to the atlas