Computational complexity

Lens

MotivationH

Easy to check, hard to find

A school in Nairobi has to schedule 40 examinations into a few time slots so that no student sits two exams at once. Draw a graph with one vertex per exam and an edge whenever some student takes both: a timetable with $k$ slots is exactly a colouring of the vertices with $k$ colours in which adjacent vertices differ. If someone hands you a proposed timetable, checking it is quick — look at every edge once. Finding one, or proving that none exists with three slots, seems to need a search through up to $3^{40} \approx 1.2 \times 10^{19}$ possibilities.

Compare two puzzles on the same graph. Euler's problem — is there a closed walk using every edge exactly once? — is answered instantly by checking that the graph is connected and every degree is even. Hamilton's problem — is there a cycle through every vertex exactly once? — looks almost the same, yet nobody knows an algorithm that is fundamentally faster than trying exponentially many possibilities.

Computability drew the line between what algorithms can and cannot do in principle. Complexity theory draws a finer line, between what they can do efficiently and what (we believe) they cannot. Its central question was asked by Kurt Gödel in a 1956 letter to John von Neumann, and in its modern form — does P equal NP? — it is one of the seven Millennium Prize Problems. This lesson assumes algorithm design and analysis and basic graph theory.

IntuitionH

Polynomial versus exponential

Measure the cost of an algorithm by the number of elementary steps it takes, as a function of the length $n$ of its input. An algorithm taking $n^2$ or $n^3$ steps slows down gracefully: doubling the input multiplies the time by $4$ or $8$ . An algorithm taking $2^n$ steps does not: each extra bit of input doubles the time, and $2^{100}$ steps would outlast the age of the universe on any conceivable computer.

Polynomial versus exponential growth

Raise k: every polynomial is eventually overtaken by 2^n.

kk = 3

Trace along xx = 1

n^k: y = 1
2^n: y = 2

Try $k = 3$ : the cubic is ahead until about $n = 10$ , after which $2^n$ leaves it behind for good. For every $k$ there is a crossover, because $n^k / 2^n \to 0$ .

The working hypothesis of the subject — the Cobham–Edmonds thesis — is that "efficiently solvable" means "solvable in polynomial time". Like the Church–Turing thesis it is not a theorem, and it is cruder: an $n^{100}$ algorithm is useless and a $1.0001^n$ algorithm may be excellent. But polynomial time has two great virtues. It is robust: Turing machines, random-access machines and real programming languages simulate each other with polynomial overhead, so the class of polynomial-time problems does not depend on the model. And it is closed under composition: a polynomial-time algorithm that calls a polynomial-time subroutine is still polynomial-time.

The second idea is the asymmetry of the timetable. For many problems a "yes" answer has a short certificate — a colouring, a cycle, a satisfying assignment — that can be checked quickly, even when finding it seems hard. NP is the class of such problems.

DefinitionsH

Definitions

A decision problem is a set $L$ of finite strings (over $\{0, 1\}$ , say): the instances whose answer is "yes". Mathematical objects are encoded as strings in any reasonable way — a graph by its adjacency matrix, a number in binary — and $|x|$ is the length of the encoding. (Numbers in unary would be an unreasonable encoding: it is exponentially longer than binary and makes some hard problems look easy.)

Definition— running time, P

A Turing machine $M$ (see computability) runs in time $T : \N \to \N$ if it halts within $T(|x|)$ steps on every input $x$ . $\mathrm{TIME}(T)$ is the class of problems decided by some machine running in time $O(T)$ . The class P is

\mathrm{P} = \bigcup_{k \ge 1} \mathrm{TIME}(n^k),

the problems decidable in polynomial time.

Definition— NP

A problem $L$ is in NP if there are a polynomial $q$ and a polynomial-time machine $V$ , the verifier, such that for every string $x$

x \in L \iff \text{there is a string } y \text{ with } |y| \le q(|x|) \text{ and } V(x, y) = 1.

The string $y$ is a certificate (or witness) for $x$ . Equivalently, NP is the class of problems decided in polynomial time by a nondeterministic Turing machine, one that may branch at each step and accepts if some branch accepts — hence the name: Nondeterministic Polynomial time.

Definition— coNP, PSPACE, EXPTIME

coNP is the class of complements of problems in NP: those whose "no" instances have short, efficiently checkable certificates. PSPACE is the class of problems decidable by a machine that uses at most polynomially many tape cells; EXPTIME $= \bigcup_k \mathrm{TIME}(2^{n^k})$ .

