The row graph of a CNF formula

The graph whose Hamilton circuits are the exactly-one models of a CNF formula, as a graph on a type of its own (DescriptiveComplexity.HamGadget.Vtx): the interpretation that draws it in the formula is in DescriptiveComplexity.Problems.Hamilton.CountingHardness, and everything about circuits is proved here, where a vertex is a constructor and not a tagged tuple.

The graph

Each variable x of the formula has a row, a two-way path

lft x, pad0 x, [ain o₁, bout o₁], pad o₁, [ain o₂, bout o₂], pad o₂, …, pad oₖ, rgt x

through its occurrences o₁ < … < oₖ (DescriptiveComplexity.SatOcc.VarStep), and an entry vertex top x with arcs to both ends; both ends have an arc to the top of the next variable, cyclically. A row is traversed from lft to rgt when the variable is true, from rgt to lft when it is false.

Inside the pair of an occurrence the path is not two-way. For a positive occurrence in the clause c the arcs are ain → cls c → bout and bout → ain: there is no arc ain → bout, so a row traversed from the left – the direction making the literal true – has to visit the clause vertex. A negative occurrence is the mirror image. A clause vertex is therefore visited once per true literal, and a Hamilton circuit visits it once: exactly one literal of each clause is true.

The pad vertices have their two row neighbours and nothing else, which is what forces a row to be traversed in one sweep: a circuit cannot enter a clause vertex from one row and leave into another without stranding a pad.

A formula with no clause has no row; its one model is matched by the single vertex zero, with a loop.

This file

The vertices, the arcs (DescriptiveComplexity.HamGadget.Arc), the circuit of an assignment (DescriptiveComplexity.HamGadget.S), and the order lemmas both directions of the correspondence use: the cyclic successor on the variables of the formula, induction along the occurrences of a variable in both directions, and the rank of an occurrence.

inductive DescriptiveComplexity.HamGadget.Vtx (A : Type) : Type

The vertices of the row graph.

• top {A : Type} (x : A) : Vtx A

  The entry of the row of the variable x.

• lft {A : Type} (x : A) : Vtx A

  The left end of the row of x.

• rgt {A : Type} (x : A) : Vtx A

  The right end of the row of x.

• pad0 {A : Type} (x : A) : Vtx A

  The padding between the left end and the first occurrence of x.

• ain {A : Type} (s : Bool) (x c : A) : Vtx A

  The left vertex of the occurrence of sign s of x in c.

• bout {A : Type} (s : Bool) (x c : A) : Vtx A

  The right vertex of the occurrence of sign s of x in c.

• pad {A : Type} (s : Bool) (x c : A) : Vtx A

  The padding after the occurrence of sign s of x in c.

• cls {A : Type} (c : A) : Vtx A

  The vertex of the clause c.

• zero {A : Type} : Vtx A

  The single vertex of a formula with no clause.

The cyclic order on the variables of the formula

def DescriptiveComplexity.HamGadget.VFirst {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) : Prop

x is the first variable of the formula.

Equations

• DescriptiveComplexity.HamGadget.VFirst x = (DescriptiveComplexity.SatOccurs A x ∧ ∀ (z : A), DescriptiveComplexity.SatOccurs A z → x ≤ z)

def DescriptiveComplexity.HamGadget.VLast {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) : Prop

x is the last variable of the formula.

Equations

• DescriptiveComplexity.HamGadget.VLast x = (DescriptiveComplexity.SatOccurs A x ∧ ∀ (z : A), DescriptiveComplexity.SatOccurs A z → z ≤ x)

def DescriptiveComplexity.HamGadget.VStep {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x y : A) : Prop

y is the variable of the formula immediately after x.

Equations

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

def DescriptiveComplexity.HamGadget.NextVar {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x y : A) : Prop

y follows x cyclically among the variables of the formula.

Equations

• DescriptiveComplexity.HamGadget.NextVar x y = (DescriptiveComplexity.HamGadget.VStep x y ∨ DescriptiveComplexity.HamGadget.VLast x ∧ DescriptiveComplexity.HamGadget.VFirst y)

theorem DescriptiveComplexity.HamGadget.NextVar.occ_left {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x y : A} (h : NextVar x y) : SatOccurs A x

theorem DescriptiveComplexity.HamGadget.NextVar.occ_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x y : A} (h : NextVar x y) : SatOccurs A y

The occurrences of a variable: ranks and inductions

noncomputable def DescriptiveComplexity.HamGadget.occRank {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) (s : Bool) : ℕ

The rank of an occurrence of x: the number of occurrences of x before it.

Equations

• DescriptiveComplexity.HamGadget.occRank x c s = {p : A × Bool | DescriptiveComplexity.SatOcc.OccIn p.1 x p.2 ∧ DescriptiveComplexity.SatOcc.occLt p.1 p.2 c s}.ncard

noncomputable def DescriptiveComplexity.HamGadget.occTotal {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) : ℕ

The number of occurrences of x.

Equations

• DescriptiveComplexity.HamGadget.occTotal x = {p : A × Bool | DescriptiveComplexity.SatOcc.OccIn p.1 x p.2}.ncard

theorem DescriptiveComplexity.HamGadget.exists_occIn_of_occurs {A : Type} [FirstOrder.Language.sat.Structure A] {x : A} (hx : SatOccurs A x) : ∃ (c : A) (s : Bool), SatOcc.OccIn c x s

