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:
-
Root reachability: $R^t_r = \text{true}$ for all $t \in T'$.
-
Terminal reachability: $R^t_t = \text{true}$ for all $t \in T'$.
-
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$.
-
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$.
-
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.
Source: SteinerTree$\leq W$ exist?") as a SAT formula, enabling SAT solver-based approaches for network design verification.
Target: SAT
Motivation: Encodes the Steiner Tree decision problem ("does a Steiner tree of cost
Reference: de Aragão & Werneck, 2002; general graph connectivity SAT encodings in Bayless et al., 2015
Reduction Algorithm
Notation:
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:
Root reachability:$R^t_r = \text{true}$ for all $t \in T'$ .
Terminal reachability:$R^t_t = \text{true}$ for all $t \in T'$ .
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$$ $t \in T'$ , each vertex $v$ , and each neighbor $u$ of $v$ .
for each
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}})$$ $t \in T'$ and each $v \neq r$ .
for each
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
num_variablesnum_clausesValidation 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}$ .
Key clauses (sample):
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.