Definition— polynomial-time reduction, NP-complete

$A$ reduces to $B$ in polynomial time, $A \le_p B$ , if there is a polynomial-time computable function $f$ with $x \in A \iff f(x) \in B$ for all $x$ (a Karp reduction). A problem $B$ is NP-hard if $A \le_p B$ for every $A \in \mathrm{NP}$ , and NP-complete if moreover $B \in \mathrm{NP}$ .

An NP-complete problem is a hardest problem in NP: a polynomial-time algorithm for it would give one for every problem in NP.

The problems we will use. Formulas are in conjunctive normal form (CNF): an AND of clauses, each an OR of literals $x_i$ or $\neg x_i$ .

SAT: is a given CNF formula satisfiable? 3-SAT: the same, for formulas with exactly three literals per clause.
INDEPENDENT SET: given a graph $G$ and $k$ , does $G$ have $k$ pairwise non-adjacent vertices?
VERTEX COVER: given $G$ and $k$ , is there a set of at most $k$ vertices touching every edge?
CLIQUE: given $G$ and $k$ , does $G$ have $k$ pairwise adjacent vertices?
3-COL: is a given graph 3-colourable? HAM-CYCLE: does it have a Hamiltonian cycle?

Worked examplesH

Where problems live

Example— Problems in P

Reachability: is there a path from $s$ to $t$ ? Breadth-first search, time linear in the size of the graph.
2-colourability: colour greedily along a breadth-first search; the graph is 2-colourable iff no edge joins two vertices of the same colour (iff it has no odd cycle).
Euler circuits (connected, all degrees even), shortest paths (Dijkstra), minimum spanning trees (Kruskal), 2-SAT (strongly connected components of the implication graph).
Perfect matching in an arbitrary graph — Edmonds's blossom algorithm (1965), the paper in which he argued that polynomial time is the right notion of a "good" algorithm.
Linear programming — Khachiyan's ellipsoid method (1979).
Primality — the AKS algorithm of Agrawal, Kayal and Saxena (2002): deciding whether an $n$ -digit number is prime takes time polynomial in $n$ , not in the number itself.

Example— Problems in NP, with their certificates

SAT: a satisfying assignment; the verifier evaluates the formula.
3-COL: a colouring; check every edge.
HAM-CYCLE: the cycle, as a list of vertices; check it visits each vertex once along edges.
CLIQUE, INDEPENDENT SET, VERTEX COVER: the set of vertices.
COMPOSITE: given $N$ , is it composite? A factor $1 < d < N$ is the certificate; division checks it in polynomial time.

All of these except COMPOSITE are NP-complete. COMPOSITE is in fact in P (by AKS), and the factoring problem in its decision form — does $N$ have a factor at most $k$ ? — is in $\mathrm{NP} \cap \mathrm{coNP}$ (a "no" certificate is the full prime factorisation together with proofs of primality) and is not believed to be NP-complete.

Example— coNP, PSPACE and beyond

TAUT — is a propositional formula true under every assignment? — is coNP-complete. A "yes" certificate would be a short proof; whether every tautology has a polynomial-size proof in some proof system is exactly the question $\mathrm{NP} = \mathrm{coNP}$ (Cook and Reckhow, 1979).
TQBF — is a fully quantified Boolean formula $\forall x_1 \exists x_2 \forall x_3 \cdots \varphi$ true? — is PSPACE-complete, and so are many two-player games, such as generalised geography (played on a directed graph) and Hex on an $n \times n$ board.
Generalised chess on an $n \times n$ board (deciding whether a position is a forced win) is EXPTIME-complete (Fraenkel and Lichtenstein, 1981), so it is provably not in P.

Example— A non-example: a misleading encoding

SUBSET-SUM — given integers $a_1, \dots, a_m$ and $t$ , does some subset sum to $t$ ? — is NP-complete. Dynamic programming solves it in about $m \cdot t$ steps. That is not polynomial time: the input length is about $m \log t$ bits, and $t$ is exponential in $\log t$ . Such "pseudo-polynomial" algorithms are fast only when the numbers are small.

ProofH

Inclusions, NP-completeness and the hierarchy theorem

The basic inclusions

Theorem— Theorem 1

$\mathrm{P} \subseteq \mathrm{NP} \subseteq \mathrm{PSPACE} \subseteq \mathrm{EXPTIME}$ .

Proof

P ⊆ NP. If a polynomial-time machine $M$ decides $L$ , take $V(x, y) = M(x)$ , ignoring the certificate (the empty string will do).

