CNF · 4 vars · 6 clauses

solving…

Assignment

a=?

b=?

c=?

d=?

Formula · each clause under the current assignment

(¬a ∨ b)∧(¬a ∨ ¬b)∧(a ∨ c)∧(¬c ∨ d)∧(c ∨ ¬d)∧(a ∨ d)

Search path · 0 decisions · 0 propagations

(empty)

Pick a formula and press Step. The solver decides a variable, propagates the forced consequences, and backtracks out of every contradiction.

Boolean Satisfiability

The problem every hard problem reduces to

Given a logical formula of variables joined by AND, OR and NOT — can you set each variable true or false so the whole thing comes out true? Checking a proposed assignment is trivial; finding one can be brutal. In 1971 Stephen Cook (and, independently, Leonid Levin) proved SAT is NP-complete: every problem whose answers are easy to verify reduces to it, so one fast SAT solver would crack them all at once. It was the first problem ever proved NP-complete, and it sits at the heart of P versus NP — yet real solvers, armed with the DPLL search and conflict-driven clause learning, routinely settle formulas with millions of variables.

Formula

Controls

Speed

3 steps/s

Clause colour

satisfied

unit: one literal forced

conflict: all false

open: undecided

Search path

▼ decision · ⤺ flipped

unit propagation

← Story ← Back to the atlas