Documentation

DescriptiveComplexity.Problems.ThreeColorability.CountDraw

#3-Colorability is one-call `#P`-complete #

The gadget graph of DescriptiveComplexity.Problems.ThreeColorability.CountGadget, drawn over the ordered expansion of a CNF formula (DescriptiveComplexity.SatToColCount.drawInterp): its universe is the set of vertices of the gadget graph (DescriptiveComplexity.SatToColCount.drawEquiv), its edges those of the gadget graph read in both directions. The number of proper 3-colorings is 6 · 8 ^ g times the number of models, g the number of non-first occurrences, a definable cardinality: one division recovers #SAT (DescriptiveComplexity.sharpSat_oneCall_sharpThreeCol).

Tags #

inductive DescriptiveComplexity.SatToColCount.CTag :

The tags of the drawing.

pal (p : Pal) : CTag
A palette vertex, at the pair of least elements.
lit (s : Bool) : CTag
The literal of sign s of a variable x, at (x, x).
gate (s b : Bool) : CTag
The Boolean vertex of polarity b of the gate of the occurrence of sign s of x in c, at (c, x).
spoil : CTag
The spoiler of an empty clause c, at (c, c).
tri (s : Bool) (j r : Fin 3) : CTag
The vertex r of the triangle j of the gate of the occurrence of sign s of x in c, at (c, x).

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SatToColCount.instDecidableEqCTag :

DecidableEq CTag

Equations

DescriptiveComplexity.SatToColCount.instDecidableEqCTag = DescriptiveComplexity.SatToColCount.instDecidableEqCTag.decEq

Dependency graph

def DescriptiveComplexity.SatToColCount.instDecidableEqCTag.decEq (x✝ x✝¹ : CTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

def DescriptiveComplexity.SatToColCount.CTag.code :

CTag → Pal ⊕ Bool ⊕ Bool × Bool ⊕ Unit ⊕ Bool × Fin 3 × Fin 3

The tags, as a sum type.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.SatToColCount.CTag.code_injective :

Function.Injective code

Dependency graph

instance DescriptiveComplexity.SatToColCount.instFiniteCTag :

Dependency graph

Points #

def DescriptiveComplexity.SatToColCount.CDom {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

CTag → A → A → Prop

The pair (c, x) is a point of tag t.

Equations

DescriptiveComplexity.SatToColCount.CDom (DescriptiveComplexity.SatToColCount.CTag.pal p) x✝¹ x✝ = ((∀ (y : A), x✝¹ ≤ y) ∧ x✝ = x✝¹)
DescriptiveComplexity.SatToColCount.CDom (DescriptiveComplexity.SatToColCount.CTag.lit s) x✝¹ x✝ = (x✝ = x✝¹ ∧ DescriptiveComplexity.SatOccurs A x✝¹)
DescriptiveComplexity.SatToColCount.CDom (DescriptiveComplexity.SatToColCount.CTag.gate s b) x✝¹ x✝ = DescriptiveComplexity.SatOcc.Chained x✝¹ x✝ s
DescriptiveComplexity.SatToColCount.CDom DescriptiveComplexity.SatToColCount.CTag.spoil x✝¹ x✝ = (x✝ = x✝¹ ∧ DescriptiveComplexity.SatOcc.EmptyCl x✝¹)
DescriptiveComplexity.SatToColCount.CDom (DescriptiveComplexity.SatToColCount.CTag.tri s j r) x✝¹ x✝ = DescriptiveComplexity.SatOcc.Chained x✝¹ x✝ s

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.least {A : Type} [LinearOrder A] [Fintype A] [Nonempty A] :

A

The least element.

Equations

DescriptiveComplexity.SatToColCount.least = Finset.univ.min' ⋯

Instances For

Dependency graph

theorem DescriptiveComplexity.SatToColCount.least_le {A : Type} [LinearOrder A] [Fintype A] [Nonempty A] (a : A) :

Dependency graph

The formulas #

noncomputable def DescriptiveComplexity.SatToColCount.occursF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

x is a variable of the formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.isMinF {α : Type} (c : α) :

SatOcc.satOrd.Formula α

c is the least element.

Equations

DescriptiveComplexity.SatToColCount.isMinF c = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.leF (Sum.inl c) (Sum.inr 0))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.domF :

CTag → SatOcc.satOrd.Formula (Fin 2)

The domain of each tag.

Equations

Instances For

Dependency graph

inductive DescriptiveComplexity.SatToColCount.OKind :

What a triangle vertex is attached to.

z : OKind
The gate output.
negP : OKind
The negated predecessor.
negL : OKind
The negated literal.
palF : OKind
The palette F.

Instances For

Dependency graph

def DescriptiveComplexity.SatToColCount.outerKind :

Fin 3 → Fin 3 → OKind

What the vertex r of the triangle j of a gate is attached to.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.outerF (s : Bool) :

OKind → CTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The point of tag t' at (1, ·) is what a triangle vertex of the gate of sign s at (0, ·) is attached to, of kind k.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatToColCount.outerF s DescriptiveComplexity.SatToColCount.OKind.palF (DescriptiveComplexity.SatToColCount.CTag.pal DescriptiveComplexity.SatToColCount.Pal.F) = ⊤
DescriptiveComplexity.SatToColCount.outerF s x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.dirF :

CTag → CTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The edges, in one direction, between the point of tag t at (0, ·) and the point of tag t' at (1, ·).

Equations

Instances For

Dependency graph

Realization #

theorem DescriptiveComplexity.SatToColCount.realize_domF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : CTag) (w : Fin 2 → A) :

