def Clique.HasKClique {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Prop

A graph G has a k-clique iff there exists a k-vertex subset all of whose pairs are adjacent in G.

def Clique.CLIQUE (V : Type u_1) : Set (SimpleGraph V × ℕ)

The language CLIQUE = {⟨G, k⟩ | G has a k-clique} as a set of graph/integer pairs.

inductive ThreeSATToClique.Polarity : Type

The polarity of a propositional literal: positive (x) or negative (¬x).

• pos : Polarity
• neg : Polarity

@[implicit_reducible]

instance ThreeSATToClique.instDecidableEqPolarity : DecidableEq Polarity

def ThreeSATToClique.instReprPolarity.repr : Polarity → ℕ → Std.Format

@[implicit_reducible]

instance ThreeSATToClique.instReprPolarity : Repr Polarity

structure ThreeSATToClique.Literal : Type

A propositional literal: a variable index together with a polarity, so that ⟨i, .pos⟩ represents x_i and ⟨i, .neg⟩ represents ¬x_i.

• varIdx : ℕ
• pol : Polarity

def ThreeSATToClique.instDecidableEqLiteral.decEq (x✝ x✝¹ : Literal) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance ThreeSATToClique.instDecidableEqLiteral : DecidableEq Literal

def ThreeSATToClique.instReprLiteral.repr : Literal → ℕ → Std.Format

@[implicit_reducible]

instance ThreeSATToClique.instReprLiteral : Repr Literal

def ThreeSATToClique.Literal.IsContradictory (l₁ l₂ : Literal) : Prop

Two literals are contradictory when they refer to the same variable but have opposite polarities (e.g. x_i and ¬x_i).

@[implicit_reducible]

instance ThreeSATToClique.instDecidableIsContradictory (l₁ l₂ : Literal) : Decidable (l₁.IsContradictory l₂)

Contradictoriness of literals is decidable, inherited from decidability of equality on variable indices and polarities.

theorem ThreeSATToClique.Literal.IsContradictory.symm' {l₁ l₂ : Literal} (h : l₁.IsContradictory l₂) : l₂.IsContradictory l₁

The "contradictory" relation between literals is symmetric.

def ThreeSATToClique.Literal.eval (σ : ℕ → Bool) (l : Literal) : Bool

Evaluate a literal under a truth assignment σ : ℕ → Bool: a positive literal returns σ l.varIdx, a negative literal returns its negation.

@[reducible, inline]

abbrev ThreeSATToClique.ThreeClause : Type

A 3-clause is a triple of literals, representing the disjunction l₁ ∨ l₂ ∨ l₃ in a 3CNF formula.

def ThreeSATToClique.ThreeClause.literalAt (c : ThreeClause) (j : Fin 3) : Literal

Project the j-th literal (for j : Fin 3) out of a 3-clause.

def ThreeSATToClique.ThreeClause.isSatBy (σ : ℕ → Bool) (c : ThreeClause) : Prop

A 3-clause is satisfied by an assignment σ iff at least one of its three literals evaluates to true under σ.

@[reducible, inline]

abbrev ThreeSATToClique.ThreeCNF : Type

A 3CNF formula, represented as a list of 3-clauses (interpreted as their conjunction).

def ThreeSATToClique.ThreeCNF.IsSatisfiable (φ : ThreeCNF) : Prop

A 3CNF formula φ is satisfiable iff there is an assignment σ under which every clause of φ is satisfied.

def ThreeSATToClique.reductionGraph (φ : ThreeCNF) : SimpleGraph (Fin (List.length φ) × Fin 3)

The graph produced by the standard 3SAT ≤_P CLIQUE reduction. Vertices are pairs (i, j) with i a clause index and j ∈ Fin 3 a literal position; two distinct vertices are adjacent iff they come from different clauses and their literals are not contradictory. A clique of size |φ| then encodes a satisfying assignment by picking, in each clause, a literal that is true.

theorem ThreeSATToClique.contradictory_not_both_true {l₁ l₂ : Literal} {σ : ℕ → Bool} (hc : l₁.IsContradictory l₂) (h₁ : Literal.eval σ l₁ = true) (h₂ : Literal.eval σ l₂ = true) : False

Two contradictory literals cannot both evaluate to true under any single assignment.

noncomputable def ThreeSATToClique.ThreeClause.trueLitPos (σ : ℕ → Bool) (c : ThreeClause) (hsat : isSatBy σ c) : Fin 3

Given a satisfying assignment σ for a clause c, choose (using classical choice) one position j : Fin 3 whose literal evaluates to true.

theorem ThreeSATToClique.ThreeClause.trueLitPos_spec (σ : ℕ → Bool) (c : ThreeClause) (hsat : isSatBy σ c) : Literal.eval σ (c.literalAt (trueLitPos σ c hsat)) = true

Specification of trueLitPos: the literal at the chosen position indeed evaluates to true under σ.

noncomputable def ThreeSATToClique.satisfyingClique (φ : ThreeCNF) (σ : ℕ → Bool) (hsat : ∀ (i : Fin (List.length φ)), ThreeClause.isSatBy σ (List.get φ i)) : Finset (Fin (List.length φ) × Fin 3)

Given a satisfying assignment σ for every clause of φ, build the candidate clique in reductionGraph φ by selecting, for each clause i, the vertex (i, j) where j is a position witnessing the clause's satisfaction.

theorem ThreeSATToClique.satisfyingClique_card (φ : ThreeCNF) (σ : ℕ → Bool) (hsat : ∀ (i : Fin (List.length φ)), ThreeClause.isSatBy σ (List.get φ i)) : (satisfyingClique φ σ hsat).card = List.length φ

The candidate clique satisfyingClique φ σ hsat has exactly |φ| vertices (one per clause), since the map i ↦ (i, _) is injective in i.

theorem ThreeSATToClique.satisfyingClique_isClique (φ : ThreeCNF) (σ : ℕ → Bool) (hsat : ∀ (i : Fin (List.length φ)), ThreeClause.isSatBy σ (List.get φ i)) : (reductionGraph φ).IsClique ↑(satisfyingClique φ σ hsat)

The candidate set satisfyingClique φ σ hsat is indeed a clique in reductionGraph φ: any two of its vertices come from different clauses, and their selected literals are both true under σ, hence not contradictory.

theorem ThreeSATToClique.satisfiable_imp_clique (φ : ThreeCNF) (hsat : φ.IsSatisfiable) : ∃ (s : Finset (Fin (List.length φ) × Fin 3)), (reductionGraph φ).IsNClique (List.length φ) s

Forward direction of the 3SAT ≤_P CLIQUE reduction: if φ is satisfiable, then reductionGraph φ contains a |φ|-clique.

theorem ThreeSATToClique.clique_imp_satisfiable (φ : ThreeCNF) (s : Finset (Fin (List.length φ) × Fin 3)) (hclique : (reductionGraph φ).IsNClique (List.length φ) s) : φ.IsSatisfiable

Backward direction of the 3SAT ≤_P CLIQUE reduction: a |φ|-clique in reductionGraph φ must hit every clause exactly once (since edges only join different clauses) and pick a pairwise non-contradictory set of literals; setting variables to make all chosen positive literals true yields a satisfying assignment for φ.

theorem ThreeSATToClique.reduction_correct (φ : ThreeCNF) : φ.IsSatisfiable ↔ ∃ (s : Finset (Fin (List.length φ) × Fin 3)), (reductionGraph φ).IsNClique (List.length φ) s

Correctness of the 3SAT ≤_P CLIQUE reduction. A 3CNF formula φ is satisfiable iff its reduction graph reductionGraph φ contains a clique of size |φ|.

inductive CliqueReduction.SATCliqueSymbol : Type

Tape alphabet used to encode either a 3SAT instance or a CLIQUE instance on a single Turing-machine tape. The symbol sat φ represents an encoded 3CNF formula φ, and clique φ represents the encoded CLIQUE instance ⟨reductionGraph φ, |φ|⟩.

• sat (φ : ThreeSATToClique.ThreeCNF) : SATCliqueSymbol
• clique (φ : ThreeSATToClique.ThreeCNF) : SATCliqueSymbol

def CliqueReduction.ThreeSATEnc : Set (List SATCliqueSymbol)

Encoded 3SAT language: those single-symbol tape strings [.sat φ] whose underlying formula φ is satisfiable.

def CliqueReduction.CLIQUEEnc : Set (List SATCliqueSymbol)

Encoded CLIQUE language (specialized to instances arising from the reduction): the single-symbol strings [.clique φ] whose reduction graph reductionGraph φ contains a |φ|-clique.

def CliqueReduction.threeSATToCliqueEnc : List SATCliqueSymbol → List SATCliqueSymbol

The reduction function f : Σ* → Σ* on encodings: maps [.sat φ] to [.clique φ] and every other input to the empty string.

theorem CliqueReduction.threeSATToCliqueEnc_default {w : List SATCliqueSymbol} (hw : ¬∃ (φ : ThreeSATToClique.ThreeCNF), w = [SATCliqueSymbol.sat φ]) : threeSATToCliqueEnc w = []

On any input that is not of the form [.sat φ], the reduction function threeSATToCliqueEnc returns the empty list.

theorem CliqueReduction.nil_not_mem_CLIQUEEnc : [] ∉ CLIQUEEnc

The empty string is not in the encoded CLIQUE language, since every member of CLIQUEEnc has the form [.clique φ].

theorem CliqueReduction.reduction_enc_correct (φ : ThreeSATToClique.ThreeCNF) : [SATCliqueSymbol.sat φ] ∈ ThreeSATEnc ↔ threeSATToCliqueEnc [SATCliqueSymbol.sat φ] ∈ CLIQUEEnc

Per-formula correctness of the encoded reduction: [.sat φ] ∈ ThreeSATEnc ↔ threeSATToCliqueEnc [.sat φ] ∈ CLIQUEEnc, obtained directly from reduction_correct.

theorem CliqueReduction.threeSATToCliqueEnc_correct (w : List SATCliqueSymbol) : w ∈ ThreeSATEnc ↔ threeSATToCliqueEnc w ∈ CLIQUEEnc

Full correctness of the reduction function as a many-one reduction: for every input string w, w ∈ ThreeSATEnc ↔ threeSATToCliqueEnc w ∈ CLIQUEEnc.

theorem CliqueReduction.threeSATToCliqueEnc_polyTime : TuringMachine.IsPolyTimeComputableFunction threeSATToCliqueEnc

The reduction function threeSATToCliqueEnc is computable in polynomial time; this is the time-complexity content of the 3SAT ≤_P CLIQUE reduction.

theorem CliqueReduction.threeSAT_polyReducible_CLIQUE : TuringMachine.PolyReducible ThreeSATEnc CLIQUEEnc

3SAT ≤_P CLIQUE. The encoded 3SAT language polynomially reduces to the encoded CLIQUE language via threeSATToCliqueEnc.

theorem CliqueReduction.inP_ThreeSAT_of_inP_CLIQUE (hCLIQUE : TuringMachine.InP CLIQUEEnc) : TuringMachine.InP ThreeSATEnc

Corollary (CLIQUE ∈ P → 3SAT ∈ P). Combining the polynomial-time reduction 3SAT ≤_P CLIQUE with closure of P under polynomial-time reductions: if the encoded CLIQUE language is in P, so is encoded 3SAT.