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

theorem DescriptiveComplexity.tseitin_isClause_node {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (σp : (m : ℕ) × Tseitin.NodeAt φ m) (k : Fin 3) (u : Fin (tseitinDim B φ) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(Sum.inl (Sum.inl (σp, k)), u)] ↔ Tseitin.IsClauseSem φ ⋯ σp.snd k u

theorem DescriptiveComplexity.tseitin_isClause_top {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (u : Fin (tseitinDim B φ) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(Sum.inl (Sum.inr ()), u)] ↔ Canon 0 u

theorem DescriptiveComplexity.tseitin_isClause_var {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (u : Fin (tseitinDim B φ) → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(Sum.inr vt, u)]

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

theorem DescriptiveComplexity.tseitin_lit_iff {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) : FirstOrder.Language.Structure.RelMap (if s = true then FirstOrder.Language.satPosIn else FirstOrder.Language.satNegIn) ![(tc, u), (tx, x)] ↔ TseitinLitSem B φ s tc tx u x

Correctness of the reduction

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) (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} (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.

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.

theorem DescriptiveComplexity.sat_mem_NP : NP.Mem SAT

SAT is in NP.

theorem DescriptiveComplexity.sat_NP_hard : NP.Hard SAT

SAT is NP-hard.

theorem DescriptiveComplexity.sat_compl_mem_coNP : coNP.Mem SATᶜ

The complement of SAT (essentially, propositional entailment of ⊥) is in coNP.