The drawing of the reduction of #1-in-SAT to #Cycle Cover

DescriptiveComplexity.SatCover.drawInterp draws, over the ordered expansion of a CNF formula, the ladder expansion of the base graph with Valiant's gadgets attached: its universe is in bijection with the nodes and the rungs of the ladder graph (DescriptiveComplexity.SatCover.drawEquiv), its arcs are the ladder edges (DescriptiveComplexity.SatCover.drawArc_iff), plus one isolated node with a self-loop so that the universe is never empty.

The number of cycle covers of the drawn digraph is then the permanent of the ladder expansion, and the number of exactly-one models is read off it by a remainder modulo 2 ^ L + 1, L the number of levels, and a quotient by 4 to the number of occurrences, both definable cardinalities (DescriptiveComplexity.sharpOneInSat_oneCall_sharpCycleCover).

The two definable cardinalities

noncomputable def DescriptiveComplexity.SatCover.occInterp : RelFOInterpretation SatOcc.satOrd FirstOrder.Language.empty OccTag 2

The occurrences, as a relativized interpretation into the empty vocabulary.

Equations

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

noncomputable def DescriptiveComplexity.SatCover.occInterpEquiv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : occInterp.MapRel A ≃ Occ A

The universe of the interpretation of the occurrences is the occurrences.

Equations

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

theorem DescriptiveComplexity.SatCover.card_occInterp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Nat.card (occInterp.MapRel A) = Nat.card (Occ A)

theorem DescriptiveComplexity.SatCover.three_mul_card_occ_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : 3 * Nat.card (Occ A) ≤ Nat.card (Level A)

There are at least three levels per occurrence.

The drawing

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.FullTag : Type

The tags of the drawing: the nodes and the rungs of the ladder graph, and one extra node.

Equations

• DescriptiveComplexity.SatCover.FullTag = (DescriptiveComplexity.SatCover.DrawTag ⊕ Unit)

noncomputable def DescriptiveComplexity.SatCover.pinF : SatOcc.satOrd.Formula (Fin 6)

Coordinates 2 to 5 pinned to coordinate 0.

Equations

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

noncomputable def DescriptiveComplexity.SatCover.drawDomF : FullTag → SatOcc.satOrd.Formula (Fin 6)

The domain of each tag: the nodes, pinned; the rungs, a node, a node, a level and an index below the width; the extra node, all coordinates the least element.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatCover.drawDomF (Sum.inl (Sum.inl t)) = DescriptiveComplexity.SatCover.vDomF t 0 1 ⊓ DescriptiveComplexity.SatCover.pinF
• DescriptiveComplexity.SatCover.drawDomF (Sum.inr PUnit.unit) = DescriptiveComplexity.SatCover.isMinF 0 ⊓ (DescriptiveComplexity.SatOcc.eqF 1 0 ⊓ DescriptiveComplexity.SatCover.pinF)

noncomputable def DescriptiveComplexity.SatCover.drawArcF : FullTag → FullTag → SatOcc.satOrd.Formula (Fin 2 × Fin 6)

The arcs: the ladder edges, and the self-loop of the extra node.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatCover.drawArcF (Sum.inr PUnit.unit) (Sum.inr PUnit.unit) = ⊤
• DescriptiveComplexity.SatCover.drawArcF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.SatCover.drawInterp : RelFOInterpretation SatOcc.satOrd FirstOrder.Language.digraph FullTag 6

The drawing: the ladder expansion of the attached graph, with an extra node.

Equations

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

theorem DescriptiveComplexity.SatCover.realize_drawDomF_base {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t : VTag} {w : Fin 6 → A} : (drawDomF (Sum.inl (Sum.inl t))).Realize w ↔ VDom t (w 0) (w 1) ∧ w 2 = w 0 ∧ w 3 = w 0 ∧ w 4 = w 0 ∧ w 5 = w 0

theorem DescriptiveComplexity.SatCover.realize_drawDomF_extra {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {w : Fin 6 → A} : (drawDomF (Sum.inr ())).Realize w ↔ (∀ (y : A), w 0 ≤ y) ∧ w 1 = w 0 ∧ w 2 = w 0 ∧ w 3 = w 0 ∧ w 4 = w 0 ∧ w 5 = w 0

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.RungA (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] : Type

The rungs of the ladder graph.

Equations

• DescriptiveComplexity.SatCover.RungA A = DescriptiveComplexity.Rung 3 (DescriptiveComplexity.widths DescriptiveComplexity.SatCover.attachedM)

def DescriptiveComplexity.SatCover.RungDom {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] (t t' : VTag) (l : LevelTag) (j : Fin 3) (w : Fin 6 → A) : Prop

A pair is a rung: two nodes, a level, and the index below the width.

Equations

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

theorem DescriptiveComplexity.SatCover.realize_drawDomF_rung {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] {t t' : VTag} {l : LevelTag} {j : Fin 3} {w : Fin 6 → A} : (drawDomF (Sum.inl (Sum.inr (t, t', l, j)))).Realize w ↔ RungDom t t' l j w

def DescriptiveComplexity.SatCover.pin {A : Type} (p : A × A) : Fin 6 → A

The pair of a node, pinned into a 6-tuple.

Equations

• DescriptiveComplexity.SatCover.pin p = ![p.1, p.2, p.1, p.1, p.1, p.1]

noncomputable def DescriptiveComplexity.SatCover.rungTuple {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] (q : RungA A) : Fin 6 → A

The tuple of a rung.

Equations

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

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

The least element.

Equations

• DescriptiveComplexity.SatCover.least = Finset.univ.min' ⋯

noncomputable def DescriptiveComplexity.SatCover.drawEquiv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] : drawInterp.MapRel A ≃ (V A ⊕ RungA A) ⊕ Unit

The universe of the drawing: the nodes and the rungs of the ladder graph, and the extra node.

Equations

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

The arcs

def DescriptiveComplexity.SatCover.DrawEdge {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] (y y' : (V A ⊕ RungA A) ⊕ Unit) : Prop

The edge relation of the drawing, read on the nodes and the rungs.

Equations

• DescriptiveComplexity.SatCover.DrawEdge (Sum.inl a) (Sum.inl b) = DescriptiveComplexity.LadderEdge 3 (DescriptiveComplexity.widths DescriptiveComplexity.SatCover.attachedM) a b
• DescriptiveComplexity.SatCover.DrawEdge (Sum.inr PUnit.unit) (Sum.inr PUnit.unit) = True
• DescriptiveComplexity.SatCover.DrawEdge y y' = False

theorem DescriptiveComplexity.SatCover.drawArc_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] [Nonempty A] (y y' : (V A ⊕ RungA A) ⊕ Unit) : DGArc (drawEquiv.symm y) (drawEquiv.symm y') ↔ DrawEdge y y'

The arcs of the drawing are the edges of the ladder graph, and the self-loop of the extra node.