Skip to content

[Rule] RegisterSufficiency to ILP #782

@isPANN

Description

@isPANN

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:

  1. 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.

  2. Each vertex evaluated exactly once: For each i ∈ {1, ..., n}:
    ∑_{j=1}^{n} x_{ij} = 1

  3. Each time step evaluates exactly one vertex: For each j ∈ {1, ..., n}:
    ∑_{i=1}^{n} x_{ij} = 1

  4. 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

  5. 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}
  6. Register bound: For each j ∈ {1, ..., n}:
    r_j ≤ K

  7. 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).

  8. 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    ruleA new reduction rule to be added.

    Type

    No type

    Projects

    Status

    Backlog

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions