A count-preserving 3-coloring gadget graph of a CNF formula

The gadget graph of DescriptiveComplexity.Problems.ThreeColorability.SatGadget decides satisfiability but does not count models: its OR gate leaves its output free when exactly one input is true. This file builds the graph the counting reduction draws, whose proper 3-colorings are the models of the formula, each 6 · 8 ^ g times, g the number of non-first occurrences (DescriptiveComplexity.SatToColCount.card_proper).

The vertices are a palette T, F, B; a pair of complementary Boolean vertices per variable of the formula and per gate, i.e., per non-first occurrence of a clause, adjacent to each other and to B, so colored T and F in some order; a spoiler per empty clause, adjacent to the palette; and nine triangle vertices per gate. A triangle whose three vertices are attached to three Boolean or palette vertices has exactly two colorings when these are not all equal and none otherwise (DescriptiveComplexity.SatToColCount.tri_card), and the gate z = p ∨ ℓ, p the value of the prefix of the clause before the occurrence and ℓ its literal, is exactly NAE(z, ¬p, ¬ℓ) ∧ NAE(¬p, z, F) ∧ NAE(¬ℓ, z, F) (DescriptiveComplexity.SatToColCount.gate_iff): three triangles per gate, each with two colorings. The value of the last prefix of each clause is forced true by an edge to F.

inductive DescriptiveComplexity.SatToColCount.Pal : Type

The palette.

• T : Pal

  True.

• F : Pal

  False.

• B : Pal

  Base.

@[instance_reducible]

instance DescriptiveComplexity.SatToColCount.instDecidableEqPal : DecidableEq Pal

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.SatToColCount.instFintypePal : Fintype Pal

Equations

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

Two Boolean facts

def DescriptiveComplexity.SatToColCount.bc (b : Bool) : Fin 3

The color of a truth value: 0 for true, 1 for false.

Equations

• DescriptiveComplexity.SatToColCount.bc b = if b = true then 0 else 1

def DescriptiveComplexity.SatToColCount.NAE3 (a b c : Fin 3) : Prop

Three colors are not all equal.

Equations

• DescriptiveComplexity.SatToColCount.NAE3 a b c = ¬(a = b ∧ b = c)

@[instance_reducible]

instance DescriptiveComplexity.SatToColCount.instDecidableNAE3 (a b c : Fin 3) : Decidable (NAE3 a b c)

Equations

• DescriptiveComplexity.SatToColCount.instDecidableNAE3 a b c = id inferInstance

theorem DescriptiveComplexity.SatToColCount.gate_iff (z p l : Bool) : NAE3 (bc z) (bc !p) (bc !l) ∧ NAE3 (bc !p) (bc z) 1 ∧ NAE3 (bc !l) (bc z) 1 ↔ z = (p || l)

The gate: z = p ∨ ℓ iff the three not-all-equal conditions hold.

