#Steiner Tree: counting the Steiner sets of the threshold size

The counting version of DescriptiveComplexity.SteinerTree, the node-weighted problem: the number of connected sets of vertices containing every terminal and using exactly as many non-terminals as the marked set has elements (DescriptiveComplexity.SteinerOfSize).

The certificate of connectivity

Connectivity is not first-order. The Σ₁ definition of the decision problem certifies it by a root and a strict order in which every other chosen vertex has a chosen neighbour below it (DescriptiveComplexity.connectedOn_iff_exists_root), and there are many such orders. The counting kernel uses the order of the instance as a clock: a binary relation R x t, “x is reached from the least chosen vertex in at most as many steps as t has predecessors”, which is determined step by step along the order (DescriptiveComplexity.IsReachClock, DescriptiveComplexity.IsReachClock.eq_clockOf) – it is DescriptiveComplexity.reachIn at the rank of t. The set is connected iff every chosen vertex is reached by the last tick (DescriptiveComplexity.clockOf_top_iff_connectedOn), a path needing fewer steps than there are vertices (DescriptiveComplexity.reachIn_card).

This kernel reads the order, and defines the same count whatever the order: the clock changes with it, the set of solutions does not. Hence DescriptiveComplexity.sharpSteinerTree_mem_sharpP, by DescriptiveComplexity.sharpPDefinable_of_sized_ordered.

As for Set Cover, the support is “some Steiner set uses exactly the threshold number of non-terminals”, not the decision problem: a Steiner set can only be extended by a neighbour.

Reachability in a bounded number of steps

theorem DescriptiveComplexity.reachIn_card {A : Type} [Finite A] {R : A → A → Prop} {r x : A} (h : Relation.ReflTransGen R r x) : reachIn R (Nat.card A - 1) r x

A path needs fewer steps than there are vertices.

The clock

def DescriptiveComplexity.IsReachClock {A : Type} [LE A] (Lk : A → A → Prop) (S : A → Prop) (R : A → A → Prop) : Prop

The relation R x t is a reachability clock for the links Lk inside S: at the first tick it holds of the least element of S, and at each later tick of what the previous tick reached, and of its Lk-successors.

Equations

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

def DescriptiveComplexity.clockOf {A : Type} [LinearOrder A] (Lk : A → A → Prop) (S : A → Prop) (x t : A) : Prop

The clock: reachability from the least element of S, in as many steps as the tick has predecessors.

Equations

• DescriptiveComplexity.clockOf Lk S x t = ∃ (r : A), (S r ∧ ∀ (y : A), S y → r ≤ y) ∧ DescriptiveComplexity.reachIn Lk (DescriptiveComplexity.orank t) r x

theorem DescriptiveComplexity.clockOf_iff {A : Type} [LinearOrder A] {Lk : A → A → Prop} {S : A → Prop} {x t : A} {k : ℕ} (hk : orank t = k) : clockOf Lk S x t ↔ ∃ (r : A), (S r ∧ ∀ (y : A), S y → r ≤ y) ∧ reachIn Lk k r x

theorem DescriptiveComplexity.IsReachClock.eq_clockOf {A : Type} [LinearOrder A] [Finite A] {Lk : A → A → Prop} {S : A → Prop} {R : A → A → Prop} (h : IsReachClock Lk S R) : R = clockOf Lk S

The clock is unique: it is determined tick by tick.

theorem DescriptiveComplexity.clockOf_top_iff_connectedOn {A : Type} [LinearOrder A] [Finite A] (Adjp : A → A → Prop) (S : A → Prop) : (∀ (x t : A), (∀ (z : A), z ≤ t) → S x → clockOf (Link Adjp S) S x t) ↔ ConnectedOn Adjp S

The set is connected iff the clock reaches all of it by the last tick.

The counting problem

def DescriptiveComplexity.SteinerOfSizeOn {A : Type} (Adjp : A → A → Prop) (Term Kp S : A → Prop) : Prop

The set S contains every terminal, is connected, and has exactly as many non-terminals as the Kp-marked set has elements.

Equations

• DescriptiveComplexity.SteinerOfSizeOn Adjp Term Kp S = ((∀ (x : A), Term x → S x) ∧ DescriptiveComplexity.ConnectedOn Adjp S ∧ {x : A | S x ∧ ¬Term x}.ncard = {x : A | Kp x}.ncard)