(domF t).Realize w ↔ CDom t (w 0) (w 1)

Dependency graph

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

prefixBv h = (Sum.inl ⟨y, hy⟩, t) ↔ SatOcc.MinOcc c x s ∧ x = y ∧ s = t

Dependency graph

theorem DescriptiveComplexity.SatToColCount.prefixBv_eq_gate {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : SatOcc.OccIn c x s) {c' x' : A} {s' : Bool} (h' : SatOcc.Chained c' x' s') (b : Bool) :

prefixBv h = (Sum.inr ⟨(c', x', s'), h'⟩, b) ↔ ¬SatOcc.MinOcc c x s ∧ (c, x, s) = (c', x', s') ∧ b = true

Dependency graph

The drawing #

def DescriptiveComplexity.SatToColCount.swapPt (p : Fin 2 × Fin 2) :

Exchanging the two points of an edge formula.

Equations

DescriptiveComplexity.SatToColCount.swapPt p = (p.1.rev, p.2)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToColCount.drawInterp :

RelFOInterpretation SatOcc.satOrd FirstOrder.Language.graph CTag 2

The drawing of the gadget graph: the edges in both directions.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.SatToColCount.sharpThreeCol_draw {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Nonempty A] [Finite A] :

SharpThreeCol.Count (drawInterp.MapRel A) = Nat.card { χ : V A → Fin 3 // Proper χ }

The number of proper 3-colorings of the drawing is that of the gadget graph.

Dependency graph

The reduction #

noncomputable def DescriptiveComplexity.SatToColCount.gateCount :

PolyTerm FirstOrder.Language.sat

The number of gates, as a polynomial term: the non-first occurrences of either sign.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.SatToColCount.gateSignEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) :

{ w : Fin 2 → A // (SatOcc.chainedF s 0 1).Realize w } ≃ { o : A × A // SatOcc.Chained o.1 o.2 s }

The gates of one sign.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.SatToColCount.gateEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

{ o : A × A // SatOcc.Chained o.1 o.2 false } ⊕ { o : A × A // SatOcc.Chained o.1 o.2 true } ≃ Gate A

The gates, by sign.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.SatToColCount.eval_gateCount (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :

PolyTerm.eval A gateCount = Nat.card (Gate A)

Dependency graph

noncomputable def DescriptiveComplexity.sharpSat_oneCall_sharpThreeCol :

OneCallReduction SharpSAT SharpThreeCol

#SAT reduces to #3-Colorability with one call: the count of the drawing is divided by 6 · 8 ^ g, g the number of non-first occurrences.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.sharpThreeCol_sharpP_oneCallComplete :

SharpP.OneCallComplete SharpThreeCol

#3-Colorability is one-call #P-complete. Registered in the Lax archive as Lax859101.ColoringComplete.sharpThreeCol_sharpP_oneCallComplete.

Dependency graph