theorem DescriptiveComplexity.SatToColCount.tri_card (a b c : Fin 3) : a ≠ 2 → b ≠ 2 → c ≠ 2 → Fintype.card { t : Fin 3 → Fin 3 // (t 0 ≠ t 1 ∧ t 0 ≠ t 2 ∧ t 1 ≠ t 2) ∧ t 0 ≠ a ∧ t 1 ≠ b ∧ t 2 ≠ c } = if NAE3 a b c then 2 else 0

A triangle attached to three vertices of colors other than B has two colorings when the three colors are not all equal, none otherwise.

The graph

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.Var (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The variables of the formula.

Equations

• DescriptiveComplexity.SatToColCount.Var A = { x : A // DescriptiveComplexity.SatOccurs A x }

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.Gate (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Type

The gates: the non-first occurrences.

Equations

• DescriptiveComplexity.SatToColCount.Gate A = { o : A × A × Bool // DescriptiveComplexity.SatOcc.Chained o.1 o.2.1 o.2.2 }

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.Bv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Type

The carriers of a Boolean pair: a variable or a gate.

Equations

• DescriptiveComplexity.SatToColCount.Bv A = (DescriptiveComplexity.SatToColCount.Var A ⊕ DescriptiveComplexity.SatToColCount.Gate A)

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.Core (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Type

The vertices outside the triangles.

Equations

• DescriptiveComplexity.SatToColCount.Core A = (DescriptiveComplexity.SatToColCount.Pal ⊕ DescriptiveComplexity.SatToColCount.Bv A × Bool ⊕ { c : A // DescriptiveComplexity.SatOcc.EmptyCl c })

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.V (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Type

The vertices: the core, and nine triangle vertices per gate.

Equations

• DescriptiveComplexity.SatToColCount.V A = (DescriptiveComplexity.SatToColCount.Core A ⊕ DescriptiveComplexity.SatToColCount.Gate A × Fin 3 × Fin 3)

theorem DescriptiveComplexity.SatToColCount.satOccurs_of_occIn {A : Type} [FirstOrder.Language.sat.Structure A] {c x : A} {s : Bool} (h : SatOcc.OccIn c x s) : SatOccurs A x

noncomputable def DescriptiveComplexity.SatToColCount.prefixBv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c y : A} {t : Bool} (h : SatOcc.OccIn c y t) : Bv A × Bool

The prefix vertex of an occurrence: the vertex whose color is the disjunction of the literals of the clause up to it. The literal itself for the first occurrence, the output of the gate otherwise.

Equations

• DescriptiveComplexity.SatToColCount.prefixBv h = if hm : DescriptiveComplexity.SatOcc.MinOcc c y t then (Sum.inl ⟨y, ⋯⟩, t) else (Sum.inr ⟨(c, y, t), ⋯⟩, true)

noncomputable def DescriptiveComplexity.SatToColCount.pred {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (g : Gate A) : A × Bool

The predecessor of a gate.

Equations

• DescriptiveComplexity.SatToColCount.pred g = (Classical.choose ⋯, Classical.choose ⋯)

theorem DescriptiveComplexity.SatToColCount.pred_spec {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (g : Gate A) : SatOcc.SuccOcc (↑g).1 (pred g).1 (pred g).2 (↑g).2.1 (↑g).2.2

noncomputable def DescriptiveComplexity.SatToColCount.negPred {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (g : Gate A) : Core A

The value of the predecessor's prefix, negated.

Equations

• DescriptiveComplexity.SatToColCount.negPred g = Sum.inr (Sum.inl ((DescriptiveComplexity.SatToColCount.prefixBv ⋯).1, !(DescriptiveComplexity.SatToColCount.prefixBv ⋯).2))

def DescriptiveComplexity.SatToColCount.zV {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (g : Gate A) : Core A

The gate output.

Equations

• DescriptiveComplexity.SatToColCount.zV g = Sum.inr (Sum.inl (Sum.inr g, true))

def DescriptiveComplexity.SatToColCount.negLit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (g : Gate A) : Core A

The negated literal of a gate.

Equations

• DescriptiveComplexity.SatToColCount.negLit g = Sum.inr (Sum.inl (Sum.inl ⟨(↑g).2.1, ⋯⟩, !(↑g).2.2))

noncomputable def DescriptiveComplexity.SatToColCount.outer {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (g : Gate A) : Fin 3 → Fin 3 → Core A

The attachment of the triangles of a gate: NAE(z, ¬p, ¬ℓ), NAE(¬p, z, F) and NAE(¬ℓ, z, F).

Equations

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

def DescriptiveComplexity.SatToColCount.CoreE {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Core A → Core A → Prop

The edges between core vertices, in one direction.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatToColCount.CoreE (Sum.inl p) (Sum.inl q) = (p ≠ q)
• DescriptiveComplexity.SatToColCount.CoreE (Sum.inr (Sum.inl (b, s))) (Sum.inr (Sum.inl (b', s'))) = (b = b' ∧ s' = !s)
• DescriptiveComplexity.SatToColCount.CoreE (Sum.inr (Sum.inl val)) (Sum.inl DescriptiveComplexity.SatToColCount.Pal.B) = True
• DescriptiveComplexity.SatToColCount.CoreE (Sum.inr (Sum.inr val)) (Sum.inl val_1) = True
• DescriptiveComplexity.SatToColCount.CoreE x✝¹ x✝ = False

def DescriptiveComplexity.SatToColCount.E {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : V A → V A → Prop

The edges of the graph, in one direction.

Equations

• DescriptiveComplexity.SatToColCount.E (Sum.inl u) (Sum.inl v) = DescriptiveComplexity.SatToColCount.CoreE u v
• DescriptiveComplexity.SatToColCount.E (Sum.inr (g, j, r)) (Sum.inr (g', j', r')) = (g = g' ∧ j = j' ∧ r ≠ r')
• DescriptiveComplexity.SatToColCount.E (Sum.inr (g, j, r)) (Sum.inl v) = (v = DescriptiveComplexity.SatToColCount.outer g j r)
• DescriptiveComplexity.SatToColCount.E x✝¹ x✝ = False

def DescriptiveComplexity.SatToColCount.Proper {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (χ : V A → Fin 3) : Prop

A proper 3-coloring.

Equations

• DescriptiveComplexity.SatToColCount.Proper χ = ∀ (u v : DescriptiveComplexity.SatToColCount.V A), DescriptiveComplexity.SatToColCount.E u v → χ u ≠ χ v

Normalizing the palette

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.palV {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : Pal) : Core A

A palette vertex.

Equations

• DescriptiveComplexity.SatToColCount.palV p = Sum.inl p

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.bvV {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (w : Bv A × Bool) : Core A

A Boolean vertex.

Equations

• DescriptiveComplexity.SatToColCount.bvV w = Sum.inr (Sum.inl w)

@[reducible, inline]

abbrev DescriptiveComplexity.SatToColCount.spV {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : { c : A // SatOcc.EmptyCl c }) : Core A

A spoiler.

Equations

• DescriptiveComplexity.SatToColCount.spV c = Sum.inr (Sum.inr c)

The triangles

def DescriptiveComplexity.SatToColCount.CoreProper {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (κ : Core A → Fin 3) : Prop

The core is properly colored.

Equations

• DescriptiveComplexity.SatToColCount.CoreProper κ = ∀ (u v : DescriptiveComplexity.SatToColCount.Core A), DescriptiveComplexity.SatToColCount.CoreE u v → κ u ≠ κ v

def DescriptiveComplexity.SatToColCount.NormC {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (κ : Core A → Fin 3) : Prop

The palette is colored 0, 1, 2, on the core.

Equations

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

The core colorings are the models

def DescriptiveComplexity.SatToColCount.AllNAE {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (κ : Core A → Fin 3) : Prop

Every triangle sees three colors not all equal.

Equations

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

def DescriptiveComplexity.SatToColCount.modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (κ : Core A → Fin 3) (x : A) : Prop

The assignment read off a core coloring.

Equations

• DescriptiveComplexity.SatToColCount.modelOf κ x = ∃ (h : DescriptiveComplexity.SatOccurs A x), κ (DescriptiveComplexity.SatToColCount.bvV (Sum.inl ⟨x, h⟩, true)) = 0

theorem DescriptiveComplexity.SatToColCount.modelOf_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (κ : Core A → Fin 3) (x : Var A) : modelOf κ ↑x ↔ κ (bvV (Sum.inl x, true)) = 0

theorem DescriptiveComplexity.SatToColCount.bv_ne_two {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {κ : Core A → Fin 3} (hκ : CoreProper κ) (hn : NormC κ) (w : Bv A × Bool) : κ (bvV w) ≠ 2

theorem DescriptiveComplexity.SatToColCount.bv_flip {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {κ : Core A → Fin 3} (hκ : CoreProper κ) (hn : NormC κ) (b : Bv A) (s : Bool) : κ (bvV (b, !s)) = 0 ↔ κ (bvV (b, s)) ≠ 0

theorem DescriptiveComplexity.SatToColCount.lit_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {κ : Core A → Fin 3} (hκ : CoreProper κ) (hn : NormC κ) (x : Var A) (s : Bool) : κ (bvV (Sum.inl x, s)) = 0 ↔ SatOcc.LitTrue (modelOf κ) (↑x) s

theorem DescriptiveComplexity.SatToColCount.satModel_modelOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {κ : Core A → Fin 3} (hκ : CoreProper κ) (hn : NormC κ) (hall : AllNAE κ) : SatModel A (modelOf κ)

A core coloring gives a model.

From a model to a core coloring

def DescriptiveComplexity.SatToColCount.baseVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) : Bv A → Prop

The value of a carrier under an assignment: the variable, or the prefix disjunction of the gate.

Equations

• DescriptiveComplexity.SatToColCount.baseVal ν (Sum.inl x_1) = ν ↑x_1
• DescriptiveComplexity.SatToColCount.baseVal ν (Sum.inr g) = DescriptiveComplexity.SatOcc.PrefixOr ν (↑g).1 (↑g).2.1 (↑g).2.2

def DescriptiveComplexity.SatToColCount.valBv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (w : Bv A × Bool) : Prop

The value of a Boolean vertex.

Equations

• DescriptiveComplexity.SatToColCount.valBv ν w = if w.2 = true then DescriptiveComplexity.SatToColCount.baseVal ν w.1 else ¬DescriptiveComplexity.SatToColCount.baseVal ν w.1

theorem DescriptiveComplexity.SatToColCount.valBv_flip {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (b : Bv A) (s : Bool) : valBv ν (b, !s) ↔ ¬valBv ν (b, s)

theorem DescriptiveComplexity.SatToColCount.valBv_prefix {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) {c y : A} {t : Bool} (h : SatOcc.OccIn c y t) : valBv ν (prefixBv h) ↔ SatOcc.PrefixOr ν c y t

noncomputable def DescriptiveComplexity.SatToColCount.colOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) : Core A → Fin 3

The core coloring of an assignment: the palette 0, 1, 2, every Boolean vertex by its value.

Equations

• DescriptiveComplexity.SatToColCount.colOf ν (Sum.inl DescriptiveComplexity.SatToColCount.Pal.T) = 0
• DescriptiveComplexity.SatToColCount.colOf ν (Sum.inl DescriptiveComplexity.SatToColCount.Pal.F) = 1
• DescriptiveComplexity.SatToColCount.colOf ν (Sum.inl DescriptiveComplexity.SatToColCount.Pal.B) = 2
• DescriptiveComplexity.SatToColCount.colOf ν (Sum.inr (Sum.inl w)) = DescriptiveComplexity.SatToColCount.bc (decide (DescriptiveComplexity.SatToColCount.valBv ν w))
• DescriptiveComplexity.SatToColCount.colOf ν (Sum.inr (Sum.inr val)) = 0

theorem DescriptiveComplexity.SatToColCount.prefixOr_max {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : SatModel A ν) {c x : A} {s : Bool} (hmax : SatOcc.MaxOcc c x s) : SatOcc.PrefixOr ν c x s

theorem DescriptiveComplexity.SatToColCount.coreProper_colOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : SatModel A ν) : CoreProper (colOf ν)

theorem DescriptiveComplexity.SatToColCount.normC_colOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} : NormC (colOf ν)

theorem DescriptiveComplexity.SatToColCount.allNAE_colOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} : AllNAE (colOf ν)

noncomputable def DescriptiveComplexity.SatToColCount.modelEquiv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : { κ : Core A → Fin 3 // (CoreProper κ ∧ NormC κ) ∧ AllNAE κ } ≃ { ν : A → Prop // SatModel A ν }

The core colorings are the models.

Equations

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

The count

theorem DescriptiveComplexity.SatToColCount.card_proper {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : Nat.card { χ : V A → Fin 3 // Proper χ } = 6 * 8 ^ Nat.card (Gate A) * Nat.card { ν : A → Prop // SatModel A ν }

The number of proper 3-colorings of the gadget graph: 6 · 8 ^ g times the number of models, g the number of non-first occurrences.