Motivation
RegisterSufficiency is a feasibility problem (decision: can the DAG be computed with ≤ K registers?). A direct ILP formulation enables witness-capable solving via the existing ILP solver infrastructure. The ILP encoding uses binary assignment variables to model the evaluation ordering and register tracking constraints.
Reference: Garey & Johnson, Computers and Intractability, A11 PO1; ILP formulation follows standard scheduling-as-assignment encoding.
Source
RegisterSufficiency
Target
ILP
Reduction Algorithm
Given a RegisterSufficiency instance with DAG G = (V, A), n = |V|, and bound K:
-
Assignment variables: For each vertex v_i ∈ V and each time step j ∈ {1, ..., n}, create binary variable x_{ij} ∈ {0, 1}, where x_{ij} = 1 means vertex v_i is evaluated at step j.
-
Each vertex evaluated exactly once: For each i ∈ {1, ..., n}:
∑_{j=1}^{n} x_{ij} = 1
-
Each time step evaluates exactly one vertex: For each j ∈ {1, ..., n}:
∑_{i=1}^{n} x_{ij} = 1
-
Dependency constraints: For each arc (v_i, v_k) ∈ A (v_i depends on v_k, i.e., v_k must be evaluated before v_i): define pos(v_i) = ∑_{j=1}^{n} j · x_{ij}. Require pos(v_k) < pos(v_i), which linearizes to:
∑_{j=1}^{n} j · x_{kj} ≤ ∑_{j=1}^{n} j · x_{ij} − 1
-
Register tracking: For each time step j ∈ {1, ..., n}, define a register-count variable r_j representing the number of values alive at step j. A value v_k is alive at step j if v_k has been evaluated at or before step j, and at least one vertex that depends on v_k has not yet been evaluated by step j. This can be linearized with auxiliary variables:
- Let alive_{kj} ∈ {0, 1} = 1 iff v_k is alive at step j
- alive_{kj} = 1 iff (pos(v_k) ≤ j) ∧ (∃ (v_i, v_k) ∈ A : pos(v_i) > j)
- r_j = ∑_{k=1}^{n} alive_{kj}
-
Register bound: For each j ∈ {1, ..., n}:
r_j ≤ K
-
Feasibility objective: The ILP is a feasibility problem — any solution satisfying all constraints is a valid witness. Set the objective to a constant (e.g., minimize 0).
-
Solution extraction: From a feasible solution, read pos(v_i) = ∑_j j · x_{ij} for each vertex to recover the evaluation ordering.
Size Overhead
Symbols:
- n = |V| =
num_vertices of source
- e = |A| =
num_arcs of source
| Target metric (code name) |
Expression |
num_variables |
n^2 + n^2 + n (assignment x_{ij} + alive_{kj} + register r_j) |
num_constraints |
2n + e + n^2 + n (assignment + dependency + alive linearization + bound) |
Validation Method
Closed-loop test: construct a small DAG, reduce to ILP, solve with ILP solver, extract the evaluation ordering, verify it uses ≤ K registers via brute-force simulation.
Example
Source (RegisterSufficiency):
DAG with V = {v_1, ..., v_7}, arcs: (v_3,v_1), (v_3,v_2), (v_4,v_2), (v_5,v_3), (v_5,v_4), (v_6,v_1), (v_7,v_5), (v_7,v_6). K = 3.
Target (ILP):
- 7×7 = 49 assignment variables x_{ij}, 49 alive variables alive_{kj}, 7 register variables r_j → 105 variables total
- 14 assignment constraints + 8 dependency constraints + ~49 alive linearization constraints + 7 register bound constraints
- Feasibility: any solution gives a valid 3-register evaluation ordering
Expected: Feasible. One witness ordering: v_1, v_2, v_3, v_4, v_6, v_5, v_7 (max registers = 3).
References
- Garey & Johnson, Computers and Intractability, A11 PO1
- Sethi, R. (1975). "Complete Register Allocation Problems." SIAM J. Comput. 4(3):226-248.
Motivation
RegisterSufficiency is a feasibility problem (decision: can the DAG be computed with ≤ K registers?). A direct ILP formulation enables witness-capable solving via the existing ILP solver infrastructure. The ILP encoding uses binary assignment variables to model the evaluation ordering and register tracking constraints.
Reference: Garey & Johnson, Computers and Intractability, A11 PO1; ILP formulation follows standard scheduling-as-assignment encoding.
Source
RegisterSufficiencyTarget
ILPReduction Algorithm
Given a RegisterSufficiency instance with DAG G = (V, A), n = |V|, and bound K:
Assignment variables: For each vertex v_i ∈ V and each time step j ∈ {1, ..., n}, create binary variable x_{ij} ∈ {0, 1}, where x_{ij} = 1 means vertex v_i is evaluated at step j.
Each vertex evaluated exactly once: For each i ∈ {1, ..., n}:
∑_{j=1}^{n} x_{ij} = 1
Each time step evaluates exactly one vertex: For each j ∈ {1, ..., n}:
∑_{i=1}^{n} x_{ij} = 1
Dependency constraints: For each arc (v_i, v_k) ∈ A (v_i depends on v_k, i.e., v_k must be evaluated before v_i): define pos(v_i) = ∑_{j=1}^{n} j · x_{ij}. Require pos(v_k) < pos(v_i), which linearizes to:
∑_{j=1}^{n} j · x_{kj} ≤ ∑_{j=1}^{n} j · x_{ij} − 1
Register tracking: For each time step j ∈ {1, ..., n}, define a register-count variable r_j representing the number of values alive at step j. A value v_k is alive at step j if v_k has been evaluated at or before step j, and at least one vertex that depends on v_k has not yet been evaluated by step j. This can be linearized with auxiliary variables:
Register bound: For each j ∈ {1, ..., n}:
r_j ≤ K
Feasibility objective: The ILP is a feasibility problem — any solution satisfying all constraints is a valid witness. Set the objective to a constant (e.g., minimize 0).
Solution extraction: From a feasible solution, read pos(v_i) = ∑_j j · x_{ij} for each vertex to recover the evaluation ordering.
Size Overhead
Symbols:
num_verticesof sourcenum_arcsof sourcenum_variablesnum_constraintsValidation Method
Closed-loop test: construct a small DAG, reduce to ILP, solve with ILP solver, extract the evaluation ordering, verify it uses ≤ K registers via brute-force simulation.
Example
Source (RegisterSufficiency):
DAG with V = {v_1, ..., v_7}, arcs: (v_3,v_1), (v_3,v_2), (v_4,v_2), (v_5,v_3), (v_5,v_4), (v_6,v_1), (v_7,v_5), (v_7,v_6). K = 3.
Target (ILP):
Expected: Feasible. One witness ordering: v_1, v_2, v_3, v_4, v_6, v_5, v_7 (max registers = 3).
References