The base graph of a #1-in-SAT instance

The reduction of #1-in-SAT to #Cycle Cover attaches Valiant's XOR gadget at one site per occurrence of a literal in a clause; this file builds the base graph the gadgets are attached to, and evaluates the terms of the XOR sum (DescriptiveComplexity.Site.xorSum) it leaves.

The graph

An occurrence (DescriptiveComplexity.SatCover.Occ) is a real one, the literal (x, s) in the clause c, or a dummy one, the literal (x, s) in the tautological clause x ∨ ¬x added for every variable x; the dummy clause is written ⊥. Every occurrence o has a track node trk o and a spoke spk o, and every clause, dummy ones included, a hub. The base edges are:

• the track of each literal (x, s): a cycle through the track nodes of its occurrences, in the order of the clauses, the dummy occurrence first (DescriptiveComplexity.SatCover.nextOcc, built on DescriptiveComplexity.cycNext);
• from each spoke to its hub, and from each hub to each of its spokes.

The site of an occurrence pairs the self-loop at its track node with the self-loop at its spoke, so that exactly one of the two is used: the track loop when the literal is true and the spoke loop when it is false. A cycle cover of the base graph with the chosen loops forced is then unique when the choice is consistent (DescriptiveComplexity.SatCover.Consistent) – the track of a literal is used entirely or not at all, so the loops of a literal are all chosen or none, exactly one loop of the two dummy occurrences of a variable is chosen, so that each variable has one value, and exactly one spoke of each clause is free to close a cycle with its hub, so that each clause has exactly one true literal – and does not exist otherwise (DescriptiveComplexity.SatCover.pdel_base). The consistent choices are the exactly-one models (DescriptiveComplexity.SatCover.consistentEquiv).

Occurrences and nodes

def DescriptiveComplexity.SatCover.OccValid {A : Type} [FirstOrder.Language.sat.Structure A] (o : WithBot A × A × Bool) : Prop

An occurrence is valid when it is a real one, (x, s) in the clause c, or the dummy one of a variable.

Equations