def DescriptiveComplexity.steinerOfSizeEquiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {TermB KB : B → Prop} {AdjA : A → A → Prop} {TermA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hterm : ∀ (b : B), TermB b ↔ TermA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) : { S : B → Prop // Finite B ∧ SteinerOfSizeOn AdjB TermB KB S } ≃ { S : A → Prop // Finite A ∧ SteinerOfSizeOn AdjA TermA KA S }

The Steiner sets of the threshold size transport along an equivalence commuting with the three predicates.

Equations

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

def DescriptiveComplexity.SteinerOfSize (A : Type) [FirstOrder.Language.steinerGraph.Structure A] (S : A → Prop) : Prop

The set S is a connected set containing every terminal and using exactly as many non-terminals as the marked set has elements, in a finite graph.

Equations

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

noncomputable def DescriptiveComplexity.SharpSteinerTree : CountingProblem FirstOrder.Language.steinerGraph

#Steiner Tree: the number of connected sets containing every terminal and using exactly as many non-terminals as the marked set has elements.

Equations

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

theorem DescriptiveComplexity.sharpSteinerTree_support_iff (A : Type) [FirstOrder.Language.steinerGraph.Structure A] [Finite A] : SharpSteinerTree.support.Holds A ↔ ∃ (S : A → Prop), SteinerOfSize A S

The support of #Steiner Tree: some Steiner set uses exactly the threshold number of non-terminals. Registered in the Lax archive as Lax280166.SteinerTreeComplete.sharpSteinerTree_support_iff.

theorem DescriptiveComplexity.steinerTree_of_sharpSteinerTree_support (A : Type) [FirstOrder.Language.steinerGraph.Structure A] [Finite A] (h : SharpSteinerTree.support.Holds A) : SteinerTree.Holds A

The support of #Steiner Tree implies Steiner Tree. Registered in the Lax archive as Lax280166.SteinerTreeComplete.steinerTree_of_sharpSteinerTree_support.

Membership

@[reducible, inline]

abbrev DescriptiveComplexity.scSelSym : steinerCountLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.scSelSym = Sum.inr DescriptiveComplexity.scSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.scMarkedSym : steinerCountLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.scMarkedSym = Sum.inl FirstOrder.Language.stMarked

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSteinerCountBlockIx : DecidableEq SteinerCountBlockIx

Equations

• DescriptiveComplexity.instDecidableEqSteinerCountBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DescriptiveComplexity.steinerCountBlock : SOBlock

The block of the counting definition of Steiner Tree: the chosen set, its non-terminals, and the reachability clock.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.scReachSym : steinerCountLang.Relations 2

The reach symbol over the sum.

Equations

• DescriptiveComplexity.scReachSym = Sum.inr DescriptiveComplexity.scReachRel

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSteinerCountBlockIx : Fintype SteinerCountBlockIx

Equations

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

inductive DescriptiveComplexity.SteinerCountBlockIx : Type

The relation variables of the block.

• sel : SteinerCountBlockIx

  The chosen set.

• non : SteinerCountBlockIx

  The non-terminals of the chosen set: the set whose size is the budget.

• reach : SteinerCountBlockIx

  The reachability clock.

def DescriptiveComplexity.scNonRel : steinerCountBlock.lang.Relations 1

The non relation variable.

Equations

• DescriptiveComplexity.scNonRel = ⟨DescriptiveComplexity.SteinerCountBlockIx.non, DescriptiveComplexity.scNonRel._proof_1⟩

def DescriptiveComplexity.scSelRel : steinerCountBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.scSelRel = ⟨DescriptiveComplexity.SteinerCountBlockIx.sel, DescriptiveComplexity.scSelRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.steinerCountLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.steinerCountLang = FirstOrder.Language.steinerGraph.sum DescriptiveComplexity.steinerCountBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.scTerminalSym : steinerCountLang.Relations 1

The terminal symbol over the sum.

Equations

• DescriptiveComplexity.scTerminalSym = Sum.inl FirstOrder.Language.stTerminal

@[reducible, inline]

abbrev DescriptiveComplexity.scNonSym : steinerCountLang.Relations 1

The non symbol over the sum.

Equations

• DescriptiveComplexity.scNonSym = Sum.inr DescriptiveComplexity.scNonRel

def DescriptiveComplexity.scReachRel : steinerCountBlock.lang.Relations 2

The reach relation variable.

Equations

• DescriptiveComplexity.scReachRel = ⟨DescriptiveComplexity.SteinerCountBlockIx.reach, DescriptiveComplexity.scReachRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.scAdjSym : steinerCountLang.Relations 2

The adj symbol over the sum.

Equations

• DescriptiveComplexity.scAdjSym = Sum.inl FirstOrder.Language.stAdj

@[reducible, inline]

abbrev DescriptiveComplexity.stoLang : FirstOrder.Language

The vocabulary of the counting kernel: the ordered graph with terminals, expanded by the block.

Equations

• DescriptiveComplexity.stoLang = (FirstOrder.Language.steinerGraph.sum FirstOrder.Language.order).sum DescriptiveComplexity.steinerCountBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.stoAdjSym : stoLang.Relations 2

The adj symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoAdjSym = Sum.inl (Sum.inl FirstOrder.Language.stAdj)

@[reducible, inline]

abbrev DescriptiveComplexity.stoTermSym : stoLang.Relations 1

The terminal symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoTermSym = Sum.inl (Sum.inl FirstOrder.Language.stTerminal)

@[reducible, inline]

abbrev DescriptiveComplexity.stoLeSym : stoLang.Relations 2

The order symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoLeSym = Sum.inl (Sum.inr FirstOrder.Language.leSymb)

@[reducible, inline]

abbrev DescriptiveComplexity.stoSelSym : stoLang.Relations 1

The sel symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoSelSym = Sum.inr DescriptiveComplexity.scSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.stoNonSym : stoLang.Relations 1

The non symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoNonSym = Sum.inr DescriptiveComplexity.scNonRel

@[reducible, inline]

abbrev DescriptiveComplexity.stoReachSym : stoLang.Relations 2

The reach symbol over the ordered sum.

Equations

• DescriptiveComplexity.stoReachSym = Sum.inr DescriptiveComplexity.scReachRel

theorem DescriptiveComplexity.sharpSteinerTree_mem_sharpP : SharpP.Mem SharpSteinerTree

#Steiner Tree is in #P: the budget is certified by the monotone bijection with the marked set, and connectivity by the reachability clock.