Documentation

DescriptiveComplexity.Problems.Hamilton.CountingForward

The circuit of an exactly-one model #

The forward half of the correspondence between the exactly-one models of a CNF formula and the Hamilton circuits of its row graph (DescriptiveComplexity.Problems.Hamilton.CountingGadget): the relation DescriptiveComplexity.HamGadget.S ν of an exactly-one assignment ν is a Hamilton circuit (DescriptiveComplexity.HamGadget.isCircuit_S).

No enumeration of the circuit is written. The relation follows the arcs (DescriptiveComplexity.HamGadget.arc_of_S), leaves every vertex exactly once (DescriptiveComplexity.HamGadget.S_total, DescriptiveComplexity.HamGadget.S_functional) and reaches every vertex (DescriptiveComplexity.HamGadget.S_surj): four case analyses on the kind of a vertex. And a potential increases along it everywhere but at the exit of the last row (DescriptiveComplexity.HamGadget.key_lt): the variable first, then the position in the row, counted from the left for a true variable and from the right for a false one. That is a circuit, by DescriptiveComplexity.isCircuit_of_potential.

source
theorem DescriptiveComplexity.HamGadget.arc_of_S {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {u v : Vtx A} (hu : Valid u) (h : S ν u v) :
Arc u v

The circuit of an assignment follows the arcs.

Dependency graph
source
theorem DescriptiveComplexity.HamGadget.S_functional {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : OneInProper ν) {u v v' : Vtx A} (h : S ν u v) (h' : S ν u v') :
v = v'

The circuit of an exactly-one assignment leaves a vertex at most once.

Dependency graph
source
theorem DescriptiveComplexity.HamGadget.S_total {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} [Finite A] (hν : OneInProper ν) {u : Vtx A} (hu : Valid u) :
∃ (v : Vtx A), S ν u v

The circuit of an exactly-one assignment leaves every vertex.

Dependency graph
source
theorem DescriptiveComplexity.HamGadget.S_surj {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} [Finite A] (hν : OneInProper ν) {v : Vtx A} (hv : Valid v) :
∃ (u : Vtx A), Valid u ∧ S ν u v

The circuit of an exactly-one assignment reaches every vertex.

Dependency graph

The potential #

source
instance DescriptiveComplexity.HamGadget.instFiniteVtx {A : Type} [Finite A] :
Finite (Vtx A)

The vertices of the row graph are finitely many.

Dependency graph
source
noncomputable def DescriptiveComplexity.HamGadget.clsLit {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (c : A) :
A × Bool

The true literal of a clause under an assignment, when there is one.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.HamGadget.clsLit_eq {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : OneInProper ν) {c x : A} {s : Bool} (ho : SatOcc.OccIn c x s) (hT : SatOcc.LitTrue ν x s) :
    clsLit ν c = (x, s)
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.HamGadget.rowKey {A : Type} (ν : A → Prop) (x : A) (p : ℤ) :
    Lex (A × ℤ)

    The key of a row vertex: its variable, then its position, counted from the left when the variable is true and from the right when it is false.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.HamGadget.rowKey_lt_pos {A : Type} [LinearOrder A] {ν : A → Prop} {x : A} {p q : ℤ} (hx : ν x) (h : p < q) :
      rowKey ν x p < rowKey ν x q
      Dependency graph
      source
      theorem DescriptiveComplexity.HamGadget.rowKey_lt_neg {A : Type} [LinearOrder A] {ν : A → Prop} {x : A} {p q : ℤ} (hx : ¬ν x) (h : q < p) :
      rowKey ν x p < rowKey ν x q
      Dependency graph
      source
      noncomputable def DescriptiveComplexity.HamGadget.key {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Nonempty A] (ν : A → Prop) :
      Vtx A → Lex (A × ℤ)

      The potential: the variable of a vertex, then its position in the row; a clause vertex sits in the row of its true literal, between the two vertices of the occurrence.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.HamGadget.topKey_lt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {x : A} {p : ℤ} (hp : 0 < p) (hp' : p ≤ 4 * ↑(occTotal x) + 7) :
        toLex (x, -(4 * ↑(occTotal x) + 8)) < rowKey ν x p
        Dependency graph
        source
        theorem DescriptiveComplexity.HamGadget.key_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} [Nonempty A] (hν : OneInProper ν) {c x : A} {s : Bool} (ho : SatOcc.OccIn c x s) (hT : SatOcc.LitTrue ν x s) :
        key ν (Vtx.cls c) = rowKey ν x (4 * ↑(occRank x c s) + 4)
        Dependency graph
        source
        theorem DescriptiveComplexity.HamGadget.key_lt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} [Finite A] [Nonempty A] (hν : OneInProper ν) {u v : Vtx A} (hu : Valid u) (h : S ν u v) :
        key ν u < key ν v ∨ (∃ (x : A), VLast x ∧ (ν x ∧ u = Vtx.rgt x ∨ ¬ν x ∧ u = Vtx.lft x)) ∨ u = Vtx.zero

        The potential increases along the circuit of an exactly-one assignment, except at the exit of the last row – and at the loop of zero.

        Dependency graph
        source
        theorem DescriptiveComplexity.HamGadget.isCircuit_S {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} [Finite A] [Nonempty A] (hν : OneInProper ν) :
        IsCircuit (fun (u v : { v : Vtx A // Valid v }) => Arc ↑u ↑v) fun (u v : { v : Vtx A // Valid v }) => S ν ↑u ↑v

        The relation of an exactly-one assignment is a Hamilton circuit of the row graph.

        Dependency graph