Documentation

DescriptiveComplexity.Problems.Hamilton.CountingHardness

#Directed Hamilton Circuit is parsimoniously `#P`-complete #

DescriptiveComplexity.sharpDirHamCircuit_sharpP_parsimoniousComplete, by a relativized reduction from #1-in-SAT (DescriptiveComplexity.sharpOneInSat_rel_ordered_parsimonious_sharpDirHamCircuit).

The mathematics is in the three files before this one: the row graph of a CNF formula (DescriptiveComplexity.Problems.Hamilton.CountingGadget) has exactly the exactly-one models of the formula as Hamilton circuits (DescriptiveComplexity.HamGadget.modelEquiv). What is left is to draw that graph in the formula, first-order: a vertex is a tag and a pair of elements (DescriptiveComplexity.HamGadget.toVtx), the vertices that exist are cut out by the domain formula of a relativized interpretation (DescriptiveComplexity.HamGadget.domF), and an arc is a formula on two such pairs (DescriptiveComplexity.HamGadget.stepF). The interpreted universe is then the vertex type of the row graph, arcs included (DescriptiveComplexity.HamGadget.vtxEquiv, DescriptiveComplexity.HamGadget.dgArc_iff).

The reduction is relativized because a circuit spans the universe: a tagged pair that is no vertex would have to lie on every circuit. It is ordered because the rows are: the occurrences of a variable are laid out in the order of the instance, and so are the variables.

inductive DescriptiveComplexity.HamGadget.HTag :

Tags of the interpretation: the kinds of vertices of the row graph.

top : HTag
The entry of a row.
lft : HTag
The left end of a row.
rgt : HTag
The right end of a row.
pad0 : HTag
The first padding of a row.
ain (s : Bool) : HTag
The left vertex of an occurrence of sign s.
bout (s : Bool) : HTag
The right vertex of an occurrence of sign s.
pad (s : Bool) : HTag
The padding after an occurrence of sign s.
cls : HTag
A clause vertex.
zero : HTag
The vertex of a formula with no clause.

Instances For

Dependency graph

def DescriptiveComplexity.HamGadget.instDecidableEqHTag.decEq (x✝ x✝¹ : HTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.HamGadget.instDecidableEqHTag :

DecidableEq HTag

Equations

DescriptiveComplexity.HamGadget.instDecidableEqHTag = DescriptiveComplexity.HamGadget.instDecidableEqHTag.decEq

Dependency graph

instance DescriptiveComplexity.HamGadget.instFiniteHTag :

Dependency graph

def DescriptiveComplexity.HamGadget.toVtx {A : Type} :

HTag → A → A → Vtx A

The vertex a tagged pair stands for.

Equations

DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.top x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.top x✝¹
DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.lft x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.lft x✝¹
DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.rgt x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.rgt x✝¹
DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.pad0 x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.pad0 x✝¹
DescriptiveComplexity.HamGadget.toVtx (DescriptiveComplexity.HamGadget.HTag.ain s) x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.ain s x✝¹ x✝
DescriptiveComplexity.HamGadget.toVtx (DescriptiveComplexity.HamGadget.HTag.bout s) x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.bout s x✝¹ x✝
DescriptiveComplexity.HamGadget.toVtx (DescriptiveComplexity.HamGadget.HTag.pad s) x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.pad s x✝¹ x✝
DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.cls x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.cls x✝¹
DescriptiveComplexity.HamGadget.toVtx DescriptiveComplexity.HamGadget.HTag.zero x✝¹ x✝ = DescriptiveComplexity.HamGadget.Vtx.zero

Instances For

Dependency graph

The formulas #

noncomputable def DescriptiveComplexity.HamGadget.varF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

x is a variable of the formula, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.noClF {α : Type} :

SatOcc.satOrd.Formula α

There is no clause, as a formula.

Equations

DescriptiveComplexity.HamGadget.noClF = FirstOrder.Language.BoundedFormula.not (FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.SatOcc.clF (Sum.inr ())))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.botF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

x is the least element, as a formula.

Equations

DescriptiveComplexity.HamGadget.botF x = FirstOrder.Language.Formula.iAlls Unit (DescriptiveComplexity.leF (Sum.inl x) (Sum.inr ()))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.vFirstF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

DescriptiveComplexity.HamGadget.VFirst, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.vLastF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

DescriptiveComplexity.HamGadget.VLast, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.vStepF {α : Type} (x y : α) :

SatOcc.satOrd.Formula α

DescriptiveComplexity.HamGadget.VStep, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.nextVarF {α : Type} (x y : α) :

SatOcc.satOrd.Formula α

DescriptiveComplexity.HamGadget.NextVar, as a formula.

Equations

DescriptiveComplexity.HamGadget.nextVarF x y = DescriptiveComplexity.HamGadget.vStepF x y ⊔ DescriptiveComplexity.HamGadget.vLastF x ⊓ DescriptiveComplexity.HamGadget.vFirstF y

Instances For

Dependency graph

def DescriptiveComplexity.HamGadget.boolF {α : Type} (b : Bool) :

SatOcc.satOrd.Formula α

A sign condition, as a formula.

Equations

DescriptiveComplexity.HamGadget.boolF b = if b = true then ⊤ else ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.domF :

HTag → SatOcc.satOrd.Formula (Fin 2)

The domain formulas: which tagged pairs are vertices.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.stepF :

HTag → HTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The arc formulas, by tags: DescriptiveComplexity.HamGadget.Step, drawn. The free variable (i, j) is the j-th component of the i-th vertex.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.hamInterp :

