The consistent choices are the exactly-one models

A consistent choice of loops (DescriptiveComplexity.SatCover.Consistent) reads as an assignment: a variable is true when the track loop of its positive dummy occurrence is chosen (DescriptiveComplexity.SatCover.toModel). Since the track of a literal is used entirely or not at all, the track loops chosen are exactly those of the true literals, and the one free spoke of each clause is its one true literal: the assignment is an exactly-one model, and the correspondence is a bijection (DescriptiveComplexity.SatCover.consistentEquiv). Hence the permanent of the base graph with the gadgets attached is 4 to the number of occurrences times the number of exactly-one models (DescriptiveComplexity.SatCover.bperm_attachAll_sites_eq).

The tracks of a consistent choice

From choices to models

def DescriptiveComplexity.SatCover.toModel {A : Type} [FirstOrder.Language.sat.Structure A] (U : Finset (Occ A)) (x : A) : Prop

The assignment read off a choice: a variable is true when the track loop of its positive dummy occurrence is chosen.

Equations

• DescriptiveComplexity.SatCover.toModel U x = ∃ (hx : DescriptiveComplexity.SatOccurs A x), DescriptiveComplexity.SatCover.Occ.dummy x hx true ∈ U

theorem DescriptiveComplexity.SatCover.litTrue_toModel_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] {U : Finset (Occ A)} (hU : Consistent U) (o : Occ A) : SatOcc.LitTrue (toModel U) o.x o.s ↔ o ∈ U

A literal is true under the assignment read off a consistent choice iff its occurrences are chosen.

theorem DescriptiveComplexity.SatCover.oneInModel_toModel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] {U : Finset (Occ A)} (hU : Consistent U) : OneInModel A (toModel U)

The assignment read off a consistent choice is an exactly-one model.

From models to choices

noncomputable def DescriptiveComplexity.SatCover.ofModel {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] (ν : A → Prop) : Finset (Occ A)

The choice read off an assignment: the occurrences of the true literals.

Equations

• DescriptiveComplexity.SatCover.ofModel ν = {o : DescriptiveComplexity.SatCover.Occ A | DescriptiveComplexity.SatOcc.LitTrue ν o.x o.s}

theorem DescriptiveComplexity.SatCover.mem_ofModel {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] {ν : A → Prop} {o : Occ A} : o ∈ ofModel ν ↔ SatOcc.LitTrue ν o.x o.s

theorem DescriptiveComplexity.SatCover.consistent_ofModel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] {ν : A → Prop} (hν : OneInModel A ν) : Consistent (ofModel ν)

The choice read off an exactly-one model is consistent.

noncomputable def DescriptiveComplexity.SatCover.consistentEquiv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : { U : Finset (Occ A) // Consistent U } ≃ { ν : A → Prop // OneInModel A ν }

The consistent choices are the exactly-one models.

Equations

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

theorem DescriptiveComplexity.SatCover.bperm_attachAll_sites_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : bperm (Site.attachAll baseM sites) = 4 ^ Fintype.card (Occ A) * ↑(SharpOneInSAT.Count A)

The permanent of the base graph with the gadgets attached is 4 to the number of occurrences times the number of exactly-one models.