Every circuit of the row graph is the circuit of a model

The reverse half of the correspondence of DescriptiveComplexity.Problems.Hamilton.CountingGadget: a Hamilton circuit of the row graph of a CNF formula is the relation DescriptiveComplexity.HamGadget.S ν of an exactly-one model ν (DescriptiveComplexity.HamGadget.Circ.eq_S, DescriptiveComplexity.HamGadget.Circ.oneInModel), the model being read off the direction in which each row is entered.

Only the local reading of a circuit is used (DescriptiveComplexity.HamGadget.Circ, from DescriptiveComplexity.IsCircuit.local): every vertex is left once and reached once, along an arc, and no two vertices follow each other both ways.

• A padding vertex has two neighbours, so the circuit passes through it (DescriptiveComplexity.HamGadget.Circ.through).
• Hence an occurrence entered from the left is left to the right, visiting its clause vertex on the way iff it is positive (DescriptiveComplexity.HamGadget.Circ.pairT), and one entered from the right is left to the left, visiting it iff it is negative (DescriptiveComplexity.HamGadget.Circ.pairF).
• Hence a row is swept in one direction, by induction along its occurrences (DescriptiveComplexity.HamGadget.Circ.rowT, DescriptiveComplexity.HamGadget.Circ.rowF).

A clause vertex is then entered from each of its true literals, and it is entered once.

structure DescriptiveComplexity.HamGadget.Circ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (N : Vtx A → Vtx A → Prop) : Prop

A Hamilton circuit of the row graph, read locally.

• succ (u : Vtx A) : Valid u → ∃ (v : Vtx A), N u v

  Every vertex is left.

• pred (v : Vtx A) : Valid v → ∃ (u : Vtx A), N u v

  Every vertex is reached.

• func {u v v' : Vtx A} : N u v → N u v' → v = v'

  A vertex is left once.

• inj {u u' v : Vtx A} : N u v → N u' v → u = u'

  A vertex is reached once.

• arc {u v : Vtx A} : N u v → Arc u v

  The circuit follows the arcs.

• two {u v : Vtx A} : N u v → N v u → ∀ (z : Vtx A), Valid z → z = u ∨ z = v

  Two vertices following each other both ways are the whole graph.

def DescriptiveComplexity.HamGadget.IsPrev {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (pv : Vtx A) (s : Bool) (x c : A) : Prop

The row predecessor of an occurrence: the first padding, or the padding of the previous occurrence.

Equations

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

The neighbours of a vertex

The local forcing

theorem DescriptiveComplexity.HamGadget.Circ.through {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) (hno2 : ∀ (a b : Vtx A), N a b → N b a → False) {p u w : Vtx A} (hp : Valid p) (hout : ∀ (v : Vtx A), Step p v → v = u ∨ v = w) (hin : ∀ (v : Vtx A), Step v p → v = u ∨ v = w) : N u p ∧ N p w ∨ N w p ∧ N p u

The circuit passes through a vertex with two neighbours.

theorem DescriptiveComplexity.HamGadget.Circ.pairT {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) {pv : Vtx A} {x c : A} {s : Bool} (ho : SatOcc.OccIn c x s) (hp : IsPrev pv s x c) (h : N pv (Vtx.ain s x c)) : (s = true → N (Vtx.ain s x c) (Vtx.cls c) ∧ N (Vtx.cls c) (Vtx.bout s x c)) ∧ (s = false → N (Vtx.ain s x c) (Vtx.bout s x c)) ∧ N (Vtx.bout s x c) (Vtx.pad s x c)

An occurrence entered from the left is left to the right, through its clause vertex iff it is positive.

theorem DescriptiveComplexity.HamGadget.Circ.pairF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) {pv : Vtx A} {x c : A} {s : Bool} (ho : SatOcc.OccIn c x s) (hp : IsPrev pv s x c) (h : N (Vtx.pad s x c) (Vtx.bout s x c)) : N (Vtx.ain s x c) pv ∧ (s = true → N (Vtx.bout s x c) (Vtx.ain s x c)) ∧ (s = false → N (Vtx.bout s x c) (Vtx.cls c) ∧ N (Vtx.cls c) (Vtx.ain s x c))

An occurrence entered from the right is left to the left, through its clause vertex iff it is negative.

theorem DescriptiveComplexity.HamGadget.isPrev_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {pv pv' : Vtx A} {x c : A} {s : Bool} (h : IsPrev pv s x c) (h' : IsPrev pv' s x c) : pv = pv'

def DescriptiveComplexity.HamGadget.TLoc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (N : Vtx A → Vtx A → Prop) (s : Bool) (x c : A) : Prop

The occurrence is traversed from the left.

Equations

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

def DescriptiveComplexity.HamGadget.FLoc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (N : Vtx A → Vtx A → Prop) (s : Bool) (x c : A) : Prop

The occurrence is traversed from the right.

Equations

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

theorem DescriptiveComplexity.HamGadget.Circ.rowT {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) {x : A} (hx : SatOccurs A x) (hν : N (Vtx.top x) (Vtx.lft x)) : N (Vtx.lft x) (Vtx.pad0 x) ∧ ∀ (c : A) (s : Bool), SatOcc.OccIn c x s → TLoc N s x c

A row entered from the left is swept from the left.

theorem DescriptiveComplexity.HamGadget.Circ.rowF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) {x : A} (hx : SatOccurs A x) (hν : ¬N (Vtx.top x) (Vtx.lft x)) : N (Vtx.top x) (Vtx.rgt x) ∧ (∀ (c : A) (s : Bool), SatOcc.VarMax x c s → N (Vtx.rgt x) (Vtx.pad s x c)) ∧ ∀ (c : A) (s : Bool), SatOcc.OccIn c x s → FLoc N s x c

A row entered from the right is swept from the right.

theorem DescriptiveComplexity.HamGadget.Circ.oneInModel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) : OneInModel A fun (x : A) => N (Vtx.top x) (Vtx.lft x)

The assignment of a circuit is an exactly-one model.

theorem DescriptiveComplexity.HamGadget.Circ.eq_S {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {N : Vtx A → Vtx A → Prop} (hC : Circ N) {u v : Vtx A} (hu : Valid u) : N u v ↔ S (fun (x : A) => N (Vtx.top x) (Vtx.lft x)) u v

A circuit is the circuit of its assignment.

The correspondence

theorem DescriptiveComplexity.HamGadget.circ_of_isCircuit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {Nxt : { v : Vtx A // Valid v } → { v : Vtx A // Valid v } → Prop} (h : IsCircuit (fun (u v : { v : Vtx A // Valid v }) => Arc ↑u ↑v) Nxt) : Circ fun (u v : Vtx A) => ∃ (hu : Valid u) (hv : Valid v), Nxt ⟨u, hu⟩ ⟨v, hv⟩

A Hamilton circuit of the row graph, read locally.

noncomputable def DescriptiveComplexity.HamGadget.modelEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : { ν : A → Prop // OneInModel A ν } ≃ { Nxt : { v : Vtx A // Valid v } → { v : Vtx A // Valid v } → Prop // IsCircuit (fun (u v : { v : Vtx A // Valid v }) => Arc ↑u ↑v) Nxt }

The Hamilton circuits of the row graph are the exactly-one models of the formula, bijectively.

Equations

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