Reducibility
Glossary Contents
←
Chapter I Satisfiability
Ch II →
  1. 01 — The mother problem
  2. 02 — DPLL in Prolog
  3. 03 — Why chip companies care
Chapter I

Satisfiability

The mother problem. Cook (1971) proved SAT NP-complete; Karp (1972) fanned out from it to twenty more problems that look nothing alike but turn out to be the same hardness in disguise.

01

The mother problem

Every other problem in this book is SAT in disguise.

A SAT instance is a Boolean formula in conjunctive normal form: a conjunction of clauses, each a disjunction of literals.

φ=j=1⋀m​(ℓ∈Cj​⋁​ℓ).(1)

The question is whether there exists a 0/1 assignment of the variables that makes (1) evaluate to true. Cook showed that any nondeterministic Turing machine running in polynomial time can be encoded as an instance of (1), which puts SAT at the top of NP. Karp's contribution the next year was to take that single hardness result and propagate it through twenty graph, scheduling, packing, and matching problems — proving them all NP-complete by reduction.

Figures, in plain terms
(1)

Read it left to right, one symbol at a time.

The Greek letter on the far left, φ (phi), is just a name for the whole formula. Whenever the rest of the chapter says "the formula," it means the thing on the right side of that equals sign.

The big stacked symbol next, ⋀ with j = 1 underneath and m on top, is shorthand for AND repeated many times. AND between two truth values just means both must be true: 1 AND 1 = 1, but 1 AND 0 = 0 and 0 AND 0 = 0. Read the stacked version as: "for every j from 1 up to m, AND together the following." So m is the count of things being AND-ed, and the result is true only when every one of them is true.

What gets AND-ed is whatever sits inside the parentheses. Inside, you find another stacked symbol — ⋁ — which is OR repeated. OR between two truth values means at least one must be true: 1 OR 1 = 1, 1 OR 0 = 1, but 0 OR 0 = 0. The stacked version reads: "OR together the following, for every literal pulled from the set" — so it returns true the moment any one literal is true.

The set is C_j (read "C-sub-j"), the j-th clause. A clause is just a handful of items.

Each item, written ℓ (a script "ell"), is a literal — either a plain variable like x₁ or a negated variable like ¬x₂. There is no other shape a literal can take.

Now reassemble: the formula φ is m clauses joined by AND, where each clause is a handful of literals joined by OR.

In plain terms

You have a list of OR-rules. Each rule is a small group of true/false claims joined by OR. Your job is to flip the variables so that every rule has at least one true claim. SAT just asks whether such a flip is possible.

Scan to come back to page 01

← Cover
1/3 · 1/63
02 DPLL in Prolog →