NP ⊆ PSPACE. Let $L$ have verifier $V$ , running in time $p(n)$ , and certificates of length at most $q(n)$ . On input $x$ , go through all strings $y$ of length at most $q(|x|)$ one at a time, in a fixed order, run $V(x, y)$ , and accept if some run accepts. The current $y$ takes $q(n)$ cells; each run of $V$ uses at most $p(n)$ cells (a machine cannot visit more cells than it takes steps), and the space is reused for the next $y$ . Total space $O(p(n) + q(n))$ , a polynomial — although the time is exponential.

PSPACE ⊆ EXPTIME. A machine with state set $Q$ and tape alphabet $\Gamma$ that uses at most $s(n)$ cells has at most $|Q| \cdot s(n) \cdot |\Gamma|^{s(n)} = 2^{O(s(n))}$ distinct configurations (state, head position, tape contents). A deterministic machine that halts never repeats a configuration — otherwise it would cycle forever — so it halts within $2^{O(s(n))}$ steps. For polynomial $s$ this is $2^{O(n^k)}$ .

∎

At least one of these three inclusions is strict, because $\mathrm{P} \ne \mathrm{EXPTIME}$ (Theorem 7 below) — but no one knows which.

Reductions

Theorem— Lemma 2

(a) If $A \le_p B$ and $B \le_p C$ then $A \le_p C$ . (b) If $A \le_p B$ and $B \in \mathrm{P}$ then $A \in \mathrm{P}$ . (c) If $A$ is NP-complete, $B \in \mathrm{NP}$ and $A \le_p B$ , then $B$ is NP-complete.

Proof

(a) Compose the reductions: if $f$ runs in time $p(n)$ and $g$ in time $q(n)$ , then $f(x)$ has length at most $p(|x|)$ , so $g(f(x))$ is computed in time $p(n) + q(p(n))$ , a polynomial. (b) Decide $x \in A$ by computing $f(x)$ and running the polynomial-time algorithm for $B$ ; the same estimate applies. (c) Every $L \in \mathrm{NP}$ satisfies $L \le_p A$ , hence $L \le_p B$ by (a).

∎

Part (c) is how NP-completeness spreads: once one NP-complete problem is known, each new one needs only a single reduction. The first one requires a direct argument.

Theorem— Theorem 3 (Cook 1971, Levin 1973)

SAT is NP-complete.

Proof

Sketch. SAT is in NP: the certificate is an assignment. Now let $L \in \mathrm{NP}$ , with verifier $V$ running in time $T = p(n)$ and certificates of length $q(n)$ . Given $x$ of length $n$ , we build in polynomial time a CNF formula $\varphi_x$ that is satisfiable iff some certificate makes $V$ accept $x$ .

The computation of $V$ on $(x, y)$ is a tableau: a $(T + 1) \times (2T + 1)$ grid whose row $t$ is the configuration at time $t$ (only cells within distance $T$ of the start can be visited). Introduce Boolean variables saying "at time $t$ , cell $i$ holds symbol $s$ ", "at time $t$ the head is at cell $i$ ", "at time $t$ the state is $q$ " — $O(T^2)$ variables in all, since $Q$ and $\Gamma$ are fixed. Add clauses expressing:

each cell holds exactly one symbol, there is exactly one head position and exactly one state, at each time;
row $0$ is the start configuration with $x$ written in place, while the certificate cells are left free — the variables for those cells are the certificate;
each row follows from the previous one by $\delta$ . The key point is locality: in one step only the cell under the head changes and the head moves one cell, so it suffices to require that every $2 \times 3$ window of the tableau is consistent with $\delta$ — a constant number of clauses of constant size per window;
the state at time $T$ is accepting (after halting, a machine is taken to repeat its final configuration).

There are $O(T^2)$ clauses of bounded size, written down in polynomial time. A satisfying assignment describes an accepting computation of $V$ on $(x, y)$ for the certificate $y$ read off row $0$ ; conversely an accepting computation gives a satisfying assignment. So $x \in L \iff \varphi_x \in \mathrm{SAT}$ .

∎

Theorem— Theorem 4

$\mathrm{SAT} \le_p \mathrm{3\text{-}SAT}$ , so 3-SAT is NP-complete.

Proof

Replace each clause by an equisatisfiable set of 3-literal clauses, using fresh variables for each clause. A clause $(\ell_1 \vee \cdots \vee \ell_k)$ with $k \ge 4$ becomes

