SAT reduces to Clique by an ordered FO reduction

The classical reduction from satisfiability to the clique threshold problem, as a first-order interpretation over the ordered expansion of the language of CNF instances: DescriptiveComplexity.sat_ordered_fo_reduction_clique : SAT ≤ᶠᵒ[≤] Clique.

Vertices of the interpreted marked graph are tagged pairs of elements of the CNF structure (DescriptiveComplexity.SatCliqueTag, dimension 2):

• (pos, (c, x)) / (neg, (c, x)): a positive/negative occurrence of the variable x in the clause c; two occurrence vertices are adjacent iff both are genuine, they belong to distinct clauses, and they are not conflicting – the same variable with opposite signs (DescriptiveComplexity.SatToClique.Compat);
• (cl, (c, c)): one marked vertex per clause, isolated in the graph, so that the cardinality of the marked set is the number of clauses.

A clique at least as large as the marked set must pick one occurrence per clause, pairwise non-conflicting, which is exactly a satisfying assignment; conversely, choosing a true literal in each clause under a satisfying assignment yields such a clique. Empty clauses – which make the CNF unsatisfiable but carry no occurrence vertex – are handled by a spoiler in the mark formula: if some clause is empty, every vertex is marked, and no clique can be as large as the whole universe since clause vertices are isolated.

The formulas do not mention the order. The reduction is nevertheless packaged as an ordered one because DescriptiveComplexity.Clique folds finiteness of the universe into its yes-instances, so correctness can only hold on finite structures – exactly the correctness contract of DescriptiveComplexity.OrderedFOReduction (a plain FOReduction would have to be correct on infinite structures as well, where SAT can hold while no clique instance is a yes-instance).

inductive DescriptiveComplexity.SatCliqueTag : Type

Tags of the clique instance interpreted in a CNF structure.

• pos : SatCliqueTag

  Positive-occurrence vertex, at pairs (c, x).

• neg : SatCliqueTag

  Negative-occurrence vertex, at pairs (c, x).

• cl : SatCliqueTag

  Marked clause vertex, at diagonal pairs (c, c).

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSatCliqueTag : DecidableEq SatCliqueTag

Equations

• DescriptiveComplexity.instDecidableEqSatCliqueTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.instNonemptySatCliqueTag : Nonempty SatCliqueTag

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSatCliqueTag : Fintype SatCliqueTag

Equations

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

def DescriptiveComplexity.SatCliqueTag.ofSign : Bool → SatCliqueTag

The occurrence tag of a sign.

Equations

• DescriptiveComplexity.SatCliqueTag.ofSign true = DescriptiveComplexity.SatCliqueTag.pos
• DescriptiveComplexity.SatCliqueTag.ofSign false = DescriptiveComplexity.SatCliqueTag.neg

The semantic side

def DescriptiveComplexity.SatToClique.Compat {A : Type} [FirstOrder.Language.sat.Structure A] (s₁ s₂ : Bool) (w₁ w₂ : Fin 2 → A) : Prop

Two genuine literal occurrences in distinct clauses that are not conflicting (the same variable with opposite signs): the adjacency condition between occurrence vertices, on the semantic side.

Equations

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

def DescriptiveComplexity.SatToClique.AdjCore {A : Type} [FirstOrder.Language.sat.Structure A] : SatCliqueTag → (Fin 2 → A) → SatCliqueTag → (Fin 2 → A) → Prop

The adjacency condition of the interpreted graph: occurrence vertices are adjacent iff compatible, clause vertices are isolated.

Equations

• DescriptiveComplexity.SatToClique.AdjCore DescriptiveComplexity.SatCliqueTag.pos x✝¹ DescriptiveComplexity.SatCliqueTag.pos x✝ = DescriptiveComplexity.SatToClique.Compat true true x✝¹ x✝
• DescriptiveComplexity.SatToClique.AdjCore DescriptiveComplexity.SatCliqueTag.pos x✝¹ DescriptiveComplexity.SatCliqueTag.neg x✝ = DescriptiveComplexity.SatToClique.Compat true false x✝¹ x✝
• DescriptiveComplexity.SatToClique.AdjCore DescriptiveComplexity.SatCliqueTag.neg x✝¹ DescriptiveComplexity.SatCliqueTag.pos x✝ = DescriptiveComplexity.SatToClique.Compat false true x✝¹ x✝
• DescriptiveComplexity.SatToClique.AdjCore DescriptiveComplexity.SatCliqueTag.neg x✝¹ DescriptiveComplexity.SatCliqueTag.neg x✝ = DescriptiveComplexity.SatToClique.Compat false false x✝¹ x✝
• DescriptiveComplexity.SatToClique.AdjCore x✝³ x✝² x✝¹ x✝ = False

