#Hamilton Circuit: counting the circuits of an undirected graph

The counting version of DescriptiveComplexity.HamCircuit: the number of Hamilton circuits of a graph, a circuit being its set of edges (DescriptiveComplexity.IsUCircuit) – the symmetric relation “x and y are consecutive” – and not one of its two orientations.

Membership

The certificate is still a linear order, and a circuit has 2n of them: n places to cut it and two directions to read it. The counting kernel (DescriptiveComplexity.sharpHamKernel) fixes both: the order starts at the least element of the instance, as for the directed problem, and of the two neighbours of that element on the circuit it goes first to the smaller one (DescriptiveComplexity.Oriented). Every circuit has exactly one such order: one exists because reversing an order reverses its cyclic successor (DescriptiveComplexity.cycSucc_reverse), and two of them with the same edges agree at the root by the orientation rule, hence everywhere, by induction along the circuit (DescriptiveComplexity.cycSucc_of_sym). Hence DescriptiveComplexity.sharpHamCircuit_mem_sharpP.

Parsimonious hardness is in DescriptiveComplexity.Problems.Hamilton.CountingUndirectedHardness.

def DescriptiveComplexity.IsUCircuit {A : Type} (R E : A → A → Prop) : Prop

The relation E is the edge set of a Hamilton circuit of R: the symmetric closure of a circuit of R.

Equations

• DescriptiveComplexity.IsUCircuit R E = ∃ (Nxt : A → A → Prop), DescriptiveComplexity.IsCircuit R Nxt ∧ ∀ (x y : A), E x y ↔ Nxt x y ∨ Nxt y x

theorem DescriptiveComplexity.IsUCircuit.of_equiv {A B : Type} (u : A ≃ B) {RA : A → A → Prop} {RB : B → B → Prop} (hR : ∀ (a a' : A), RA a a' ↔ RB (u a) (u a')) {E : A → A → Prop} (h : IsUCircuit RA E) : IsUCircuit RB fun (b b' : B) => E (u.symm b) (u.symm b')

Undirected circuits transport along an equivalence commuting with the relations.

def DescriptiveComplexity.ucircuitEquiv {A B : Type} (u : A ≃ B) {RA : A → A → Prop} {RB : B → B → Prop} (hR : ∀ (a a' : A), RA a a' ↔ RB (u a) (u a')) : { E : A → A → Prop // Finite A ∧ IsUCircuit RA E } ≃ { E : B → B → Prop // Finite B ∧ IsUCircuit RB E }

The undirected circuits of two relations an equivalence exchanges are in bijection.

Equations

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

One order per undirected circuit

def DescriptiveComplexity.Oriented {A : Type} [LE A] (C : A → A → Prop) : Prop

The orientation rule: from the least element, the circuit goes first to the smaller of its two neighbours.

Equations

• DescriptiveComplexity.Oriented C = ∀ (x y z : A), IsBot x → C x y → C z x → y ≤ z

theorem DescriptiveComplexity.cycSucc_of_sym {A : Type} [LinearOrder A] [Finite A] {Le Le' : A → A → Prop} (h : IsLinOrd Le) (h' : IsLinOrd Le') {a₀ : A} (ha₀ : IsBot a₀) (hsym : ∀ (x y : A), CycSucc Le x y ∨ CycSucc Le y x ↔ CycSucc Le' x y ∨ CycSucc Le' y x) (ho : Oriented (CycSucc Le)) (ho' : Oriented (CycSucc Le')) (x y : A) : CycSucc Le x y → CycSucc Le' x y

Two oriented cuts with the same edges have the same cyclic successor.

theorem DescriptiveComplexity.card_orientedTour_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (R : A → A → Prop) (hRsym : ∀ (x y : A), R x y → R y x) : Nat.card { Le : A → A → Prop // IsLinOrd Le ∧ (∀ (x y : A), SuccOf Le x y → R x y) ∧ (∀ (x y : A), (∀ (z : A), Le x z) → (∀ (z : A), Le z y) → R y x) ∧ (∀ (x : A), IsBot x → ∀ (y : A), Le x y) ∧ Oriented (CycSucc Le) } = Nat.card { E : A → A → Prop // IsUCircuit R E }

Undirected circuits are the oriented orders that start at the least element, bijectively.

The counting problem

def DescriptiveComplexity.UCircuit (A : Type) [FirstOrder.Language.digraph.Structure A] (E : A → A → Prop) : Prop

The relation E is the edge set of a Hamilton circuit of a finite graph.

Equations

• DescriptiveComplexity.UCircuit A E = (Finite A ∧ DescriptiveComplexity.IsUCircuit (fun (x y : A) => DescriptiveComplexity.DGEdge x y) E)

noncomputable def DescriptiveComplexity.SharpHamCircuit : CountingProblem FirstOrder.Language.digraph

#Hamilton Circuit: the number of Hamilton circuits of a graph, a circuit being its set of edges.

Equations

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

theorem DescriptiveComplexity.sharpHamCircuit_support_iff (A : Type) [FirstOrder.Language.digraph.Structure A] [Finite A] : SharpHamCircuit.support.Holds A ↔ HamCircuit.Holds A

The support of #Hamilton Circuit is Hamilton Circuit. Registered in the Lax archive as Lax280166.HamCircuitComplete.sharpHamCircuit_support_iff.

Membership

noncomputable def DescriptiveComplexity.cycF {α : Type} (x y : α) : dhcLang.Formula α

The cyclic successor of the guessed order, as a formula.

Equations

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

theorem DescriptiveComplexity.sharpHamCircuit_mem_sharpP : SharpP.Mem SharpHamCircuit

#Hamilton Circuit is in #P: a circuit has exactly one oriented cut at the least element of the instance.