(\ell_1 \vee \ell_2 \vee z_1) \wedge (\neg z_1 \vee \ell_3 \vee z_2) \wedge (\neg z_2 \vee \ell_4 \vee z_3) \wedge \cdots \wedge (\neg z_{k-3} \vee \ell_{k-1} \vee \ell_k),

$k - 2$ clauses. If some $\ell_j$ is true, set $z_i$ true for $i \le j - 2$ and false for $i \ge j - 1$ : every new clause is satisfied. If all $\ell_j$ are false, the chain forces $z_1$ true, then $z_2$ true, …, then $z_{k-3}$ true, and the last clause fails. Short clauses are padded: $(\ell_1 \vee \ell_2)$ becomes $(\ell_1 \vee \ell_2 \vee w) \wedge (\ell_1 \vee \ell_2 \vee \neg w)$ , and $(\ell_1)$ becomes four clauses with two fresh variables. The new formula is satisfiable iff the old one is, and it is built in linear time. 3-SAT is in NP, so Lemma 2(c) applies.

∎

Theorem— Theorem 5 (Karp 1972: 3-SAT reduces to INDEPENDENT SET)

Given a 3-CNF formula $\varphi$ with clauses $C_1, \dots, C_m$ , let $G_\varphi$ have a vertex $(i, j)$ for the $j$ -th literal of $C_i$ ( $1 \le j \le 3$ ), with an edge between two vertices of the same clause, and an edge between any two vertices labelled by complementary literals $x$ and $\neg x$ . Then $\varphi$ is satisfiable if and only if $G_\varphi$ has an independent set of size $m$ . Hence INDEPENDENT SET is NP-complete.

Proof

( $\Rightarrow$ ) Fix a satisfying assignment and choose, in each clause, one literal that it makes true. The $m$ chosen vertices lie in different clauses, so no triangle edge joins two of them; and two of them cannot be complementary, since both are true. So they form an independent set of size $m$ .

( $\Leftarrow$ ) Let $S$ be independent with $|S| = m$ . Each clause's three vertices are pairwise adjacent, so $S$ contains at most one of them; since there are $m$ clauses and $|S| = m$ , it contains exactly one vertex from each clause. No two literals in $S$ are complementary (they would be adjacent), so we may set every literal in $S$ to true consistently, and give the remaining variables any values. Each clause then contains a true literal, so $\varphi$ is satisfied.

The graph has $3m$ vertices and fewer than $(3m)^2$ edges, and is built in polynomial time; INDEPENDENT SET is in NP (the certificate is the set). By Theorem 4 and Lemma 2(c), it is NP-complete.

∎

Theorem— Corollary 6

VERTEX COVER and CLIQUE are NP-complete.

Proof

$S$ is independent in $G$ iff its complement $V \setminus S$ is a vertex cover: an edge with no endpoint in $V \setminus S$ would have both endpoints in $S$ . So $(G, k) \mapsto (G, |V| - k)$ reduces INDEPENDENT SET to VERTEX COVER. And $S$ is independent in $G$ iff it is a clique in the complement graph $\overline{G}$ (same vertices, edges exactly between distinct non-adjacent pairs), so $(G, k) \mapsto (\overline{G}, k)$ reduces INDEPENDENT SET to CLIQUE. Both problems are in NP.

∎

Thousands of problems have been shown NP-complete in this way: 3-COL (by a gadget reduction from 3-SAT; Garey, Johnson and Stockmeyer, 1976), HAM-CYCLE and the travelling salesperson problem (Karp, 1972), SUBSET-SUM, scheduling, protein folding in simple lattice models, Sudoku and Minesweeper generalised to $n \times n$ boards. A remarkable dichotomy is visible already among the examples: 2-SAT and 2-COL are in P, while 3-SAT and 3-COL are NP-complete.

The hierarchy theorem

Theorem— Theorem 7 (time hierarchy; Hartmanis and Stearns 1965, sharpened by Hennie and Stearns 1966)

If $g$ is time-constructible and $f(n) \log f(n) = o(g(n))$ , then $\mathrm{TIME}(f) \subsetneq \mathrm{TIME}(g)$ . In particular $\mathrm{P} \subsetneq \mathrm{EXPTIME}$ .

Proof

