Learning LabExplorable explanations
← All artifacts
Complexity Theory

Solve vs Verify: P vs NP Made Concrete

Checking an answer can be instant while finding one takes forever. Watch a DPLL solver grind through an exponential search tree while a checker verifies any solution in a glance: the gap behind P vs NP.

p-vs-npcomplexitysatdpllnp-complete
LiveInteractive · drag, toggle, run it
Complexity Theory / The open question

Solve vs Verify

Here is one Boolean formula in conjunctive normal form: a stack of clauses, each a group of three literals joined by or, all clauses joined by and. Two questions look almost identical. Solving asks whether any assignment of true and false to the variables makes the whole formula true. Verifying asks whether one specific assignment you are handed actually works. The first can take an exponential search. The second is a quick scan. That gap is what P vs NP is about.

Full search space is 28 = 256 possible assignments. Adding one variable doubles it.
Solver steps so far
0
of up to 2^8 = 256 in the worst case
Backtracks
0
wrong branches abandoned
Verifier ops
—
run the check below
The hard job: search for a solution
step 0 / 28
A real DPLL solver: pick a variable, propagate everything forced, branch when stuck, backtrack on conflict. Step through it or let it run.
c0x6∨x2∨x7
c1x2∨x8∨x1
c2x7∨x4∨x6
c3x1∨x8∨x5
c4x1∨x8∨x5
c5x1∨x5∨x3
c6x4∨x3∨x2
c7x7∨x2∨x6
c8x6∨x8∨x2
c9x2∨x7∨x8
c10x8∨x7∨x4
c11x6∨x7∨x2
c12x5∨x8∨x6
c13x1∨x2∨x4
c14x8∨x4∨x5
c15x2∨x6∨x5
c16x6∨x8∨x7
c17x8∨x4∨x7
c18x4∨x8∨x3
c19x7∨x1∨x6
c20x8∨x3∨x7
c21x3∨x5∨x1
c22x1∨x3∨x5
c23x8∨x3∨x1
c24x7∨x1∨x4
c25x8∨x3∨x2
c26x3∨x5∨x8
c27x4∨x7∨x5
c28x8∨x1∨x2
c29x3∨x2∨x7
c30x3∨x7∨x8
c31x2∨x6∨x1
c32x6∨x3∨x4
c33x6∨x4∨x3
The search has not started
Every variable is unassigned. The solver will pick a variable, try true, propagate every forced consequence, and only branch again when nothing is forced. A conflict sends it back to flip an earlier choice.
The gap, and the open question

NP is the class of verify-fast problems. A decision problem is in NP when every yes-instance has a certificate that a polynomial-time checker can confirm. SAT fits: the certificate is a satisfying assignment, and the verifier above reads each clause once. P is the class of problems you can solve in polynomial time. Every problem in P is also in NP, because solving fast is at least as good as checking fast.

SAT is NP-complete. It is in NP, and every other NP problem can be rewritten as a SAT instance in polynomial time. That reduction is why these problems travel together: a fast algorithm for SAT would give a fast algorithm for every problem in NP, from graph colouring to the travelling salesman decision problem. They are all the same hardness in disguise.

P vs NP asks whether solving is really harder than verifying. For SAT and the thousands of other NP-complete problems, no polynomial-time solver is known: the best general methods still search a tree that can blow up exponentially, exactly as you saw above. But nobody has proved that a fast solver cannot exist. P = NP would mean every quickly-checkable problem is also quickly solvable; P ≠ NP would mean some are genuinely harder to solve than to check. Which one is true is still open. The exponential search you watched is the best we currently know how to do, not a proof that nothing better exists.

Real 3-SAT at clause-to-variable ratio 4.2, instances seeded by mulberry32 so they are reproducible. DPLL with unit propagation drives the search; the verifier is a single linear pass over the clauses.