The Cook–Levin theorem: hardness of SAT

The hardness half of the Cook–Levin theorem (Cook 1971; Levin 1973), machine-free and in the style of Dahlhaus (Dahlhaus 1983): every existential-second-order definable problem admits an ordered first-order reduction to SAT (DescriptiveComplexity.sat_hard_of_sigmaSODefinable). Since NP is defined as Σ₁-definability (DescriptiveComplexity.Hierarchy), together with the membership half DescriptiveComplexity.sat_sigmaSODefinable this makes SAT NP-complete (DescriptiveComplexity.SAT_NP_complete) – relying on no axioms beyond Lean's standard three, as #print axioms confirms.

Given the single second-order block B and the first-order kernel φ of a Σ₁ definition of a problem Q, the reduction interprets, inside an ordered input structure A, the CNF instance of the Tseitin encoding (Tseitin 1968) of φ (DescriptiveComplexity.Problems.Sat.Tseitin):

• propositional variables: one per relation variable i of B and B.arity i-tuple over A (element (Sum.inr (Sum.inl i), x)), and one per subformula position p of φ and context tuple (element (Sum.inr (Sum.inr ⟨m, p⟩), x));
• clauses: up to three kinds per position (elements (Sum.inl (Sum.inl (⟨m, p⟩, k)), u)), plus the top-level unit clause (Sum.inl (Sum.inr ()), u) forcing the root variable;
• tuples of length DescriptiveComplexity.tseitinDim B φ are padded canonically with minimal elements of the order – the one place where the order is used; non-canonical tuples are junk: they are neither clauses nor occur in any clause.

The correctness proof (DescriptiveComplexity.tseitin_satisfiable_iff) composes the characterization lemmas of the interpreted relations with the semantic equivalence DescriptiveComplexity.Tseitin.satCond_iff_gates and the gate-correctness lemmas DescriptiveComplexity.Tseitin.gates_realize / DescriptiveComplexity.Tseitin.gates_canonVal.