Sketch. ("Time-constructible" means $g(n)$ can be computed in time $O(g(n))$ , which holds for all the usual functions.) Diagonalise, as in the halting problem, but with a clock. Let $D$ be the machine that, on input $w$ , reads $w$ as the code of a machine $M_w$ (allowing arbitrary padding), runs a universal simulation of $M_w$ on $w$ , stops it after $g(|w|)$ of its own steps, and outputs the opposite of $M_w$ 's answer if the simulation finished (and "no" otherwise). $D$ runs in time $O(g)$ . Suppose some machine $M$ decided the same problem as $D$ in time $O(f)$ . A universal machine simulates $t$ steps of $M$ in $O(t \log t)$ steps, with a constant depending only on $M$ ; since $f \log f = o(g)$ , for long enough padded codes $w$ of $M$ the simulation of $M$ on $w$ finishes within $g(|w|)$ steps, and then $D(w) \ne M(w)$ — a contradiction.

For the corollary: every polynomial is eventually below $2^n$ , so $\mathrm{P} \subseteq \mathrm{TIME}(2^n)$ ; and $2^n \cdot n = o(2^{2n})$ , so $\mathrm{TIME}(2^n) \subsetneq \mathrm{TIME}(2^{2n}) \subseteq \mathrm{EXPTIME}$ .

∎

So EXPTIME-complete problems, like generalised chess, provably have no polynomial-time algorithm. The same argument cannot separate P from NP, as the next section explains.

ExplanationH

P versus NP: what is known and what is not

Open. Whether $\mathrm{P} = \mathrm{NP}$ ; whether $\mathrm{NP} = \mathrm{coNP}$ ; whether $\mathrm{P} = \mathrm{PSPACE}$ . None of the inclusions in Theorem 1 is known to be strict. Most researchers believe $\mathrm{P} \ne \mathrm{NP}$ — decades of effort have found no polynomial algorithm for any NP-complete problem, and $\mathrm{P} = \mathrm{NP}$ would make finding proofs about as easy as checking them — but belief is not proof.

Known implications. If any NP-complete problem is in P, then $\mathrm{P} = \mathrm{NP}$ (Lemma 2). If $\mathrm{P} = \mathrm{NP}$ then $\mathrm{NP} = \mathrm{coNP}$ (P is closed under complement). If $\mathrm{P} \ne \mathrm{NP}$ , then there are problems in NP that are neither in P nor NP-complete (Ladner, 1975); factoring and graph isomorphism are the natural candidates, and Babai (2015) showed graph isomorphism is solvable in quasi-polynomial time $2^{(\log n)^{O(1)}}$ .

Why it is hard. Three "barrier" theorems explain why familiar techniques cannot settle the question. Diagonalisation, as in Theorem 7, relativises — it works equally well for machines with access to any oracle — but Baker, Gill and Solovay (1975) built oracles relative to which $\mathrm{P} = \mathrm{NP}$ and others relative to which $\mathrm{P} \ne \mathrm{NP}$ . Razborov and Rudich (1994) showed that "natural" circuit lower-bound arguments would break widely believed cryptographic assumptions; Aaronson and Wigderson (2008) found a further barrier, algebrisation. The best proven lower bounds for explicit problems in NP are, for general circuits, only linear in $n$ .

Cryptography. Public-key cryptography needs functions that are easy to compute and hard to invert. If $\mathrm{P} = \mathrm{NP}$ , no such one-way functions exist, since inverting is an NP search problem. Conversely, $\mathrm{P} \ne \mathrm{NP}$ alone is not known to be enough: cryptography needs problems that are hard on average, for randomly generated keys, not merely in the worst case. So RSA rests on the unproved assumption that factoring products of two random large primes is hard. The general number field sieve factors $N$ in heuristic time $\exp\big(O((\log N)^{1/3} (\log \log N)^{2/3})\big)$ , faster than exponential in the number of digits but not polynomial; and Shor's algorithm (1994) factors in polynomial time on a quantum computer, which is why "post-quantum" cryptosystems based on lattice problems are being deployed. See cryptography.

In practice. NP-completeness is a statement about the worst case. Modern SAT solvers routinely decide industrial instances with millions of variables (in hardware and software verification), and SAT solving has settled mathematical questions, such as the Boolean Pythagorean triples problem (Heule, Kullmann and Marek, 2016). Approximation algorithms, parameterised algorithms and heuristics make many NP-hard optimisation problems tractable for the instances that arise.

Formal mathematicsF

Satisfiability and reductions in Lean