RelFOInterpretation SatOcc.satOrd FirstOrder.Language.digraph HTag 2

The relativized interpretation drawing the row graph of a CNF formula.

Equations

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

Instances For

Dependency graph

Realization #

def DescriptiveComplexity.HamGadget.Dom {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

HTag → A → A → Prop

Which pairs of elements are vertices, by tag.

Equations

DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.top x✝¹ x✝ = (x✝¹ = x✝ ∧ DescriptiveComplexity.SatOccurs A x✝¹)
DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.lft x✝¹ x✝ = (x✝¹ = x✝ ∧ DescriptiveComplexity.SatOccurs A x✝¹)
DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.rgt x✝¹ x✝ = (x✝¹ = x✝ ∧ DescriptiveComplexity.SatOccurs A x✝¹)
DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.pad0 x✝¹ x✝ = (x✝¹ = x✝ ∧ DescriptiveComplexity.SatOccurs A x✝¹)
DescriptiveComplexity.HamGadget.Dom (DescriptiveComplexity.HamGadget.HTag.ain s) x✝¹ x✝ = DescriptiveComplexity.SatOcc.OccIn x✝ x✝¹ s
DescriptiveComplexity.HamGadget.Dom (DescriptiveComplexity.HamGadget.HTag.bout s) x✝¹ x✝ = DescriptiveComplexity.SatOcc.OccIn x✝ x✝¹ s
DescriptiveComplexity.HamGadget.Dom (DescriptiveComplexity.HamGadget.HTag.pad s) x✝¹ x✝ = DescriptiveComplexity.SatOcc.OccIn x✝ x✝¹ s
DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.cls x✝¹ x✝ = (x✝¹ = x✝ ∧ DescriptiveComplexity.SatOcc.IsCl x✝¹)
DescriptiveComplexity.HamGadget.Dom DescriptiveComplexity.HamGadget.HTag.zero x✝¹ x✝ = ((x✝¹ = x✝ ∧ IsBot x✝¹) ∧ ¬∃ (c : A), DescriptiveComplexity.SatOcc.IsCl c)

Instances For

Dependency graph

theorem DescriptiveComplexity.HamGadget.realize_domF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t : HTag} {w : Fin 2 → A} :

(domF t).Realize w ↔ Dom t (w 0) (w 1)

Dependency graph

The interpreted universe is the vertex type of the row graph #

theorem DescriptiveComplexity.HamGadget.valid_toVtx {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t : HTag} {x y : A} (h : Dom t x y) :

Valid (toVtx t x y)

Dependency graph

def DescriptiveComplexity.HamGadget.vtxOf {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : hamInterp.MapRel A) :

{ v : Vtx A // Valid v }

The vertex of a point of the interpreted universe.

Equations

DescriptiveComplexity.HamGadget.vtxOf p = ⟨DescriptiveComplexity.HamGadget.toVtx (↑p).1 ((↑p).2 0) ((↑p).2 1), ⋯⟩

Instances For

Dependency graph

theorem DescriptiveComplexity.HamGadget.vtxOf_injective {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

Function.Injective vtxOf

Dependency graph

theorem DescriptiveComplexity.HamGadget.vtxOf_surjective {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

Function.Surjective vtxOf

Dependency graph

noncomputable def DescriptiveComplexity.HamGadget.vtxEquiv (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

hamInterp.MapRel A ≃ { v : Vtx A // Valid v }

The interpreted universe is the vertex type of the row graph.

Equations

DescriptiveComplexity.HamGadget.vtxEquiv A = Equiv.ofBijective DescriptiveComplexity.HamGadget.vtxOf ⋯

Instances For

Dependency graph

theorem DescriptiveComplexity.HamGadget.dgArc_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p q : hamInterp.MapRel A) :

DGArc p q ↔ Arc ↑(vtxOf p) ↑(vtxOf q)

The interpreted arcs are the arcs of the row graph.

Dependency graph

theorem DescriptiveComplexity.HamGadget.sharpDirHamCircuit_mapRel (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

SharpDirHamCircuit.Count (hamInterp.MapRel A) = SharpOneInSAT.Count A

Correctness of the interpretation, for counting.

Dependency graph

noncomputable def DescriptiveComplexity.sharpOneInSat_rel_ordered_parsimonious_sharpDirHamCircuit :

RelOrderedParsimoniousReduction SharpOneInSAT SharpDirHamCircuit

#1-in-SAT reduces parsimoniously to #Directed Hamilton Circuit, by a relativized interpretation: the tagged pairs that are no vertex of the row graph are left out of the universe.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.sharpDirHamCircuit_sharpP_parsimoniousHard :

SharpP.ParsimoniousHard SharpDirHamCircuit

#Directed Hamilton Circuit is parsimoniously #P-hard.

Dependency graph

theorem DescriptiveComplexity.sharpDirHamCircuit_sharpP_parsimoniousComplete :

SharpP.ParsimoniousComplete SharpDirHamCircuit

#Directed Hamilton Circuit is parsimoniously #P-complete: counting the Hamilton circuits of a digraph. Registered in the Lax archive as Lax280166.DirHamCircuitComplete.sharpDirHamCircuit_sharpP_parsimoniousComplete.

Dependency graph

theorem DescriptiveComplexity.sharpDirHamCircuit_sharpP_complete :

SharpP.Complete SharpDirHamCircuit

SharpDirHamCircuit is #P-complete: parsimoniously, hence under subtractive reductions.

Dependency graph