• DescriptiveComplexity.SatCover.OccValid o = (o.1 = ⊥ ∧ DescriptiveComplexity.SatOccurs A o.2.1 ∨ ∃ (c : A), o.1 = ↑c ∧ DescriptiveComplexity.SatOcc.OccIn c o.2.1 o.2.2)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Occ (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The occurrences: the real ones and the dummy ones.

Equations

• DescriptiveComplexity.SatCover.Occ A = { o : WithBot A × A × Bool // DescriptiveComplexity.SatCover.OccValid o }

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Occ.c {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : WithBot A

The clause of an occurrence, ⊥ for a dummy one.

Equations

• o.c = (↑o).1

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Occ.x {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : A

The variable of an occurrence.

Equations

• o.x = (↑o).2.1

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Occ.s {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : Bool

The sign of an occurrence.

Equations

• o.s = (↑o).2.2

theorem DescriptiveComplexity.SatCover.Occ.ext {A : Type} [FirstOrder.Language.sat.Structure A] {o o' : Occ A} (hc : o.c = o'.c) (hx : o.x = o'.x) (hs : o.s = o'.s) : o = o'

theorem DescriptiveComplexity.SatCover.Occ.satOccurs {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : SatOccurs A o.x

The variable of an occurrence is a variable of the formula.

theorem DescriptiveComplexity.SatCover.Occ.occIn_of_coe {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) {c : A} (h : o.c = ↑c) : SatOcc.OccIn c o.x o.s

def DescriptiveComplexity.SatCover.Occ.dummy {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) (hx : SatOccurs A x) (s : Bool) : Occ A

The dummy occurrence of a variable.

Equations

• DescriptiveComplexity.SatCover.Occ.dummy x hx s = ⟨(⊥, x, s), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Hub (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The hubs: one per clause, and one per variable for its dummy clause.

Equations

• DescriptiveComplexity.SatCover.Hub A = ({ c : A // DescriptiveComplexity.SatOcc.IsCl c } ⊕ { x : A // DescriptiveComplexity.SatOccurs A x })

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Node (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The nodes of the base graph: a track node and a spoke per occurrence, and the hubs.

Equations

• DescriptiveComplexity.SatCover.Node A = (DescriptiveComplexity.SatCover.Occ A ⊕ DescriptiveComplexity.SatCover.Occ A ⊕ DescriptiveComplexity.SatCover.Hub A)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.trk {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : Node A

The track node of an occurrence.

Equations

• DescriptiveComplexity.SatCover.trk o = Sum.inl o

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.spk {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : Node A

The spoke of an occurrence.

Equations

• DescriptiveComplexity.SatCover.spk o = Sum.inr (Sum.inl o)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.hub {A : Type} [FirstOrder.Language.sat.Structure A] (h : Hub A) : Node A

A hub, as a node.

Equations

• DescriptiveComplexity.SatCover.hub h = Sum.inr (Sum.inr h)

noncomputable def DescriptiveComplexity.SatCover.hubOf {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : Hub A

The hub of the clause of an occurrence.

Equations

• DescriptiveComplexity.SatCover.hubOf o = if h : o.c = ⊥ then Sum.inr ⟨o.x, ⋯⟩ else Sum.inl ⟨o.c.unbot h, ⋯⟩

The tracks

noncomputable def DescriptiveComplexity.SatCover.chain {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (x : A) (s : Bool) : Finset (WithBot A)

The clauses an occurrence of the literal (x, s) can be in, the dummy clause ⊥ first.

Equations

• DescriptiveComplexity.SatCover.chain x s = insert ⊥ (Finset.image WithBot.some {c : A | DescriptiveComplexity.SatOcc.OccIn c x s})

theorem DescriptiveComplexity.SatCover.mem_chain {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] {x : A} {s : Bool} {c : WithBot A} : c ∈ chain x s ↔ c = ⊥ ∨ ∃ (c' : A), c = ↑c' ∧ SatOcc.OccIn c' x s

theorem DescriptiveComplexity.SatCover.chain_nonempty {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (x : A) (s : Bool) : (chain x s).Nonempty

noncomputable def DescriptiveComplexity.SatCover.nextOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : Occ A

The next occurrence of the same literal, cyclically.

Equations

• DescriptiveComplexity.SatCover.nextOcc o = ⟨(DescriptiveComplexity.cycNext (DescriptiveComplexity.SatCover.chain o.x o.s) o.c, o.x, o.s), ⋯⟩

@[simp]

theorem DescriptiveComplexity.SatCover.nextOcc_c {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : (nextOcc o).c = cycNext (chain o.x o.s) o.c

@[simp]

theorem DescriptiveComplexity.SatCover.nextOcc_x {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : (nextOcc o).x = o.x

@[simp]

theorem DescriptiveComplexity.SatCover.nextOcc_s {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : (nextOcc o).s = o.s

The base edges

inductive DescriptiveComplexity.SatCover.BaseEdge {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : Node A → Node A → Prop

The edges of the base graph.

• track {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : BaseEdge (trk o) (trk (nextOcc o))

  Along the track of a literal.

• spoke {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : BaseEdge (spk o) (SatCover.hub (hubOf o))

  From a spoke to its hub.

• hub {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (o : Occ A) : BaseEdge (SatCover.hub (hubOf o)) (spk o)

  From a hub to each of its spokes.

noncomputable def DescriptiveComplexity.SatCover.baseM {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : Node A → Node A → ℤ

The base matrix: the adjacency matrix of the base graph.

Equations

• DescriptiveComplexity.SatCover.baseM n n' = if DescriptiveComplexity.SatCover.BaseEdge n n' then 1 else 0

The sites and the choices

@[instance_reducible]

instance DescriptiveComplexity.SatCover.instFintypeWithBot {A : Type} [Fintype A] : Fintype (WithBot A)

Equations

• DescriptiveComplexity.SatCover.instFintypeWithBot = { elems := DescriptiveComplexity.SatCover.instFintypeWithBot._aux_1, complete := ⋯ }

instance DescriptiveComplexity.SatCover.instFiniteWithBot {A : Type} [Finite A] : Finite (WithBot A)

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instFintypeOcc {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] : Fintype (Occ A)

Equations

• DescriptiveComplexity.SatCover.instFintypeOcc = Subtype.fintype DescriptiveComplexity.SatCover.OccValid

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instFintypeHub {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] : Fintype (Hub A)

Equations

• DescriptiveComplexity.SatCover.instFintypeHub = inferInstance

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instFintypeNode {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] : Fintype (Node A)

Equations

• DescriptiveComplexity.SatCover.instFintypeNode = inferInstance

@[instance_reducible]

instance DescriptiveComplexity.SatCover.instDecidableEqOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : DecidableEq (Occ A)

Equations

• DescriptiveComplexity.SatCover.instDecidableEqOcc = Subtype.instDecidableEq

@[instance_reducible]

instance DescriptiveComplexity.SatCover.instDecidableEqHub {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : DecidableEq (Hub A)

Equations

• DescriptiveComplexity.SatCover.instDecidableEqHub = inferInstance

@[instance_reducible]

instance DescriptiveComplexity.SatCover.instDecidableEqNode {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : DecidableEq (Node A)

Equations

• DescriptiveComplexity.SatCover.instDecidableEqNode = inferInstance

def DescriptiveComplexity.SatCover.site {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : Site (Node A)

The site of an occurrence: the self-loop at its track node, used when the literal is true, paired with the self-loop at its spoke, used when it is false.

Equations

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

noncomputable def DescriptiveComplexity.SatCover.del {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (U : Finset (Occ A)) : Finset (Node A)

The rows deleted by the choice U of the occurrences whose track loop is used: their track nodes, and the spokes of the other occurrences.

Equations

• DescriptiveComplexity.SatCover.del U = Finset.image DescriptiveComplexity.SatCover.trk U ∪ Finset.image DescriptiveComplexity.SatCover.spk Uᶜ

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

A consistent choice: the track loops of a literal are all chosen or none (the track is then used entirely or not at all), and every hub has exactly one spoke whose loop is not chosen, to close a cycle with.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Rem {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (U : Finset (Occ A)) : Type

The nodes left by a choice.

Equations

• DescriptiveComplexity.SatCover.Rem U = { n : DescriptiveComplexity.SatCover.Node A // n ∉ DescriptiveComplexity.SatCover.del U }

theorem DescriptiveComplexity.SatCover.pdel_base {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (U : Finset (Occ A)) : pdel baseM (del U) (del U) = if Consistent U then 1 else 0

The term of the XOR sum of a choice: 1 when the choice is consistent, 0 otherwise.

The XOR sum over all the choices

theorem DescriptiveComplexity.SatCover.site_injective {A : Type} [FirstOrder.Language.sat.Structure A] : Function.Injective site

theorem DescriptiveComplexity.SatCover.mem_cols_map_site {A : Type} [FirstOrder.Language.sat.Structure A] {l : List (Occ A)} {n : Node A} : n ∈ Site.cols (List.map site l) ↔ ∃ o ∈ l, n = trk o ∨ n = spk o

theorem DescriptiveComplexity.SatCover.cols_map_site_nodup {A : Type} [FirstOrder.Language.sat.Structure A] {l : List (Occ A)} (hl : l.Nodup) : (Site.cols (List.map site l)).Nodup

noncomputable def DescriptiveComplexity.SatCover.sites {A : Type} [FirstOrder.Language.sat.Structure A] [Fintype A] : List (Site (Node A))

The sites, enumerated.

Equations

• DescriptiveComplexity.SatCover.sites = List.map DescriptiveComplexity.SatCover.site Finset.univ.toList