def DescriptiveComplexity.SatToClique.MarkedCore {A : Type} [FirstOrder.Language.sat.Structure A] : SatCliqueTag → (Fin 2 → A) → Prop

The marking condition of the interpreted graph: diagonal clause vertices – or every vertex, if some clause is empty.

Equations

• DescriptiveComplexity.SatToClique.MarkedCore DescriptiveComplexity.SatCliqueTag.cl x✝ = (x✝ 0 = x✝ 1 ∧ DescriptiveComplexity.SatOcc.IsCl (x✝ 0) ∨ ∃ (c : A), DescriptiveComplexity.SatOcc.EmptyCl c)
• DescriptiveComplexity.SatToClique.MarkedCore x✝¹ x✝ = ∃ (c : A), DescriptiveComplexity.SatOcc.EmptyCl c

def DescriptiveComplexity.SatToClique.Genuine {A : Type} [FirstOrder.Language.sat.Structure A] : SatCliqueTag → (Fin 2 → A) → Prop

A vertex stands for an actual literal occurrence of the CNF structure.

Equations

• DescriptiveComplexity.SatToClique.Genuine DescriptiveComplexity.SatCliqueTag.pos x✝ = DescriptiveComplexity.SatOcc.OccIn (x✝ 0) (x✝ 1) true
• DescriptiveComplexity.SatToClique.Genuine DescriptiveComplexity.SatCliqueTag.neg x✝ = DescriptiveComplexity.SatOcc.OccIn (x✝ 0) (x✝ 1) false
• DescriptiveComplexity.SatToClique.Genuine DescriptiveComplexity.SatCliqueTag.cl x✝ = False

theorem DescriptiveComplexity.SatToClique.adjCore_ofSign {A : Type} [FirstOrder.Language.sat.Structure A] {s₁ s₂ : Bool} {w₁ w₂ : Fin 2 → A} : AdjCore (SatCliqueTag.ofSign s₁) w₁ (SatCliqueTag.ofSign s₂) w₂ ↔ Compat s₁ s₂ w₁ w₂

theorem DescriptiveComplexity.SatToClique.AdjCore.exists_sign {A : Type} [FirstOrder.Language.sat.Structure A] {t₁ t₂ : SatCliqueTag} {w₁ w₂ : Fin 2 → A} (h : AdjCore t₁ w₁ t₂ w₂) : ∃ (s₁ : Bool) (s₂ : Bool), t₁ = SatCliqueTag.ofSign s₁ ∧ t₂ = SatCliqueTag.ofSign s₂ ∧ Compat s₁ s₂ w₁ w₂

theorem DescriptiveComplexity.SatToClique.AdjCore.genuine_right {A : Type} [FirstOrder.Language.sat.Structure A] {t₁ t₂ : SatCliqueTag} {w₁ w₂ : Fin 2 → A} (h : AdjCore t₁ w₁ t₂ w₂) : Genuine t₂ w₂

theorem DescriptiveComplexity.SatToClique.AdjCore.ne_clause {A : Type} [FirstOrder.Language.sat.Structure A] {t₁ t₂ : SatCliqueTag} {w₁ w₂ : Fin 2 → A} (h : AdjCore t₁ w₁ t₂ w₂) : w₁ 0 ≠ w₂ 0

theorem DescriptiveComplexity.SatToClique.Genuine.isCl {A : Type} [FirstOrder.Language.sat.Structure A] {t : SatCliqueTag} {w : Fin 2 → A} (h : Genuine t w) : SatOcc.IsCl (w 0)

The formulas and the interpretation