noncomputable def DescriptiveComplexity.tseitinDim {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : ℕ

The dimension of the Tseitin interpretation: large enough for every context tuple of the kernel and every argument tuple of a block variable.

Equations

• DescriptiveComplexity.tseitinDim B φ = max (DescriptiveComplexity.Tseitin.maxCtx φ) (DescriptiveComplexity.blockArityBound B)

theorem DescriptiveComplexity.maxCtx_le_tseitinDim {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : Tseitin.maxCtx φ ≤ tseitinDim B φ

theorem DescriptiveComplexity.arity_le_tseitinDim {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (i : B.ι) : B.arity i ≤ tseitinDim B φ

def DescriptiveComplexity.TseitinTag {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : Type

The tags of the Tseitin interpretation: clauses of the encoding (per position and kind, plus the top-level unit clause), then propositional variables (per block variable, and per position).

Equations

• DescriptiveComplexity.TseitinTag B φ = ((((m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt φ m) × Fin 3 ⊕ Unit) ⊕ B.ι ⊕ (m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt φ m)

instance DescriptiveComplexity.instFiniteTseitinTag {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : Finite (TseitinTag B φ)

instance DescriptiveComplexity.instNonemptyTseitinTag {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : Nonempty (TseitinTag B φ)

noncomputable def DescriptiveComplexity.tseitinLitFml {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (s : Bool) (tc tx : TseitinTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (tseitinDim B φ))

The defining formula of satPosIn (s = true) and satNegIn (s = false), by clause and variable tag: the literals of the node clauses (DescriptiveComplexity.Tseitin.litF), and the root variable, at fully padded tuples, positively in the top clause.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.tseitinLitFml B φ s tc tx = ⊥

noncomputable def DescriptiveComplexity.tseitinInterp {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.sat (TseitinTag B φ) (tseitinDim B φ)

The Tseitin interpretation: the CNF instance of the encoding of φ, defined inside the ordered input structure.

Equations

• One or more equations did not get rendered due to their size.

Characterization of the interpreted relations

def DescriptiveComplexity.TseitinLitSem {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tc tx : TseitinTag B φ) (u x : Fin (tseitinDim B φ) → A) : Prop

The semantic content of the literal formulas, by clause and variable tag.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.TseitinLitSem B φ s (Sum.inl (Sum.inl (σp, k))) (Sum.inr vt) u x = DescriptiveComplexity.Tseitin.LitSem s φ ⋯ σp.snd k u vt x
• DescriptiveComplexity.TseitinLitSem B φ s tc tx u x = False

Correctness of the reduction

The two directions are stated for an explicit truth assignment of the interpreted instance, so that they can be reused where the assignments themselves matter and not only their existence (counting, DescriptiveComplexity.Problems.Sat.CountingHardness).

def DescriptiveComplexity.tseitinVal {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] (μ : B.Assignment A) (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) : Prop

The valuation of the propositional variables of the encoding determined by an assignment of the block: a block variable at a tuple reads the assignment at the tuple's prefix, a position variable the truth value of its subformula.

Equations

• DescriptiveComplexity.tseitinVal B φ μ (Sum.inl i) x = μ i fun (j : Fin (B.arity i)) => x (Fin.castLE ⋯ j)
• DescriptiveComplexity.tseitinVal B φ μ (Sum.inr σp) x = DescriptiveComplexity.Tseitin.canonVal μ φ σp.fst σp.snd (DescriptiveComplexity.pref ⋯ x)

theorem DescriptiveComplexity.padAssign_tseitinVal {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] (a₀ : A) (μ : B.Assignment A) : Tseitin.padAssign a₀ (tseitinVal B φ μ) = μ

theorem DescriptiveComplexity.padVal_tseitinVal {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] (a₀ : A) (μ : B.Assignment A) : Tseitin.padVal a₀ (tseitinVal B φ μ) = Tseitin.canonVal μ φ

theorem DescriptiveComplexity.tseitin_gates_of_clauses {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (ν : (tseitinInterp B φ).Map A → Prop) (hν : ∀ (c : (tseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : (tseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) : Tseitin.Gates (Tseitin.padAssign a₀ fun (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) => ν (Sum.inr vt, x)) φ (Tseitin.padVal a₀ fun (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) => ν (Sum.inr vt, x)) ∧ Tseitin.RealizeWith (Tseitin.padAssign a₀ fun (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) => ν (Sum.inr vt, x)) φ finZeroElim

From clauses to gates: a truth assignment satisfying every clause of the interpreted instance induces, through canonical padding, a valuation satisfying every gate, and the block assignment it induces realizes the kernel.

theorem DescriptiveComplexity.tseitin_satisfiable_iff {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Satisfiable ((tseitinInterp B φ).Map A) ↔ ∃ (μ : B.Assignment A), Tseitin.RealizeWith μ φ finZeroElim

Correctness of the Tseitin interpretation: the interpreted CNF instance is satisfiable iff some assignment of the block variables realizes the kernel.

theorem DescriptiveComplexity.sorealize_head_iff {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] : SORealize L A [B] φ true ↔ ∃ (μ : B.Assignment A), Tseitin.RealizeWith μ φ finZeroElim

The head of a one-block second-order satisfaction is realization of the kernel in the expansion by an assignment.

noncomputable def DescriptiveComplexity.tseitinReduction {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) [L.IsRelational] (Q : DecisionProblem L) (hφ : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], Q.Holds A ↔ SORealize L A [B] φ true) : OrderedFOReduction Q SAT

The generic Tseitin reduction: an ordered first-order reduction to SAT from any problem defined, on nonempty finite structures, by an existential second-order sentence with a single block.

Equations

• One or more equations did not get rendered due to their size.

The Cook–Levin theorem

theorem DescriptiveComplexity.sat_hard_of_sigmaSODefinable {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) : SigmaSODefinable 1 Q → Nonempty (OrderedFOReduction Q SAT)

The hardness half of the Cook–Levin theorem: every existential-second-order definable problem admits an ordered first-order reduction to SAT. Machine-free NP-hardness in the style of Dahlhaus, by the generic Tseitin reduction DescriptiveComplexity.tseitinReduction. Registered in the Lax archive as Lax904597.CookLevin.sat_hard_of_sigmaSODefinable.

theorem DescriptiveComplexity.SAT_NP_complete : NP.Complete SAT

The Cook–Levin theorem: SAT is NP-complete. Membership is DescriptiveComplexity.sat_sigmaSODefinable; hardness is DescriptiveComplexity.sat_hard_of_sigmaSODefinable, the generic Tseitin reduction. Registered in the Lax archive as Lax904597.CookLevin.SAT_NP_complete.

theorem DescriptiveComplexity.sat_mem_NP : NP.Mem SAT

SAT is in NP.

theorem DescriptiveComplexity.sat_NP_hard : NP.Hard SAT

SAT is NP-hard.