Steiner Tree is NP-complete

Umbrella file for DescriptiveComplexity.SteinerTree, the node-weighted Steiner tree with unit weights (defined in DescriptiveComplexity.Problems.Steiner.Defs), deriving NP-completeness from

• DescriptiveComplexity.steinerTree_sigmaSODefinable (DescriptiveComplexity.Problems.Steiner.Membership): membership, by guessing the chosen set, a root, an order certifying connectivity, and the threshold injection;
• DescriptiveComplexity.vertexCover_ordered_fo_reduction_steinerTree (DescriptiveComplexity.Problems.Steiner.Reductions): hardness, from the NP-hardness of Vertex Cover (DescriptiveComplexity.Problems.CliqueFamily), and so ultimately from the Cook–Levin theorem, with no machine model anywhere.

As with any complexity-theoretic statement, these results are about finite structures only (DescriptiveComplexity.ComplexityClass.mem_congr_finite/hard_congr_finite).

theorem DescriptiveComplexity.steinerTree_mem_NP : NP.Mem SteinerTree

Steiner Tree is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.steinerTree_NP_hard : NP.Hard SteinerTree

Steiner Tree is NP-hard: Vertex Cover, which is NP-hard, ordered-FO-reduces to it by the edge-incidence structure with a root.

theorem DescriptiveComplexity.steinerTree_NP_complete : NP.Complete SteinerTree

Steiner Tree is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

The edge-weighted variant

theorem DescriptiveComplexity.edgeSteinerTree_mem_NP : NP.Mem EdgeSteinerTree

The edge-weighted Steiner Tree is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.edgeSteinerTree_NP_hard : NP.Hard EdgeSteinerTree

The edge-weighted Steiner Tree is NP-hard: Vertex Cover, which is NP-hard, ordered-FO-reduces to it.

theorem DescriptiveComplexity.edgeSteinerTree_NP_complete : NP.Complete EdgeSteinerTree

The edge-weighted Steiner Tree is NP-complete – Karp's original reading of the problem.