[Rule] SteinerTree to SAT

[zazabap]

Source: SteinerTree
Target: SAT
Motivation: Encodes the Steiner Tree decision problem ("does a Steiner tree of cost $\leq W$ exist?") as a SAT formula, enabling SAT solver-based approaches for network design verification.
Reference: de Aragão & Werneck, 2002; general graph connectivity SAT encodings in Bayless et al., 2015

Reduction Algorithm

Notation:

• Source: undirected weighted graph $G = (V, E, w)$, terminals $T \subseteq V$, budget $W$, $n = |V|$, $m = |E|$
• Target: SAT formula in CNF

Decision version: Does there exist a Steiner tree with total weight $\leq W$?

Step 1 — Edge selection variables:

Boolean variable $y_e$ for each edge $e \in E$: true if edge $e$ is in the tree.

Step 2 — Reachability variables:

Pick a root terminal $r \in T$. For each non-root terminal $t \in T' = T \setminus {r}$ and each vertex $v \in V$, introduce boolean variable $R^t_v$: true if $v$ is reachable from $r$ via selected edges in the subproblem for terminal $t$.

Step 3 — Clauses:

1. Root reachability: $R^t_r = \text{true}$ for all $t \in T'$.

2. Terminal reachability: $R^t_t = \text{true}$ for all $t \in T'$.

3. Reachability propagation: If $R^t_v$ is true and edge $(v, u)$ is selected, then $R^t_u$ is true:
   $$\neg R^t_v \lor \neg y_{{v,u}} \lor R^t_u$$
   for each $t \in T'$, each vertex $v$, and each neighbor $u$ of $v$.

4. Reachability grounding: A non-root vertex can only be reachable if at least one neighbor is reachable and the connecting edge is selected:
   $$R^t_v \Rightarrow \bigvee_{u : {u,v} \in E} (R^t_u \wedge y_{{u,v}})$$
   for each $t \in T'$ and each $v \neq r$.

5. Budget constraint: At most $W$ total weight of edges can be selected. Encoded via a cardinality/pseudo-boolean constraint on the weighted sum $\sum_e w_e \cdot y_e \leq W$ (using standard totalizer or binary adder encoding).

Solution extraction: Edges with $y_e = \text{true}$ form the Steiner tree.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_variables	$m + n(k-1)$ (edge + reachability variables, plus budget encoding auxiliaries)
num_clauses	$O(m \cdot k + \text{budget encoding})$

Validation Method

Closed-loop testing: solve SteinerTree by brute-force, binary search on $W$ with the SAT oracle, and verify the optimal cost matches.

Example

Source: 5 vertices, 7 edges, terminals $T = {0, 2, 4}$, budget $W = 6$.

SAT encoding: root $r = 0$, non-root terminals ${2, 4}$.

• 7 edge variables ($y_0, \ldots, y_6$)
• 10 reachability variables ($R^t_v$ for $t \in {2,4}$, $v \in {0,1,2,3,4}$)
• Plus auxiliary variables for budget encoding

Key clauses (sample):

• $R^2_0 = \text{true}$ (root reachable for terminal 2)
• $R^2_2 = \text{true}$ (terminal 2 must be reached)
• $\neg R^2_0 \lor \neg y_{(0,1)} \lor R^2_1$ (if 0 reached and edge 0-1 selected, then 1 reached)

Satisfying assignment: $y_{(0,1)} = y_{(1,2)} = y_{(1,3)} = y_{(3,4)} = \text{true}$, all others false. Total weight $= 6 \leq W$. SAT.

[zazabap]

Withdrawing in favor of higher-impact reduction rules.