Lean functions come without a cost model, so this module formalises what complexity theory says about correctness — verifiers, search spaces and reductions — and leaves running times to the prose. (Mathlib does contain a Turing-machine notion of polynomial-time computability, Turing.TM2ComputableInPolyTime; the Cook–Levin theorem has been machine-checked in Coq, by Gäher and Kunze in 2021, and in Isabelle, by Balbach in 2023, but not in Mathlib.)

The verifier. A CNF formula over $n$ variables is a list of clauses, each a list of literals; evaluating it under an assignment is the polynomial-time verifier for SAT, and satisfiability is "some certificate passes":

evalLean 4Formally verified

/-- **The verifier for SAT.** A formula is true when every clause is true. Checking a proposed
assignment (a *certificate*) is a single pass over the formula: linear time in its length. -/
def CNF.eval {n : ℕ} (a : Assignment n) (φ : CNF n) : Bool :=
  φ.all (Clause.eval a)

Axioms used: No axiomsformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

SatisfiableLean 4Formally verified

/-- A formula is satisfiable if some assignment makes it true — "some certificate passes the
verifier". This is the shape of every problem in NP. -/
def Satisfiable {n : ℕ} (φ : CNF n) : Prop :=
  ∃ a : Assignment n, φ.eval a = true

Axioms used: No axiomsformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

Brute force runs the verifier on every assignment. The search space has exactly $2^n$ elements, and the algorithm is correct — so SAT is decidable, and the whole question is speed:

length_allAssignmentsLean 4Proved here from basic factsFormally verified

/-- **The search space doubles with every variable**: there are exactly `2 ^ n` assignments. -/
theorem length_allAssignments (n : ℕ) : (allAssignments n).length = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp only [allAssignments, List.length_flatMap, List.length_cons, List.length_nil]
    rw [List.map_const', List.sum_replicate, ih, smul_eq_mul, pow_succ, Nat.mul_comm]

Axioms used: propext, Quot.soundformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

bruteForceLean 4Formally verified

/-- The exponential-time algorithm: run the verifier on all `2 ^ n` assignments. -/
def bruteForce {n : ℕ} (φ : CNF n) : Bool :=
  (allAssignments n).any fun a => φ.eval a

Axioms used: propextformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

bruteForce_correctLean 4Proved here from basic factsFormally verified

/-- **Brute force is correct**: it answers `true` exactly for the satisfiable formulas.
So SAT is decidable; the open question is whether it can be decided in polynomial time. -/
theorem bruteForce_correct {n : ℕ} (φ : CNF n) : bruteForce φ = true ↔ Satisfiable φ := by
  unfold bruteForce Satisfiable
  rw [List.any_eq_true]
  constructor
  · rintro ⟨a, -, ha⟩
    exact ⟨a, ha⟩
  · rintro ⟨a, ha⟩
    exact ⟨a, mem_allAssignments n a, ha⟩

Axioms used: propext, Quot.soundformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

Running the algorithm proves that three pigeons do not fit in two holes. The pigeonhole formulas are a classic of proof complexity: Haken (1985) showed that resolution — the proof system underlying most SAT solvers — needs proofs of exponential length for them.

php32_unsatLean 4Proved here from basic factsFormally verified

/-- Three pigeons do not fit into two holes: PHP(3, 2) is unsatisfiable. The proof *runs* the
brute-force algorithm (64 assignments, checked by `decide`) and then uses its correctness.
For PHP(n + 1, n) the same method needs `2 ^ (n (n + 1))` assignments, and Haken (1985) proved
that even resolution proofs of these formulas must be exponentially long. -/
theorem php32_unsat : ¬ Satisfiable php32 := by
  rw [← bruteForce_correct]
  decide

Axioms used: propext, Quot.soundformal/Lumenary/ComplexityTheory.leanTry it in the Lean web editor

Reductions. Corollary 6, formalised for Mathlib's SimpleGraph. First the complementation fact, proved here and then quoted from Mathlib:

indepSet_iff_vertexCover_complLean 4Proved here from basic factsFormally verified

/-- **Independent sets and vertex covers are complements.** `s` contains no edge if and only if
every edge has an endpoint outside `s`. -/
theorem indepSet_iff_vertexCover_compl {V : Type*} (G : SimpleGraph V) (s : Set V) :
    G.IsIndepSet s ↔ G.IsVertexCover sᶜ := by
  constructor
  · intro hs v w hadj
    by_contra h
    simp only [Set.mem_compl_iff, not_or, not_not] at h
    exact hs h.1 h.2 hadj.ne hadj
  · intro hc v hv w hw _ hadj
    rcases hc hadj with h | h
    · exact h hv
    · exact h hw