theorem DescriptiveComplexity.HamGadget.occurs_of_occIn {A : Type} [FirstOrder.Language.sat.Structure A] {x c : A} {s : Bool} (h : SatOcc.OccIn c x s) : SatOccurs A x

theorem DescriptiveComplexity.HamGadget.not_varMax_of_step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s s' : Bool} (h : SatOcc.VarStep x c s c' s') : ¬SatOcc.VarMax x c s

theorem DescriptiveComplexity.HamGadget.not_varMin_of_step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s s' : Bool} (h : SatOcc.VarStep x c s c' s') : ¬SatOcc.VarMin x c' s'

The graph

def DescriptiveComplexity.HamGadget.Valid {A : Type} [FirstOrder.Language.sat.Structure A] : Vtx A → Prop

The vertices that exist: those of variables, occurrences and clauses of the formula, and zero when there is no clause.

Equations

• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.top x_1) = DescriptiveComplexity.SatOccurs A x_1
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.lft x_1) = DescriptiveComplexity.SatOccurs A x_1
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.rgt x_1) = DescriptiveComplexity.SatOccurs A x_1
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.pad0 x_1) = DescriptiveComplexity.SatOccurs A x_1
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.ain s x_1 c) = DescriptiveComplexity.SatOcc.OccIn c x_1 s
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.bout s x_1 c) = DescriptiveComplexity.SatOcc.OccIn c x_1 s
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.pad s x_1 c) = DescriptiveComplexity.SatOcc.OccIn c x_1 s
• DescriptiveComplexity.HamGadget.Valid (DescriptiveComplexity.HamGadget.Vtx.cls c) = DescriptiveComplexity.SatOcc.IsCl c
• DescriptiveComplexity.HamGadget.Valid DescriptiveComplexity.HamGadget.Vtx.zero = ¬∃ (c : A), DescriptiveComplexity.SatOcc.IsCl c

def DescriptiveComplexity.HamGadget.Step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Vtx A → Vtx A → Prop

The arcs of the row graph, between vertices assumed to exist.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.lft x_2) (DescriptiveComplexity.HamGadget.Vtx.pad0 y) = (x_2 = y)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.pad0 x_2) (DescriptiveComplexity.HamGadget.Vtx.lft y) = (x_2 = y)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.pad0 x_2) (DescriptiveComplexity.HamGadget.Vtx.ain s y c) = (x_2 = y ∧ DescriptiveComplexity.SatOcc.VarMin x_2 c s)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.ain s y c) (DescriptiveComplexity.HamGadget.Vtx.pad0 x_2) = (x_2 = y ∧ DescriptiveComplexity.SatOcc.VarMin x_2 c s)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.bout s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.pad s' x' c') = (s = s' ∧ x_2 = x' ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.pad s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.bout s' x' c') = (s = s' ∧ x_2 = x' ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.pad s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.rgt y) = (x_2 = y ∧ DescriptiveComplexity.SatOcc.VarMax x_2 c s)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.rgt y) (DescriptiveComplexity.HamGadget.Vtx.pad s x_2 c) = (x_2 = y ∧ DescriptiveComplexity.SatOcc.VarMax x_2 c s)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.ain s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.cls c') = (s = true ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.cls c') (DescriptiveComplexity.HamGadget.Vtx.bout s x_2 c) = (s = true ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.bout s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.ain s' x' c') = (s = true ∧ s' = true ∧ x_2 = x' ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.bout s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.cls c') = (s = false ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.cls c') (DescriptiveComplexity.HamGadget.Vtx.ain s x_2 c) = (s = false ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.ain s x_2 c) (DescriptiveComplexity.HamGadget.Vtx.bout s' x' c') = (s = false ∧ s' = false ∧ x_2 = x' ∧ c = c')
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.top x_2) (DescriptiveComplexity.HamGadget.Vtx.lft y) = (x_2 = y)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.top x_2) (DescriptiveComplexity.HamGadget.Vtx.rgt y) = (x_2 = y)
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.lft x_2) (DescriptiveComplexity.HamGadget.Vtx.top y) = DescriptiveComplexity.HamGadget.NextVar x_2 y
• DescriptiveComplexity.HamGadget.Step (DescriptiveComplexity.HamGadget.Vtx.rgt x_2) (DescriptiveComplexity.HamGadget.Vtx.top y) = DescriptiveComplexity.HamGadget.NextVar x_2 y
• DescriptiveComplexity.HamGadget.Step DescriptiveComplexity.HamGadget.Vtx.zero DescriptiveComplexity.HamGadget.Vtx.zero = True
• DescriptiveComplexity.HamGadget.Step x✝¹ x✝ = False

def DescriptiveComplexity.HamGadget.Arc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (u v : Vtx A) : Prop

The arcs of the row graph.

Equations

• DescriptiveComplexity.HamGadget.Arc u v = (DescriptiveComplexity.HamGadget.Valid u ∧ DescriptiveComplexity.HamGadget.Valid v ∧ DescriptiveComplexity.HamGadget.Step u v)

def DescriptiveComplexity.HamGadget.S {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) : Vtx A → Vtx A → Prop

The circuit of an assignment, as its “comes next” relation: the row of a true variable is traversed from the left, that of a false one from the right, and a clause vertex is visited from the occurrence of a true literal.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HamGadget.S ν DescriptiveComplexity.HamGadget.Vtx.zero x✝ = (x✝ = DescriptiveComplexity.HamGadget.Vtx.zero)