Documentation

DescriptiveComplexity.Problems.Steiner.CountingHardness

#Steiner Tree is parsimoniously #P-complete #

DescriptiveComplexity.sharpSteinerTree_sharpP_parsimoniousComplete, by the reduction from Vertex Cover of DescriptiveComplexity.Problems.Steiner.Reductions, which is parsimonious as it stands (DescriptiveComplexity.sharpVertexCover_ordered_parsimonious_sharpSteinerTree).

In the incidence structure of a graph the terminals are the edges and the root, and the only other points with a neighbour are the vertices (DescriptiveComplexity.steiner_nonterminal_shape). So a connected set containing the terminals is the terminals together with a set of vertices, which covers every edge, and any cover will do: the Steiner sets using a given number of non-terminals are the vertex covers of that size, bijectively. A superset of a solution is a solution on both sides here, and the two paddings are the same vertices.

source
theorem DescriptiveComplexity.steiner_nonterminal_shape {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {p q : steinerInterp.Map A} (h : STAdj p q ∨ STAdj q p) (hp : ¬STTerminal p) :
∃ (v : A), p = vPt v

A point of the incidence structure with a neighbour is a terminal or a vertex.

Dependency graph
source
theorem DescriptiveComplexity.sharpSteinerTree_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
SharpSteinerTree.Count (steinerInterp.Map A) = SharpVertexCover.Count A

Correctness of the interpretation, for counting.

Dependency graph
source
noncomputable def DescriptiveComplexity.sharpVertexCover_ordered_parsimonious_sharpSteinerTree :
OrderedParsimoniousReduction SharpVertexCover SharpSteinerTree

#Vertex Cover reduces parsimoniously to #Steiner Tree, by the incidence structure of the graph with a root.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.sharpSteinerTree_sharpP_parsimoniousHard :
    SharpP.ParsimoniousHard SharpSteinerTree

    #Steiner Tree is parsimoniously #P-hard.

    Dependency graph
    source
    theorem DescriptiveComplexity.sharpSteinerTree_sharpP_parsimoniousComplete :
    SharpP.ParsimoniousComplete SharpSteinerTree

    #Steiner Tree is parsimoniously #P-complete, counting the Steiner sets using exactly the threshold number of non-terminals. Registered in the Lax archive as Lax280166.SteinerTreeComplete.sharpSteinerTree_sharpP_parsimoniousComplete.

    Dependency graph
    source
    theorem DescriptiveComplexity.sharpSteinerTree_sharpP_complete :
    SharpP.Complete SharpSteinerTree

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

    Dependency graph