def DescriptiveComplexity.SatToClique.compatF (s₁ s₂ : Bool) : SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The adjacency formula between occurrence vertices of signs s₁, s₂: the FO counterpart of DescriptiveComplexity.SatToClique.Compat. The free variable (i, j) is the j-th component of the i-th vertex.

Equations

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

def DescriptiveComplexity.SatToClique.adjF : SatCliqueTag → SatCliqueTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The adjacency formulas of the interpretation, by tag.

Equations

• DescriptiveComplexity.SatToClique.adjF DescriptiveComplexity.SatCliqueTag.pos DescriptiveComplexity.SatCliqueTag.pos = DescriptiveComplexity.SatToClique.compatF true true
• DescriptiveComplexity.SatToClique.adjF DescriptiveComplexity.SatCliqueTag.pos DescriptiveComplexity.SatCliqueTag.neg = DescriptiveComplexity.SatToClique.compatF true false
• DescriptiveComplexity.SatToClique.adjF DescriptiveComplexity.SatCliqueTag.neg DescriptiveComplexity.SatCliqueTag.pos = DescriptiveComplexity.SatToClique.compatF false true
• DescriptiveComplexity.SatToClique.adjF DescriptiveComplexity.SatCliqueTag.neg DescriptiveComplexity.SatCliqueTag.neg = DescriptiveComplexity.SatToClique.compatF false false
• DescriptiveComplexity.SatToClique.adjF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatToClique.markedF : SatCliqueTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

The mark formulas of the interpretation, by tag: diagonal clause vertices – or everything, if some clause is empty.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatToClique.markedF x✝ = DescriptiveComplexity.SatOcc.exEmptyClF

noncomputable def DescriptiveComplexity.SatToClique.satToClique : FOInterpretation SatOcc.satOrd FirstOrder.Language.markedGraph SatCliqueTag 2

The interpretation producing, from an ordered CNF structure, its clique threshold instance.

Equations

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

Characterizations of the interpreted relations

theorem DescriptiveComplexity.SatToClique.realize_compatF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s₁ s₂ : Bool} {v : Fin 2 × Fin 2 → A} : (compatF s₁ s₂).Realize v ↔ Compat s₁ s₂ (fun (j : Fin 2) => v (0, j)) fun (j : Fin 2) => v (1, j)

theorem DescriptiveComplexity.SatToClique.realize_adjF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t₁ t₂ : SatCliqueTag} {v : Fin 2 × Fin 2 → A} : (adjF t₁ t₂).Realize v ↔ AdjCore t₁ (fun (j : Fin 2) => v (0, j)) t₂ fun (j : Fin 2) => v (1, j)

theorem DescriptiveComplexity.SatToClique.realize_markedF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t : SatCliqueTag} {v : Fin 1 × Fin 2 → A} : (markedF t).Realize v ↔ MarkedCore t fun (j : Fin 2) => v (0, j)

theorem DescriptiveComplexity.SatToClique.satToClique_adj {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : SatCliqueTag) (w₁ w₂ : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgAdj ![(t₁, w₁), (t₂, w₂)] ↔ AdjCore t₁ w₁ t₂ w₂

Characterization of the interpreted adjacency relation.

theorem DescriptiveComplexity.SatToClique.satToClique_marked {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : SatCliqueTag) (w : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.mgMarked ![(t, w)] ↔ MarkedCore t w

Characterization of the interpreted mark relation.

Correctness

theorem DescriptiveComplexity.SatToClique.satisfiable_iff_hasLargeClique (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Satisfiable A ↔ HasLargeClique (satToClique.Map A)

Correctness of the reduction: a finite ordered CNF structure is satisfiable iff its interpreted marked graph has a clique at least as large as the marked set.

noncomputable def DescriptiveComplexity.sat_ordered_fo_reduction_clique : OrderedFOReduction SAT Clique

SAT FO-reduces to Clique on ordered structures: the one-vertex-per-literal-occurrence interpretation SatToClique.satToClique, over the ordered expansion of the language of CNF instances, maps a finite CNF structure to a yes-instance of Clique iff it is satisfiable. (The order is never mentioned by the formulas; the ordered packaging only serves to restrict correctness to finite structures, as required by the finiteness conjunct of DescriptiveComplexity.Clique.)

Equations

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