diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index d5909d575..1a84950e9 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -11488,6 +11488,8 @@ the displayed rule, extracted from the corresponding `pred path` entry.
 )[
   This $O(n^2 m)$ reduction constructs an ILP with binary assignment variables $x_(t,p)$, integer completion-time variables $C_t$, and binary ordering variables $y_(i,j)$ for task pairs. Big-M disjunctive constraints enforce non-overlapping execution on shared processors.
 ][
+  _Numeric magnitude._ Let $h$ be `max_processing_time_bits` and $n$ the task count. With $L$ the total processing time, the disjunction rows have magnitudes at most $3L$, and variable endpoints at most $L$. Target `max_constraint_magnitude_bits` is at most $h+n+2$. Objective weights need no parameter.
+
   _Construction._ Let $n = |T|$ and $m$ be the number of processors. Create $n m$ binary assignment variables $x_(t,p) in {0, 1}$ (task $t$ on processor $p$), $n$ integer completion-time variables $C_t$, and $n(n-1)/2$ binary ordering variables $y_(i,j)$ for $i < j$. The constraints are:
   (1) Assignment: $sum_p x_(t,p) = 1$ for each $t$.
   (2) Completion bounds: $C_t >= ell(t)$ for each $t$.
@@ -11575,6 +11577,8 @@ the displayed rule, extracted from the corresponding `pred path` entry.
 )[
   The radius-threshold relation between centers and dominating sets @hochbaumshmoys1985 is extended here to all signed source bounds using two mandatory isolated centers. This $O(n+m+1)$ construction preserves the existing endpoint variants.
 ][
+  _Numeric magnitude._ Unit vertex weights and edge lengths give target `max_numeric_magnitude_bits` exactly $1$.
+
   _Construction._ For source graph $G=(V,E)$ with $n$ vertices and integer bound $K$, set $q=max(-1,min(K,n))$. Add isolated vertices $a=n$ and $b=n+1$, leaving every original edge record unchanged. Give all vertices and edges unit weights and lengths, and require exactly $k=q+2$ centers. Then $1<=k<=n+2$ for every input, including an empty graph.
 
   _Correctness._ Every finite target placement must select both isolated vertices. If a source dominating set $D$ has $|D|<=K$, then $q>=0$ and $|D|<=q<=n$. Extend $D$ to $q$ original vertices and add $a,b$. This placement has $k$ centers and radius at most $1$, proving the forward direction. Conversely, a target placement of radius at most $1$ selects both isolates and exactly $q$ original vertices. Each original vertex is within one original edge of a selected vertex, so those $q<=K$ vertices dominate $G$. For $K<0$, $k=1$ cannot cover both isolates and the target has no finite placement. For $n=0,K>=0$, the two isolates form a radius-zero placement. Loops and repeated edges preserve this reasoning.
@@ -13258,6 +13262,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("MultipleChoiceBranching", "ILP")[
   A topological-order formulation makes the branching acyclicity condition linear while retaining the source indegree, partition, and weight inequalities directly.
 ][
+  _Numeric magnitude._ Let $h$ be `max_weight_bits`, covering signed arc weights and the threshold, and $n$ the vertex count. Order constraints introduce magnitudes at most $n$, so target `max_constraint_magnitude_bits` is at most $h+n$.
+
   _Construction._ For every arc $a$ introduce a nonnegative integer $x_a <= 1$, and for every vertex $v$ introduce an integer order $0 <= p_v <= n-1$. Add $sum_(a in A_i)x_a <= 1$ for each partition group, $sum_(a in delta^-(v))x_a <= 1$ for each vertex, and $sum_a w_a x_a >= K$. For every arc $a=(u,v)$ add $p_u-p_v+n x_a <= n-1$. The target has exactly $m+n$ variables and $2m+2n+g+1$ constraints for $g$ partition groups.
 
   _Correctness._ A source branching admits a topological order, which satisfies the order rows. Conversely, selecting $(u,v)$ forces $p_v >= p_u+1$, so selected arcs cannot contain a directed cycle. All remaining source conditions are represented verbatim by their corresponding rows.
@@ -13808,6 +13814,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   @lawler1978 This $O(n + m)$ reduction turns each vertex into a unit-length job, each edge into a zero-length job, and uses precedences so that every edge job completes exactly when its later endpoint does. The weighted completion-time objective then equals the linear-arrangement objective plus the fixed shift $d_"max" n (n + 1) / 2$.
 ][
+  _Numeric magnitude._ Processing lengths are zero or one, so target `max_processing_time_bits` is exactly $1$.
+
   _Construction._ Let the source instance be an undirected graph $G = (V, E)$ with $n = |V|$, $m = |E|$, and maximum degree $d_"max" = max_(v in V) deg(v)$. For each vertex $v in V$, create a job $J_v$ of length 1 and weight $d_"max" - deg(v)$. For each edge $e = {u, v} in E$, create a job $J_e$ of length 0 and weight 2. Add the precedence constraints $J_u prec.eq J_e$ and $J_v prec.eq J_e$ for every edge job $J_e$. There are no other precedences, so the target has $n + m$ jobs and $2m$ precedence arcs.
 
   _Correctness._ Write the source arrangement as a bijection $pi : V -> {0, dots, n - 1}$. Schedule the vertex jobs in increasing $pi$-order, so $J_v$ completes at time $C_v = pi(v) + 1$. Because $J_e$ has length 0 and must follow both endpoints, edge job $J_{ {u, v} }$ completes at time $max(pi(u), pi(v)) + 1$. The total weighted completion time is
@@ -13857,6 +13865,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("SequencingToMinimizeWeightedCompletionTime", "ILP")[
   Completion times are natural integer variables, precedence constraints compare those completion times directly, and one binary order variable per task pair enforces that a single machine cannot overlap two jobs.
 ][
+  _Numeric magnitude._ Let $h$ be `max_processing_time_bits` and $n$ the task count. Constraint magnitudes and completion-variable bounds are at most the total processing time (or unit constants), giving target `max_constraint_magnitude_bits` at most $h+n$. Objective weights need no parameter.
+
   _Construction._ For each task $j$, introduce an integer completion-time variable $C_j$. For each unordered pair $i < j$, introduce a binary order variable $y_(i j)$ with $y_(i j) = 1$ meaning task $i$ finishes before task $j$. Let $M = sum_h l_h$.
 
   _Bounds._ $l_j <= C_j <= M$ for every task $j$, and $y_(i j) in {0, 1}$.
@@ -14681,6 +14691,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("PartiallyOrderedKnapsack", "ILP")[
   Standard knapsack with precedence constraints: item $b$ can only be selected if item $a$ is also selected for each precedence $(a, b)$.
 ][
+  _Numeric magnitude._ Let $h$ be `max_weight_bits`, covering item weights and capacity. The capacity row and unit precedence rows give target `max_constraint_magnitude_bits` exactly $h$; item values occur only in the objective.
+
   _Construction._ Variables: $x_i in {0, 1}$ per item. The ILP is:
   $
     max quad & sum_i v_i x_i \
@@ -14713,6 +14725,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("ShortestWeightConstrainedPath", "ILP")[
   Find a minimum-length $s$-$t$ path subject to a weight budget, using directed arc variables with MTZ ordering $o_v - o_u >= 1 - M (1 - a_(u,v))$ on selected arcs to prevent subtours.
 ][
+  _Numeric magnitude._ Let $h$ be `max_weight_bits`, covering edge weights and the weight bound, and $n$ the vertex count. These numeric inputs and the order-variable bounds give target `max_constraint_magnitude_bits` at most $h+n$. Objective edge lengths require no additional parameter.
+
   _Construction._ Let $A$ contain both orientations of every undirected edge and let $M = n$. Variables: binary $a_(u,v) in {0, 1}$ for each directed arc $(u, v) in A$, plus integer $o_v in {0, dots, n-1}$ per vertex. The ILP is:
   $
     "minimize" quad & sum_((u,v) in A) l_(u,v) a_(u,v) \
@@ -14768,6 +14782,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("MinMaxMulticenter", "ILP")[
   Select $k$ centers minimizing the maximum weighted distance from any vertex to its assigned center.
 ][
+  _Numeric magnitude._ Let $h$ be `max_numeric_magnitude_bits`, covering vertex weights and edge lengths, and $n$ the vertex count. A shortest simple path uses at most $n-1$ edges. Multiplying its length by a vertex weight gives a magnitude below $n 2^(2h)$, so target `max_constraint_magnitude_bits` is at most $2h+n$.
+
   _Construction._ Same assignment structure as MinimumSumMulticenter (binary $x_j$, $y_(i,j)$), plus an integer variable $z$. The ILP is:
   $
     "minimize" quad & z \
@@ -14796,12 +14812,16 @@ The following reductions to Integer Linear Programming are straightforward formu
 
   _Correctness._ One-hot constraints ensure each task is assigned to exactly one processor; load constraints enforce the deadline on every processor.
 
+  _Numeric magnitude._ Let $h >= 1$ be the smallest integer such that every task length and the deadline are strictly below $2^h$. At least one processor is present, so the load rows copy all these numbers. All remaining coefficients, right-hand sides, and Boolean endpoints have magnitude at most one. Thus the target's `max_constraint_magnitude_bits` equals the source's `max_numeric_magnitude_bits`, including instances with no tasks.
+
   _Solution extraction._ Task $j$ goes to processor $arg max_p x_(j,p)$.
 ]
 
 #reduction-rule("CapacityAssignment", "ILP")[
   Assign a capacity level to each link to minimize total cost subject to a delay budget.
 ][
+  _Numeric magnitude._ Let $h$ be `max_delay_bits`, covering all delays and the delay budget with absolute values strictly below $2^h$. These values, together with unit assignment rows, give target `max_constraint_magnitude_bits` exactly $h$. Costs occur only in the objective.
+
   _Construction._ Variables: binary $x_(l,c)$ (link $l$ gets capacity $c$), one-hot per link. The ILP is:
   $
     "minimize" quad & sum_(l,c) "cost"[l][c] x_(l,c) \
@@ -14889,6 +14909,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   This $O(n + m)$ parameter-setting reduction (Hadlock, 1974; Garey and Johnson @garey1979[ND10, p.~208]) constructs a Bounded Component Spanning Forest instance on the same graph with unit vertex weights, $K = |V| slash 3$ components, and weight bound $B = 3$.
 ][
+  _Numeric magnitude._ Unit vertex weights and component bound $3$ give target `max_weight_bits` exactly $2$, including the empty graph.
+
   _Construction._ Given a Partition into Paths of Length 2 instance on graph $G = (V, E)$ with $|V| = 3q$:
   - Graph: use $G$ unchanged.
   - Vertex weights: $w(v) = 1$ for all $v in V$.
@@ -15268,6 +15290,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("FlowShopScheduling", "ILP")[
   Order the jobs with pairwise precedence bits and completion-time variables on every machine; the deadline becomes a makespan bound.
 ][
+  _Numeric magnitude._ Let $h$ be `max_time_bits`, covering processing times and the deadline. The disjunction constant is the deadline plus the largest processing time, giving target `max_constraint_magnitude_bits` at most $h+1$.
+
   _Construction._ Let $q in {1, dots, m}$ index the machines, let $p_(j,q) = ell(t_q [j])$ be the processing time of job $j$ on machine $q$, and let $M = D + max_(j, q) p_(j,q)$. Variables: binary $y_(i,j)$ with $y_(i,j) = 1$ iff job $i$ precedes job $j$, and integer completion times $C_(j,q)$. The ILP is:
   $
     "find" quad & bold(x) \
@@ -15328,36 +15352,46 @@ The following reductions to Integer Linear Programming are straightforward formu
 ]
 
 #reduction-rule("MinimumTardinessSequencing", "ILP")[
-  A position-assignment ILP captures the permutation, the precedence constraints, and a binary tardy indicator for each unit-length task.
+  A position-assignment ILP captures the permutation, the precedence constraints, and a binary tardy indicator for each task.
 ][
-  _Construction._ Variables: binary $x_(j,p)$ placing task $j$ in position $p in {0, dots, n-1}$ and binary tardy indicators $u_j$, where $M = n$. The ILP is:
+  _Numeric magnitude._ For unit lengths, target `max_constraint_magnitude_bits` is at most $n+1$. For integer lengths let $h$ be `max_processing_time_bits`; then $L<n 2^h$ and every row magnitude is at most $2L$, giving the bound $h+n+1$. Deadline clipping makes a deadline-magnitude parameter unnecessary.
+
+  _Construction._ Variables: binary $x_(j,p)$ placing task $j$ in position $p in {0, dots, n-1}$ and binary tardy indicators $u_j$, where $M = n$. Replace each deadline by $d'_j = min(n,max(0,d_j))$. The ILP is:
   $
     min quad & sum_j u_j \
     "subject to" quad & sum_p x_(j,p) = 1 quad forall j \
     & sum_j x_(j,p) = 1 quad forall p \
     & sum_p p x_(i,p) + 1 <= sum_p p x_(j,p) quad "for each precedence" (i, j) \
-    & sum_p (p + 1) x_(j,p) - d_j <= M u_j quad forall j \
+    & sum_p (p + 1) x_(j,p) - d'_j <= M u_j quad forall j \
     & x_(j,p), u_j in {0, 1}.
   $
 
-  _Correctness._ ($arrow.r.double$) Any feasible schedule gives a permutation and tardy bits with objective equal to the number of tardy tasks. ($arrow.l.double$) Any feasible ILP assignment decodes to a precedence-respecting permutation, and each $u_j$ is forced to record whether task $j$ misses its deadline.
+  For positive integer lengths, let $L = sum_j ell_j$, set $M=L$, and clip deadlines to $[0,L]$. Replace each tardiness row by the position-specific rows
+  $ L x_(j,p) + sum_(q<p) sum_i ell_i x_(i,q) - L u_j <= d'_j - ell_j + L. $
+  At the assigned position this enforces the completion-time comparison; at other positions it is redundant. Clipping preserves tardiness because every nonempty completion time lies in $[1,L]$.
+
+  _Correctness._ ($arrow.r.double$) Any feasible schedule gives a permutation and tardy bits with objective equal to the number of tardy tasks. ($arrow.l.double$) Any feasible ILP assignment decodes to a precedence-respecting permutation, and a late task must have $u_j=1$. Minimization sets every other indicator to zero, so the optimum is the minimum number of tardy tasks.
 
-  _Solution extraction._ Decode the permutation from $x_(j,p)$ and encode it as Lehmer code.
+  _Solution extraction._ Decode the permutation directly from $x_(j,p)$.
 ]
 
 #reduction-rule("ResourceConstrainedScheduling", "ILP")[
   The source witness is already a time-slot assignment, so a standard time-indexed ILP suffices.
 ][
-  _Construction._ Variables: binary $x_(j,t)$ with $x_(j,t) = 1$ iff task $j$ is run in slot $t in {0, dots, D - 1}$, where $r_(j,q) = R_q(t_j)$ denotes the amount of resource $q$ consumed by task $j$. The ILP is:
+  _Numeric magnitude._ Let $h$ be `max_resource_bits`, covering all resource requirements and capacities. After capping the processor count by $n$, target `max_constraint_magnitude_bits` is at most $h+n$; neither deadline nor processor magnitude needs a new parameter.
+
+  _Construction._ Put $D'=min(D,n)$ and $m'=min(m,n)$, where $n$ is the task count. Variables: binary $x_(j,t)$ with $x_(j,t) = 1$ iff task $j$ is run in slot $t in {0, dots, D' - 1}$, where $r_(j,q) = R_q(t_j)$ denotes the amount of resource $q$ consumed by task $j$. The ILP is:
   $
     "find" quad & bold(x) \
     "subject to" quad & sum_t x_(j,t) = 1 quad forall j \
-    & sum_j x_(j,t) <= m quad forall t \
+    & sum_j x_(j,t) <= m' quad forall t \
     & sum_j r_(j,q) x_(j,t) <= B_q quad forall q, t \
     & x_(j,t) in {0, 1}.
   $
 
-  _Correctness._ ($arrow.r.double$) Any feasible schedule chooses one slot per task while respecting processor and resource capacities in every period. ($arrow.l.double$) Any feasible ILP solution directly gives such a slot assignment.
+  _Correctness._ ($arrow.r.double$) A feasible schedule uses at most $n$ occupied slots. Renumber these in order from zero, preserving each group of simultaneous tasks. This respects the deadline and all capacities, so it yields a feasible assignment within $D'$ slots. ($arrow.l.double$) Any feasible ILP solution directly gives such a slot assignment.
+
+  _Size bound._ There are at most $n^2$ variables, $n(r+2)$ constraints, and $n^3(r+2)$ nonzero coefficients for $r$ resources, independently of the numeric deadline.
 
   _Solution extraction._ Task $j$ is assigned to the unique slot $t$ with $x_(j,t) = 1$.
 ]
@@ -15365,24 +15399,28 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("SequencingToMinimizeMaximumCumulativeCost", "ILP")[
   Assign each task to one position in the permutation and bound the running cumulative cost at every prefix.
 ][
-  _Construction._ Variables: binary $x_(j,p)$ with $x_(j,p) = 1$ iff task $j$ is scheduled in position $p$. The ILP is:
+  _Numeric magnitude._ Let $h$ be `max_cost_bits` and $n$ the task count. Signed prefix magnitudes and the objective-variable endpoint are bounded by the sum of absolute costs; position coefficients are at most $n$. Target `max_constraint_magnitude_bits` is at most $h+n$.
+
+  _Construction._ Variables: binary $x_(j,p)$ with $x_(j,p) = 1$ iff task $j$ is scheduled in position $p$, and integer $z$ with $0<=z<=sum_j abs(c_j)$. The lower bound includes the empty prefix. The ILP is:
   $
-    "find" quad & bold(x) \
+    min quad & z \
     "subject to" quad & sum_p x_(j,p) = 1 quad forall j \
     & sum_j x_(j,p) = 1 quad forall p \
     & sum_p p x_(i,p) + 1 <= sum_p p x_(j,p) quad "for each precedence" (i, j) \
-    & sum_j sum_(p in {0, dots, q}) c_j x_(j,p) <= K quad forall q \
+    & sum_j sum_(p in {0, dots, q}) c_j x_(j,p) <= z quad forall q \
     & x_(j,p) in {0, 1}.
   $
 
-  _Correctness._ ($arrow.r.double$) A feasible permutation satisfies the precedence constraints and keeps every prefix sum at most $K$. ($arrow.l.double$) Any feasible ILP assignment is a permutation whose cumulative cost after each prefix is exactly the linear expression being bounded.
+  _Correctness._ ($arrow.r.double$) A feasible permutation satisfies the precedence constraints and sets $z$ to its maximum prefix cost, including zero for the empty prefix. ($arrow.l.double$) Any feasible ILP assignment is a permutation whose cumulative cost after each prefix is exactly the linear expression being bounded. Minimizing $z$ therefore preserves the optimum.
 
-  _Solution extraction._ Decode the position assignment and convert the resulting permutation to Lehmer code.
+  _Solution extraction._ Decode the permutation directly from the position assignment.
 ]
 
 #reduction-rule("SequencingToMinimizeTardyTaskWeight", "ILP")[
   Use position assignments and exact tardiness indicators, with both implications of each deadline comparison. Prefix bounds supply valid constants for the bounded-disjunction construction @vielma2015, including the signed lengths, signed weights, and arbitrary deadlines accepted by the source model.
 ][
+  _Numeric magnitude._ Let $h$ be `max_processing_time_bits` and $n$ the task count. Prefix bounds have absolute value below $n 2^h$; the clipped comparisons and normalized coefficients require at most two additional bits. Target `max_constraint_magnitude_bits` is at most $h+n+2$. Neither deadlines nor objective weights need a size parameter.
+
   _Construction._ For $n$ tasks introduce binary $x_(j,p)$ (task $j$ occupies position $p$) and binary $u_j$ (task $j$ is tardy), with the two families of assignment equations. Let $P_p = sum_(q<p) sum_j ell_j x_(j,q)$. Define $L_p$ and $U_p$ as the sums of the $p$ smallest and $p$ largest lengths respectively; both are zero for $p=0$. Any permutation satisfies $L_p <= P_p <= U_p$.
 
   For each task and position put
@@ -15403,6 +15441,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("SequencingWithDeadlinesAndSetUpTimes", "ILP")[
   Assign tasks to positions with switch-detection auxiliaries that gate per-compiler setup costs into the deadline constraints.
 ][
+  _Numeric magnitude._ Let $h$ be `max_time_bits`, covering lengths, deadlines, and setup times, and $n$ the task count. The disjunction constant is bounded by the sum of lengths plus $(n-1)$ times the largest setup time. Including row right-hand sides gives target `max_constraint_magnitude_bits` at most $h+n+2$.
+
   _Construction._ Let $n$ be the number of tasks. Variables: binary $x_(j,p)$ with $x_(j,p) = 1$ iff task $j$ occupies position $p$; binary $"sw"_p$ for $p >= 1$ indicating a compiler switch before position $p$; binary $a_(j,p) = x_(j,p) dot "sw"_p$ (linearised product). Let $M = sum_j ell_j + max_c s(c) dot (n-1)$. The ILP is:
   $
     "find" quad & bold(x) \
@@ -15423,6 +15463,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("SequencingToMinimizeWeightedTardiness", "ILP")[
   Encode the single-machine order with pairwise precedence bits and completion times, then linearize the weighted tardiness bound with nonnegative tardiness variables.
 ][
+  _Numeric magnitude._ Let $h$ be `max_numeric_magnitude_bits`, covering lengths, weights, deadlines, and the acceptance bound, and $n$ the task count. Completion and tardiness-variable endpoints are bounded by the total processing time, while the weighted acceptance row copies source weights. Target `max_constraint_magnitude_bits` is at most $h+n$.
+
   _Construction._ Variables: binary $y_(i,j)$ with $y_(i,j) = 1$ iff job $i$ precedes job $j$, integer completion times $C_j$, and nonnegative tardiness variables $T_j$, where $M = sum_j ell_j$ is a valid schedule-horizon bound. The ILP is:
   $
     "find" quad & bold(x) \
@@ -15647,6 +15689,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   @garey1979 This $O(m)$ reduction copies the graph unchanged and assigns unit weight to every edge ($n$ target vertices, $m$ target edges). A Hamiltonian circuit exists iff the optimal circuit length equals $n$.
 ][
+  _Numeric magnitude._ Every edge has length one, so target `max_length_bits` is exactly $1$.
+
   _Construction._ Given a Hamiltonian Circuit instance $G = (V, E)$ with $n = |V|$ and $m = |E|$, construct a DecisionLongestCircuit instance with bound $n$ on the same graph $G' = G$ with edge lengths $l(e) = 1$ for every $e in E$. Its decision condition is circuit length $>= n$.
 
   _Correctness._ ($arrow.r.double$) If $G$ has a Hamiltonian circuit $v_0, v_1, dots, v_(n-1), v_0$, then this circuit uses $n$ edges each of length 1, giving total length $n$. Since a simple circuit on $n$ vertices can use at most $n$ edges, this is optimal. ($arrow.l.double$) If the longest circuit in $G'$ has length $n$, it uses $n$ unit-weight edges and therefore visits $n$ distinct vertices, i.e., every vertex exactly once. This circuit is therefore a Hamiltonian circuit in $G$.
@@ -15690,9 +15734,11 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   Impose the decision bound on the selected circuit length. The optimization formulation gains one constraint and no variables.
 ][
-  _Construction._ For bound $B$, use the LongestCircuit-to-ILP construction above, add $sum_(e in E) l_e y_e >= B$, and replace the objective with zero.
+  _Numeric magnitude._ Let $h$ be `max_length_bits` and $m$ the edge count. The nonconstant acceptance row has bound at most $S<m 2^h$, while the original circuit constraints use magnitudes at most $2$. Target `max_constraint_magnitude_bits` is at most $h+m+1$. This needs no parameter for the generic decision threshold.
+
+  _Construction._ For bound $B$, use the LongestCircuit-to-ILP construction above, let $S=sum_(e in E) l_e$. Add $0>=0$ if $B<=0$, $0>=1$ if $B>S$, and $sum_(e in E) l_e y_e >= B$ otherwise, and replace the objective with zero.
 
-  _Correctness._ ($arrow.r.double$) A circuit of length at least $B$ extends to the existing selection and connectivity variables and meets the new constraint. ($arrow.l.double$) Every feasible target assignment selects one simple circuit, and the new constraint guarantees its length is at least $B$. A graph with no circuit remains infeasible regardless of the bound.
+  _Correctness._ ($arrow.r.double$) A circuit of length at least $B$ extends to the existing selection and connectivity variables and meets the new constraint. ($arrow.l.double$) Every feasible target assignment selects one simple circuit, and the new constraint guarantees its length is at least $B$. Positive edge lengths make the two constant-row cases equivalent to the original threshold comparison. A graph with no circuit remains infeasible regardless of the bound.
 
   _Solution extraction._ Check target feasibility, then return the existing edge-selection vector. Construction has the same asymptotic cost as the optimization formulation.#footnote[Complexity follows from the implementation; not independently verified from literature.]
 ]
@@ -15775,6 +15821,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("AcyclicPartition", "ILP")[
   Assign every vertex to a topologically numbered partition class and directly require every arc to have nondecreasing class labels, following the upper-triangular formulation of @ozkayaCatalyurek2022.
 ][
+  _Numeric magnitude._ Let $h$ be `max_numeric_magnitude_bits`, covering vertex weights, arc costs, and both bounds, and $n$ the vertex count. Label coefficients and endpoints are at most $n$; normalized product rows can contain coefficient $2$. Target `max_constraint_magnitude_bits` is at most $h+n+1$.
+
   _Construction._ Let $n = |V|$ and let the directed arcs be $A = {a_0, dots, a_(m-1)}$ with $a_t = (u_t -> v_t)$. The source witness already allows every vertex to choose one label in ${0, dots, n - 1}$, so the ILP uses exactly the same label range. Use `ILP<i64>` with variable order
   $(x_(v,c))_(v,c), (s_(t,c))_(t,c), (y_t)_t$.
   The indices are
@@ -15853,6 +15901,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("BoundedComponentSpanningForest", "ILP")[
   Assign every vertex to one of at most $K$ components, bound each component's total weight, and certify connectivity inside each used component by a flow witness.
 ][
+  _Numeric magnitude._ Let $h$ be `max_weight_bits`, covering vertex weights and the component bound, and $n$ the vertex count. Weight rows, unit flow rows, and flow-variable endpoints give target `max_constraint_magnitude_bits` at most $h+n$.
+
   _Construction._ Let $n = |V|$, let the graph edges be $E = {e_0, dots, e_(m-1)}$ with $e_i = {u_i, v_i}$, and let the allowed component labels be $c in {0, dots, K - 1}$. Use `ILP<i64>` with variables ordered as
   $(x_(v,c))_(v,c), (u_c)_c, (r_(v,c))_(v,c), (s_c)_c, (b_(v,c))_(v,c), (f_(i,eta,c))_(i,eta,c)$.
   Their indices are
@@ -16943,6 +16993,8 @@ The following table shows concrete target-variable counts for example instances,
 #reduction-rule("MinimumCapacitatedSpanningTree", "ILP")[
   Binary edge selectors $y_e$, directed requirement-flow variables $f$, and directed unit-demand connectivity variables $g$. The first flow enforces subtree capacities; the second connects even zero-requirement vertices.
 ][
+  _Numeric magnitude._ Let $h$ be `max_requirement_bits`, covering requirements and capacity, and $n$ the vertex count. Flow bounds and balance rows involve at most the sum of $n$ requirements; target `max_constraint_magnitude_bits` is at most $h+n$. Edge costs occur only in the objective.
+
   _Construction._ $5m$ variables: $m$ edge selectors and two directed flows of $2m$ variables each. Requirement flow sends $r(v)$ units from each non-root vertex to the root and is bounded by capacity $c$. Connectivity flow sends one unit from every non-root vertex to the root and satisfies $g_(u v)+g_(v u) <= (n-1)y_e$. Also impose $sum_e y_e=n-1$ and minimize $sum_e w(e) dot y_e$. This combines the standard non-unit-demand flow model @gouveiaLopes2000 with the standard unit-demand spanning-tree flow.
 
   _Correctness._ ($arrow.r.double$) A feasible capacitated spanning tree induces both flows along its unique root paths. ($arrow.l.double$) Unit-demand flow makes every vertex reachable from the root; together with $n-1$ selected edges this gives a spanning tree. Requirement flow on that tree equals each rooted subtree's total requirement, so its capacity bounds are exactly the source constraints.
@@ -17098,6 +17150,8 @@ The following table shows concrete target-variable counts for example instances,
 ][
   _Construction._ Let $A = (a_1, dots, a_n)$ with total sum $S = sum_(i=1)^n a_i$. Set task lengths $ell_i = a_i$, number of processors $m = 2$, and deadline $D = floor(S / 2)$.
 
+  _Numeric magnitude._ If each source size is below $2^h$, then $S < n dot 2^h <= 2^(h+n)$. Both the copied lengths and $D$ are therefore below $2^(h+n)$, giving the local upper bound `max_numeric_magnitude_bits + num_elements` on the target's `max_numeric_magnitude_bits`.
+
   _Correctness._ ($arrow.r.double$) If $A' subset.eq A$ has $sum_(i in A') a_i = S/2$, assign tasks in $A'$ to processor 0 and the rest to processor 1; both loads equal $S/2 = D$. ($arrow.l.double$) If a feasible schedule exists with both loads $<= D = floor(S/2)$, since both loads sum to $S$ and each is at most $floor(S/2)$, equality holds, giving a balanced partition.
 
   _Solution extraction._ The processor assignment $p_i in {0, 1}$ is the partition assignment directly.
@@ -17780,6 +17834,8 @@ The following table shows concrete target-variable counts for example instances,
 )[
   Compose the literal-compatibility clique construction @karp1972 with the incidence construction below. All weights and arc costs are positive integers of polynomial magnitude. This incidence lemma is proved here; it does not use the digit-encoded Subset Sum chain.
 ][
+  _Numeric magnitude._ For $c$ clauses, incidence count $L$ is at most $5(c+1)^2$, the cluster parameter is $c+1$, and capacity is at most $(c+1)^2$. All constructed magnitudes are below $64(c+1)^4<=2^(4c+6)$. Thus target `max_numeric_magnitude_bits` is at most $4c+6$, including $c=0$.
+
   _Construction._ First obtain a clique instance $H=(V,E)$ with threshold $k$ from the formal 3-SAT-to-KClique rule, including its universal vertex and padding. Write $h=|V|$, $e=|E|$, and $L=h+e$. Here $1 <= k <= h$.
 
   1. Create one unit-weight item per vertex and edge of $H$. Set $c=k(k+1)/2$, $M=2L+1$, and $B=2(L+c)+1$.
@@ -18920,6 +18976,8 @@ The following table shows concrete target-variable counts for example instances,
 )[
   This $O(n)$ specialization of Karp's common-deadline sequencing construction @karp1972 maps each element $a_i$ to a task with processing time and tardy weight $a_i$. For total $S$, use common deadline $B = floor(S / 2)$. A balanced partition exists exactly when the minimum tardy weight is $B$; other optimum values map to false through the formal aggregate reduction.
 ][
+  _Numeric magnitude._ Task lengths copy the source integers, so target `max_processing_time_bits` equals source `max_numeric_magnitude_bits`.
+
   _Construction._ The source has $n >= 1$ positive sizes with checked total $S$. Create $n$ tasks in source order, each with length and weight $a_i$, and deadline $B = floor(S / 2)$. The construction is identical for odd and even totals. Karp's original paper gives Knapsack to Job Sequencing (p. 100), with equal processing times and penalties and a common deadline; the Partition specialization and its optimization certificate are proved here.
 
   _Correctness._ Let $E$ be the total size of tasks completing by $B$ in any valid permutation. Positive processing times make these tasks a prefix, so $E <= B$. Because weights equal processing times, tardy weight is $W = S - E >= S - B >= B$.
@@ -19080,6 +19138,8 @@ The following table shows concrete target-variable counts for example instances,
 )[
   This $O(t^2)$ reduction @garey1979 first checks whether every coordinate of $W$, $X$, and $Y$ appears in some triple; uncovered coordinates yield a fixed infeasible 3-Partition instance. Otherwise it composes the classical 3DM $arrow.r$ ABCD-Partition, ABCD-Partition $arrow.r$ 4-Partition, and 4-Partition $arrow.r$ 3-Partition constructions, producing $24 t^2 - 3 t$ integers arranged into $8 t^2 - t$ triples.
 ][
+  _Numeric magnitude._ For universe size $q>=1$, the nonconstant gadget has partition bound $42949672960 q^4+964<2^36 q^4$. Since $q<=2^q$, target `max_numeric_magnitude_bits` is at most $4q+36$. The fixed feasible and infeasible outputs also satisfy this bound, including $q=0$.
+
   _Construction._ Let the source instance have universe size $q$ and triples $m_l = (w_(a_l), x_(b_l), y_(c_l))$ for $l = 0, dots, t - 1$. If $q=0$, the empty matching is a solution: return sizes $(1,1,1)$ with bound $3$, and recover the empty matching. Otherwise, if some coordinate of $W union X union Y$ is absent from all triples (including $t=0$), return the fixed infeasible instance $(6,6,6,6,7,9)$ with bound $20$. Including these constant cases, $24t^2-3t+6$ elements and $8t^2-t+2$ groups are upper bounds, not exact counts.
 
   Otherwise set $r = 32 q$ and $T_1 = 40 r^4$. For each triple create
@@ -19227,6 +19287,8 @@ The following table shows concrete target-variable counts for example instances,
 )[
   Each element becomes a unit-length task requiring $a_i$ units of a shared resource with bound $B$. With 3 processors and deadline $m$, every slot receives exactly 3 tasks summing to $B$.
 ][
+  _Numeric magnitude._ Resource requirements copy the element sizes and the resource capacity copies the partition bound. Target `max_resource_bits` therefore equals source `max_numeric_magnitude_bits`.
+
   _Construction._ Given $(S, B)$ with $|S| = 3m$ and $B/4 < a_i < B/2$. Create $3m$ unit-length tasks with resource requirement $r_i = a_i$, $p = 3$ processors, resource bound $B$, deadline $D = m$.
 
   _Correctness._ ($arrow.r.double$) A valid 3-partition assigns each triple to a time slot; each slot uses exactly $B$ resource units. ($arrow.l.double$) $3m$ tasks in $m$ slots with $p = 3$: every slot has exactly 3 tasks. Resource bound $B$ with total $m B$: each slot sums to exactly $B$. Size constraints prevent fewer or more than 3 elements per slot.
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index 698b9e1fa..5d3b7f9c4 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -5601,14 +5601,7 @@ fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
 #[test]
 fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let output = pred()
-        .args([
-            "path",
-            "DecisionLongestCircuit",
-            "ILP/bool",
-            "--limit",
-            "1",
-            "--json",
-        ])
+        .args(["path", "BMF", "BicliqueCover", "--limit", "1", "--json"])
         .output()
         .unwrap();
     assert!(output.status.success());
@@ -5625,14 +5618,15 @@ fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
             )
         })
         .collect::<std::collections::BTreeMap<_, _>>();
-    assert_eq!(relations["num_constraints"], "exact");
-    assert_eq!(relations["num_vars"], "exact");
-    assert_eq!(relations["max_constraint_magnitude_bits"], "unavailable");
+    for field in ["num_vertices", "left_size", "right_size", "rank"] {
+        assert_eq!(relations[field], "exact");
+    }
+    assert_eq!(relations["num_edges"], "unavailable");
     let unavailable = fields
         .iter()
         .find(|field| field["relation"] == "unavailable")
         .unwrap();
-    assert!(unavailable["reason"].as_str().unwrap().contains("length"));
+    assert!(!unavailable["reason"].as_str().unwrap().is_empty());
 }
 
 #[test]
diff --git a/src/lib.rs b/src/lib.rs
index afeac7aa1..1c70132cb 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -159,3 +159,7 @@ mod test_reduction_graph;
 #[cfg(test)]
 #[path = "unit_tests/unitdiskmapping_algorithms/mod.rs"]
 mod test_unitdiskmapping_algorithms;
+
+#[cfg(test)]
+#[path = "unit_tests/ilp_overhead.rs"]
+mod ilp_overhead;
diff --git a/src/models/graph/acyclic_partition.rs b/src/models/graph/acyclic_partition.rs
index b56ec16c6..219eed6d4 100644
--- a/src/models/graph/acyclic_partition.rs
+++ b/src/models/graph/acyclic_partition.rs
@@ -219,6 +219,17 @@ impl<W: WeightElement> AcyclicPartition<W> {
         !W::IS_UNIT
     }
 
+    /// Smallest h >= 1 bounding vertex weights, arc costs, and both budgets in magnitude by 2^h.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.vertex_weights
+                .iter()
+                .chain(&self.arc_costs)
+                .map(|value| value.to_sum())
+                .chain([self.weight_bound.clone(), self.cost_bound.clone()]),
+        )
+    }
+
     /// Get the number of vertices.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -253,7 +264,11 @@ where
     type Solution = Vec<usize>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_arcs", num_arcs), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("num_arcs", num_arcs),
+        ("num_vertices", num_vertices),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![W]
diff --git a/src/models/graph/bounded_component_spanning_forest.rs b/src/models/graph/bounded_component_spanning_forest.rs
index 4b0f3a30b..4671ac06d 100644
--- a/src/models/graph/bounded_component_spanning_forest.rs
+++ b/src/models/graph/bounded_component_spanning_forest.rs
@@ -161,6 +161,16 @@ impl<G: Graph, W: WeightElement> BoundedComponentSpanningForest<G, W> {
         &self.max_weight
     }
 
+    /// Smallest h >= 1 with every vertex weight and the component weight limit below 2^h.
+    pub fn max_weight_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.weights
+                .iter()
+                .map(|weight| weight.to_sum())
+                .chain(std::iter::once(self.max_weight.clone())),
+        )
+    }
+
     /// Get the number of vertices in the underlying graph.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -263,6 +273,7 @@ where
     type Value = crate::types::Or;
 
     crate::problem_parameters![
+        ("max_weight_bits", max_weight_bits),
         ("max_components", max_components),
         ("num_edges", num_edges),
         ("num_vertices", num_vertices),
diff --git a/src/models/graph/longest_circuit.rs b/src/models/graph/longest_circuit.rs
index e98895bb7..83d6d0ac7 100644
--- a/src/models/graph/longest_circuit.rs
+++ b/src/models/graph/longest_circuit.rs
@@ -181,6 +181,13 @@ impl<G: Graph, W: WeightElement> LongestCircuit<G, W> {
         self.edge_lengths.clone()
     }
 
+    /// Smallest h >= 1 with every edge length strictly below 2^h.
+    pub fn max_length_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.edge_lengths.iter().map(|length| length.to_sum()),
+        )
+    }
+
     /// Get the number of vertices in the graph.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -211,7 +218,11 @@ where
     type Solution = Vec<bool>;
     type Value = Max<W::Sum>;
 
-    crate::problem_parameters![("num_edges", num_edges), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("max_length_bits", max_length_bits),
+        ("num_edges", num_edges),
+        ("num_vertices", num_vertices),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![G, W]
diff --git a/src/models/graph/min_max_multicenter.rs b/src/models/graph/min_max_multicenter.rs
index 661fa6c51..880c598cd 100644
--- a/src/models/graph/min_max_multicenter.rs
+++ b/src/models/graph/min_max_multicenter.rs
@@ -236,6 +236,16 @@ impl<G: Graph, W: WeightElement> MinMaxMulticenter<G, W> {
         self.k
     }
 
+    /// Smallest h >= 1 with every vertex weight and edge length strictly below 2^h.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.vertex_weights
+                .iter()
+                .chain(&self.edge_lengths)
+                .map(|value| value.to_sum()),
+        )
+    }
+
     /// Get the number of vertices in the underlying graph.
     pub fn num_vertices(&self) -> usize {
         self.graph().num_vertices()
@@ -258,11 +268,11 @@ impl<G: Graph, W: WeightElement> MinMaxMulticenter<G, W> {
     /// Correct because all edge lengths are non-negative.
     ///
     /// Returns `None` if any vertex is unreachable from all centers.
-    fn shortest_distances(&self, config: &[bool]) -> Option<Vec<W::Sum>> {
+    fn shortest_distances(
+        &self,
+        config: &[bool],
+    ) -> Result<Option<Vec<W::Sum>>, crate::traits::EvaluationError> {
         let n = self.graph.num_vertices();
-        if config.len() != n {
-            return None;
-        }
         let edges = self.graph.edges();
 
         let mut adj: Vec<Vec<(usize, W::Sum)>> = vec![Vec::new(); n];
@@ -312,7 +322,11 @@ impl<G: Graph, W: WeightElement> MinMaxMulticenter<G, W> {
                 if visited[next] {
                     continue;
                 }
-                let new_dist = du.clone() + len.clone();
+                let new_dist = W::checked_add_to_sum(
+                    du.clone(),
+                    len.clone(),
+                    "adding min-max multicenter path lengths",
+                )?;
                 let update = match &dist[next] {
                     None => true,
                     Some(d) => new_dist < *d,
@@ -323,7 +337,7 @@ impl<G: Graph, W: WeightElement> MinMaxMulticenter<G, W> {
             }
         }
 
-        dist.into_iter().collect()
+        Ok(dist.into_iter().collect())
     }
 }
 
@@ -336,7 +350,11 @@ where
     type Solution = Vec<bool>;
     type Value = Min<W::Sum>;
 
-    crate::problem_parameters![("num_edges", num_edges), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("num_edges", num_edges),
+        ("num_vertices", num_vertices),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![G, W]
@@ -360,7 +378,7 @@ where
             }
 
             // Compute shortest distances to nearest center
-            let distances = match self.shortest_distances(config) {
+            let distances = match self.shortest_distances(config)? {
                 Some(d) => d,
                 None => {
                     return Ok(Min(None));
diff --git a/src/models/graph/minimum_capacitated_spanning_tree.rs b/src/models/graph/minimum_capacitated_spanning_tree.rs
index 8ce48e7d5..ad014ba6d 100644
--- a/src/models/graph/minimum_capacitated_spanning_tree.rs
+++ b/src/models/graph/minimum_capacitated_spanning_tree.rs
@@ -227,6 +227,16 @@ impl<G: Graph, W: WeightElement> MinimumCapacitatedSpanningTree<G, W> {
         &self.capacity
     }
 
+    /// Smallest h >= 1 bounding vertex requirements and capacity in magnitude strictly by 2^h.
+    pub fn max_requirement_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.requirements
+                .iter()
+                .map(|value| value.to_sum())
+                .chain(std::iter::once(self.capacity.clone())),
+        )
+    }
+
     /// Get the number of vertices in the underlying graph.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -381,7 +391,11 @@ where
     type Solution = Vec<bool>;
     type Value = Min<W::Sum>;
 
-    crate::problem_parameters![("num_edges", num_edges), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("max_requirement_bits", max_requirement_bits),
+        ("num_edges", num_edges),
+        ("num_vertices", num_vertices),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![G, W]
diff --git a/src/models/graph/multiple_choice_branching.rs b/src/models/graph/multiple_choice_branching.rs
index b04671ee2..e10c858d4 100644
--- a/src/models/graph/multiple_choice_branching.rs
+++ b/src/models/graph/multiple_choice_branching.rs
@@ -193,6 +193,16 @@ impl<W: WeightElement> MultipleChoiceBranching<W> {
         &self.threshold
     }
 
+    /// Smallest h >= 1 bounding arc weights and the threshold in magnitude strictly by 2^h.
+    pub fn max_weight_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.weights
+                .iter()
+                .map(|weight| weight.to_sum())
+                .chain(std::iter::once(self.threshold.clone())),
+        )
+    }
+
     /// Get the number of vertices.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -232,6 +242,7 @@ where
     type Value = crate::types::Or;
 
     crate::problem_parameters![
+        ("max_weight_bits", max_weight_bits),
         ("num_vertices", num_vertices),
         ("num_arcs", num_arcs),
         ("num_partition_groups", num_partition_groups),
diff --git a/src/models/graph/shortest_weight_constrained_path.rs b/src/models/graph/shortest_weight_constrained_path.rs
index b95ce34d8..7715caa35 100644
--- a/src/models/graph/shortest_weight_constrained_path.rs
+++ b/src/models/graph/shortest_weight_constrained_path.rs
@@ -267,6 +267,16 @@ impl<G: Graph, N: WeightElement> ShortestWeightConstrainedPath<G, N> {
         !N::IS_UNIT
     }
 
+    /// Smallest h >= 1 with every edge weight and the weight limit strictly below 2^h.
+    pub fn max_weight_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.edge_weights
+                .iter()
+                .map(|weight| weight.to_sum())
+                .chain(std::iter::once(self.weight_bound.clone())),
+        )
+    }
+
     /// Get the number of vertices in the graph.
     pub fn num_vertices(&self) -> usize {
         self.graph.num_vertices()
@@ -341,7 +351,11 @@ where
     type Solution = Vec<bool>;
     type Value = Min<N::Sum>;
 
-    crate::problem_parameters![("num_edges", num_edges), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("max_weight_bits", max_weight_bits),
+        ("num_edges", num_edges),
+        ("num_vertices", num_vertices),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![G, N]
diff --git a/src/models/misc/capacity_assignment.rs b/src/models/misc/capacity_assignment.rs
index aa18cea41..e76d250d2 100644
--- a/src/models/misc/capacity_assignment.rs
+++ b/src/models/misc/capacity_assignment.rs
@@ -118,6 +118,17 @@ impl CapacityAssignment {
         })
     }
 
+    /// Smallest h >= 1 bounding every delay and the delay budget in magnitude strictly by 2^h.
+    pub fn max_delay_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.delay
+                .iter()
+                .flatten()
+                .copied()
+                .chain(std::iter::once(self.delay_budget)),
+        )
+    }
+
     /// Number of communication links.
     pub fn num_links(&self) -> usize {
         self.cost.len()
@@ -189,7 +200,11 @@ impl Problem for CapacityAssignment {
     type Solution = Vec<usize>;
     type Value = crate::types::Min<i64>;
 
-    crate::problem_parameters![("num_capacities", num_capacities), ("num_links", num_links),];
+    crate::problem_parameters![
+        ("max_delay_bits", max_delay_bits),
+        ("num_capacities", num_capacities),
+        ("num_links", num_links),
+    ];
 
     fn evaluate(
         &self,
diff --git a/src/models/misc/flow_shop_scheduling.rs b/src/models/misc/flow_shop_scheduling.rs
index 1ef72562f..a33e1b30a 100644
--- a/src/models/misc/flow_shop_scheduling.rs
+++ b/src/models/misc/flow_shop_scheduling.rs
@@ -143,6 +143,17 @@ impl FlowShopScheduling {
         self.deadline
     }
 
+    /// Smallest h >= 1 with every processing time and the deadline strictly below 2^h.
+    pub fn max_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.task_lengths
+                .iter()
+                .flatten()
+                .copied()
+                .chain(std::iter::once(self.deadline)),
+        )
+    }
+
     /// Get the number of jobs.
     pub fn num_jobs(&self) -> usize {
         self.task_lengths.len()
@@ -206,7 +217,11 @@ impl Problem for FlowShopScheduling {
     type Solution = Vec<usize>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_jobs", num_jobs), ("num_processors", num_processors),];
+    crate::problem_parameters![
+        ("max_time_bits", max_time_bits),
+        ("num_jobs", num_jobs),
+        ("num_processors", num_processors),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/minimum_tardiness_sequencing.rs b/src/models/misc/minimum_tardiness_sequencing.rs
index a17af7951..0b7b2784a 100644
--- a/src/models/misc/minimum_tardiness_sequencing.rs
+++ b/src/models/misc/minimum_tardiness_sequencing.rs
@@ -201,6 +201,11 @@ fn validate_task_data(
 }
 
 impl<W: WeightElement> MinimumTardinessSequencing<W> {
+    /// Smallest h >= 1 with every processing time strictly below 2^h.
+    pub fn max_processing_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(self.lengths.iter().map(|length| length.to_sum()))
+    }
+
     /// Returns the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.deadlines.len()
@@ -253,6 +258,7 @@ impl Problem for MinimumTardinessSequencing<One> {
     type Value = Min<i64>;
 
     crate::problem_parameters![
+        ("max_processing_time_bits", max_processing_time_bits),
         ("num_precedences", num_precedences),
         ("num_tasks", num_tasks),
     ];
@@ -318,6 +324,7 @@ impl Problem for MinimumTardinessSequencing<i64> {
     type Value = Min<i64>;
 
     crate::problem_parameters![
+        ("max_processing_time_bits", max_processing_time_bits),
         ("num_precedences", num_precedences),
         ("num_tasks", num_tasks),
     ];
diff --git a/src/models/misc/multiprocessor_scheduling.rs b/src/models/misc/multiprocessor_scheduling.rs
index 8eb7c7f0c..6abcd7301 100644
--- a/src/models/misc/multiprocessor_scheduling.rs
+++ b/src/models/misc/multiprocessor_scheduling.rs
@@ -126,6 +126,16 @@ impl MultiprocessorScheduling {
         self.lengths.len()
     }
 
+    /// Smallest h >= 1 such that every task length and the deadline are below 2^h.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.lengths
+                .iter()
+                .copied()
+                .chain(std::iter::once(self.deadline)),
+        )
+    }
+
     /// Returns the total processing time of all tasks.
     pub fn total_length(&self) -> i64 {
         self.lengths.iter().sum()
@@ -137,7 +147,11 @@ impl Problem for MultiprocessorScheduling {
     type Solution = Vec<usize>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_processors", num_processors), ("num_tasks", num_tasks),];
+    crate::problem_parameters![
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("num_processors", num_processors),
+        ("num_tasks", num_tasks),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/partially_ordered_knapsack.rs b/src/models/misc/partially_ordered_knapsack.rs
index b0445099e..3d0b24072 100644
--- a/src/models/misc/partially_ordered_knapsack.rs
+++ b/src/models/misc/partially_ordered_knapsack.rs
@@ -223,6 +223,16 @@ impl PartiallyOrderedKnapsack {
         self.capacity
     }
 
+    /// Smallest h >= 1 with every item weight and the capacity strictly below 2^h.
+    pub fn max_weight_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.weights
+                .iter()
+                .copied()
+                .chain(std::iter::once(self.capacity)),
+        )
+    }
+
     /// Returns the number of items.
     pub fn num_items(&self) -> usize {
         self.weights.len()
@@ -257,6 +267,7 @@ impl Problem for PartiallyOrderedKnapsack {
     type Value = Max<i64>;
 
     crate::problem_parameters![
+        ("max_weight_bits", max_weight_bits),
         ("num_items", num_items),
         ("num_precedences", num_precedences),
     ];
diff --git a/src/models/misc/resource_constrained_scheduling.rs b/src/models/misc/resource_constrained_scheduling.rs
index c43d4bdca..c186a6f0a 100644
--- a/src/models/misc/resource_constrained_scheduling.rs
+++ b/src/models/misc/resource_constrained_scheduling.rs
@@ -118,6 +118,17 @@ impl ResourceConstrainedScheduling {
         })
     }
 
+    /// Smallest h >= 1 with every resource requirement and bound strictly below 2^h.
+    pub fn max_resource_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.resource_requirements
+                .iter()
+                .flatten()
+                .copied()
+                .chain(self.resource_bounds.iter().copied()),
+        )
+    }
+
     /// Get the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.resource_requirements.len()
@@ -179,6 +190,7 @@ impl Problem for ResourceConstrainedScheduling {
     type Value = crate::types::Or;
 
     crate::problem_parameters![
+        ("max_resource_bits", max_resource_bits),
         ("deadline", deadline),
         ("num_resources", num_resources),
         ("num_tasks", num_tasks),
@@ -211,8 +223,12 @@ impl Problem for ResourceConstrainedScheduling {
                     ));
                 }
 
-                // Check processor capacity and resource constraints at each time slot
-                for u in 0..d {
+                // Empty slots consume no resources. Keep ascending slot order and
+                // task order within each slot for checked accumulation.
+                let mut occupied = config.clone();
+                occupied.sort_unstable();
+                occupied.dedup();
+                for u in occupied {
                     // Collect tasks scheduled at time slot u
                     let mut task_count = 0usize;
                     let mut resource_usage = vec![0i64; r];
diff --git a/src/models/misc/scheduling_to_minimize_weighted_completion_time.rs b/src/models/misc/scheduling_to_minimize_weighted_completion_time.rs
index 68459fc3f..bd478f199 100644
--- a/src/models/misc/scheduling_to_minimize_weighted_completion_time.rs
+++ b/src/models/misc/scheduling_to_minimize_weighted_completion_time.rs
@@ -142,6 +142,11 @@ impl SchedulingToMinimizeWeightedCompletionTime {
         }
     }
 
+    /// Smallest h >= 1 bounding every processing time in magnitude strictly by 2^h.
+    pub fn max_processing_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(self.lengths.iter().copied())
+    }
+
     /// Returns the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.lengths.len()
@@ -275,7 +280,11 @@ impl Problem for SchedulingToMinimizeWeightedCompletionTime {
     type Solution = Vec<usize>;
     type Value = Min<i64>;
 
-    crate::problem_parameters![("num_processors", num_processors), ("num_tasks", num_tasks),];
+    crate::problem_parameters![
+        ("max_processing_time_bits", max_processing_time_bits),
+        ("num_processors", num_processors),
+        ("num_tasks", num_tasks),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/sequencing_to_minimize_maximum_cumulative_cost.rs b/src/models/misc/sequencing_to_minimize_maximum_cumulative_cost.rs
index 95b9cc819..b226e1914 100644
--- a/src/models/misc/sequencing_to_minimize_maximum_cumulative_cost.rs
+++ b/src/models/misc/sequencing_to_minimize_maximum_cumulative_cost.rs
@@ -89,6 +89,11 @@ impl SequencingToMinimizeMaximumCumulativeCost {
         &self.precedences
     }
 
+    /// Smallest h >= 1 bounding every task cost in magnitude strictly by 2^h.
+    pub fn max_cost_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(self.costs.iter().copied())
+    }
+
     /// Return the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.costs.len()
@@ -153,6 +158,7 @@ impl Problem for SequencingToMinimizeMaximumCumulativeCost {
     type Value = crate::types::Min<i64>;
 
     crate::problem_parameters![
+        ("max_cost_bits", max_cost_bits),
         ("num_precedences", num_precedences),
         ("num_tasks", num_tasks),
     ];
diff --git a/src/models/misc/sequencing_to_minimize_tardy_task_weight.rs b/src/models/misc/sequencing_to_minimize_tardy_task_weight.rs
index cae8f9a6d..edf3b7916 100644
--- a/src/models/misc/sequencing_to_minimize_tardy_task_weight.rs
+++ b/src/models/misc/sequencing_to_minimize_tardy_task_weight.rs
@@ -118,6 +118,11 @@ impl SequencingToMinimizeTardyTaskWeight {
         }
     }
 
+    /// Smallest h >= 1 bounding every processing time in magnitude strictly by 2^h.
+    pub fn max_processing_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(self.lengths.iter().copied())
+    }
+
     /// Returns the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.lengths.len()
@@ -190,7 +195,10 @@ impl Problem for SequencingToMinimizeTardyTaskWeight {
     type Solution = Vec<usize>;
     type Value = Min<i64>;
 
-    crate::problem_parameters![("num_tasks", num_tasks),];
+    crate::problem_parameters![
+        ("max_processing_time_bits", max_processing_time_bits),
+        ("num_tasks", num_tasks),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/sequencing_to_minimize_weighted_completion_time.rs b/src/models/misc/sequencing_to_minimize_weighted_completion_time.rs
index 05cd17d62..a0004949c 100644
--- a/src/models/misc/sequencing_to_minimize_weighted_completion_time.rs
+++ b/src/models/misc/sequencing_to_minimize_weighted_completion_time.rs
@@ -120,6 +120,11 @@ impl SequencingToMinimizeWeightedCompletionTime {
         }
     }
 
+    /// Smallest h >= 1 bounding every processing time in magnitude strictly by 2^h.
+    pub fn max_processing_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(self.lengths.iter().copied())
+    }
+
     /// Returns the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.lengths.len()
@@ -223,6 +228,7 @@ impl Problem for SequencingToMinimizeWeightedCompletionTime {
     type Value = Min<i64>;
 
     crate::problem_parameters![
+        ("max_processing_time_bits", max_processing_time_bits),
         ("num_precedences", num_precedences),
         ("num_tasks", num_tasks),
     ];
diff --git a/src/models/misc/sequencing_to_minimize_weighted_tardiness.rs b/src/models/misc/sequencing_to_minimize_weighted_tardiness.rs
index ebcba6231..dc729a1e8 100644
--- a/src/models/misc/sequencing_to_minimize_weighted_tardiness.rs
+++ b/src/models/misc/sequencing_to_minimize_weighted_tardiness.rs
@@ -144,6 +144,18 @@ impl SequencingToMinimizeWeightedTardiness {
         self.bound
     }
 
+    /// Smallest h >= 1 with all lengths, weights, deadlines, and the cost bound below 2^h.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.lengths
+                .iter()
+                .chain(&self.weights)
+                .chain(&self.deadlines)
+                .copied()
+                .chain(std::iter::once(self.bound)),
+        )
+    }
+
     /// Returns the number of jobs.
     pub fn num_tasks(&self) -> usize {
         self.lengths.len()
@@ -208,7 +220,10 @@ impl Problem for SequencingToMinimizeWeightedTardiness {
     type Solution = Vec<usize>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_tasks", num_tasks),];
+    crate::problem_parameters![
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("num_tasks", num_tasks),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/sequencing_with_deadlines_and_set_up_times.rs b/src/models/misc/sequencing_with_deadlines_and_set_up_times.rs
index 568c4f3df..0f5ddbebb 100644
--- a/src/models/misc/sequencing_with_deadlines_and_set_up_times.rs
+++ b/src/models/misc/sequencing_with_deadlines_and_set_up_times.rs
@@ -111,6 +111,17 @@ impl SequencingWithDeadlinesAndSetUpTimes {
         }
     }
 
+    /// Smallest h >= 1 bounding lengths, deadlines, and setup times in magnitude by 2^h.
+    pub fn max_time_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.lengths
+                .iter()
+                .chain(&self.deadlines)
+                .chain(&self.setup_times)
+                .copied(),
+        )
+    }
+
     /// Returns the number of tasks.
     pub fn num_tasks(&self) -> usize {
         self.lengths.len()
@@ -211,7 +222,7 @@ impl Problem for SequencingWithDeadlinesAndSetUpTimes {
     type Solution = Vec<usize>;
     type Value = Or;
 
-    crate::problem_parameters![("num_tasks", num_tasks),];
+    crate::problem_parameters![("max_time_bits", max_time_bits), ("num_tasks", num_tasks),];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/three_partition.rs b/src/models/misc/three_partition.rs
index 9a57d336c..2220198c8 100644
--- a/src/models/misc/three_partition.rs
+++ b/src/models/misc/three_partition.rs
@@ -88,6 +88,16 @@ impl ThreePartition {
         Ok(Self { sizes, bound })
     }
 
+    /// Smallest h >= 1 with every element size and the target sum strictly below 2^h.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.sizes
+                .iter()
+                .copied()
+                .chain(std::iter::once(self.bound)),
+        )
+    }
+
     /// Create a new 3-Partition instance.
     ///
     /// # Panics
@@ -183,7 +193,11 @@ impl Problem for ThreePartition {
     type Solution = Vec<usize>;
     type Value = Or;
 
-    crate::problem_parameters![("num_elements", num_elements), ("num_groups", num_groups),];
+    crate::problem_parameters![
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("num_elements", num_elements),
+        ("num_groups", num_groups),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/rules/acyclicpartition_ilp.rs b/src/rules/acyclicpartition_ilp.rs
index a176bdca9..a409c6fe1 100644
--- a/src/rules/acyclicpartition_ilp.rs
+++ b/src/rules/acyclicpartition_ilp.rs
@@ -44,14 +44,12 @@ impl ReductionResult for ReductionAcyclicPartitionToILP {
 impl crate::rules::AggregateReductionResult for ReductionAcyclicPartitionToILP {}
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "vertex weights, arc costs and feasibility budgets are not registered source parameters",
-    },
     exact {
         num_vars = "num_vertices * num_vertices + num_arcs * num_vertices + num_arcs + num_vertices",
         num_constraints = "num_vertices^2 + 4 * num_vertices + 3 * num_arcs * num_vertices + 2 * num_arcs + 1",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_numeric_magnitude_bits + num_vertices + 1",
         num_nonzeros = "(num_vertices * num_vertices + num_arcs * num_vertices + num_arcs + num_vertices) * (num_vertices^2 + 4 * num_vertices + 3 * num_arcs * num_vertices + 2 * num_arcs + 1)",
     },
 })]
diff --git a/src/rules/boundedcomponentspanningforest_ilp.rs b/src/rules/boundedcomponentspanningforest_ilp.rs
index 9b5989b8a..02018bba1 100644
--- a/src/rules/boundedcomponentspanningforest_ilp.rs
+++ b/src/rules/boundedcomponentspanningforest_ilp.rs
@@ -46,14 +46,12 @@ impl ReductionResult for ReductionBCSFToILP {
 impl crate::rules::AggregateReductionResult for ReductionBCSFToILP {}
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "component weight bounds and vertex weights are not registered source parameters",
-    },
     exact {
         num_vars = "3 * num_vertices * max_components + 2 * max_components + 2 * num_edges * max_components",
         num_constraints = "num_vertices + 5 * max_components + 6 * num_vertices * max_components + 6 * num_edges * max_components",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_weight_bits + num_vertices",
         num_nonzeros = "(3 * num_vertices * max_components + 2 * max_components + 2 * num_edges * max_components) * (num_vertices + 5 * max_components + 6 * num_vertices * max_components + 6 * num_edges * max_components)",
     },
 })]
diff --git a/src/rules/capacityassignment_ilp.rs b/src/rules/capacityassignment_ilp.rs
index 3f7bb842c..af1ca2817 100644
--- a/src/rules/capacityassignment_ilp.rs
+++ b/src/rules/capacityassignment_ilp.rs
@@ -50,10 +50,8 @@ impl ReductionResult for ReductionCAToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "delays and the delay budget are not registered source parameters",
-    },
     exact {
+        max_constraint_magnitude_bits = "max_delay_bits",
         num_vars = "num_links * num_capacities",
         num_constraints = "num_links + 1",
     },
diff --git a/src/rules/decisionminimumdominatingset_minmaxmulticenter.rs b/src/rules/decisionminimumdominatingset_minmaxmulticenter.rs
index ac4b58d98..757c4223f 100644
--- a/src/rules/decisionminimumdominatingset_minmaxmulticenter.rs
+++ b/src/rules/decisionminimumdominatingset_minmaxmulticenter.rs
@@ -48,6 +48,7 @@ impl crate::rules::AggregateReductionResult
 
 #[reduction(
     transform = exact {
+        max_numeric_magnitude_bits = "1",
         num_vertices = "num_vertices + 2",
         num_edges = "num_edges",
     }
diff --git a/src/rules/flowshopscheduling_ilp.rs b/src/rules/flowshopscheduling_ilp.rs
index affc67e2f..712610d30 100644
--- a/src/rules/flowshopscheduling_ilp.rs
+++ b/src/rules/flowshopscheduling_ilp.rs
@@ -73,13 +73,11 @@ impl crate::rules::AggregateReductionResult for ReductionFSSToILP {}
 
 #[reduction(
     transform = upper_bound {
+        max_constraint_magnitude_bits = "max_time_bits + 1",
         num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors",
         num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs",
         num_nonzeros = "(num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors) * (num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs)",
     },
-    unavailable = {
-        max_constraint_magnitude_bits = "processing times and the deadline are not registered source parameters",
-    },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for FlowShopScheduling {
     type Result = ReductionFSSToILP;
diff --git a/src/rules/hamiltoniancircuit_longestcircuit.rs b/src/rules/hamiltoniancircuit_longestcircuit.rs
index 03ab5871c..0eaf83041 100644
--- a/src/rules/hamiltoniancircuit_longestcircuit.rs
+++ b/src/rules/hamiltoniancircuit_longestcircuit.rs
@@ -47,6 +47,7 @@ impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToLon
 
 #[reduction(
     transform = exact {
+        max_length_bits = "1",
         num_vertices = "num_vertices",
         num_edges = "num_edges",
     }
diff --git a/src/rules/ksatisfiability_acyclicpartition.rs b/src/rules/ksatisfiability_acyclicpartition.rs
index d88ce5861..f1b404d0b 100644
--- a/src/rules/ksatisfiability_acyclicpartition.rs
+++ b/src/rules/ksatisfiability_acyclicpartition.rs
@@ -53,6 +53,7 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToAcyclicPartition
 
 #[reduction(
     transform = upper_bound {
+        max_numeric_magnitude_bits = "4 * num_clauses + 6",
         num_vertices = "(9 * num_clauses^2 + 3 * num_clauses + 6) / 2",
         num_arcs = "18 * num_clauses^2 + 2",
     }
diff --git a/src/rules/longestcircuit_ilp.rs b/src/rules/longestcircuit_ilp.rs
index 489689502..dbf34f385 100644
--- a/src/rules/longestcircuit_ilp.rs
+++ b/src/rules/longestcircuit_ilp.rs
@@ -216,11 +216,9 @@ impl crate::rules::AggregateReductionResult for ReductionDecisionLongestCircuitT
         num_constraints = "3 + num_vertices + 2 * num_vertices^2 + 2 * num_edges * num_vertices",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_length_bits + num_edges + 1",
         num_nonzeros = "(num_edges + 2 * num_vertices + 2 * num_edges * num_vertices) * (3 + num_vertices + 2 * num_vertices^2 + 2 * num_edges * num_vertices)",
     },
-    unavailable {
-        max_constraint_magnitude_bits = "the decision threshold and edge lengths copied into the acceptance row are not registered source parameters",
-    },
 })]
 impl ReduceTo<ILP<bool>> for Decision<LongestCircuit<SimpleGraph, i64>> {
     type Result = ReductionDecisionLongestCircuitToILP;
@@ -228,10 +226,22 @@ impl ReduceTo<ILP<bool>> for Decision<LongestCircuit<SimpleGraph, i64>> {
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let mut inner = ReduceTo::<ILP<bool>>::reduce_to(self.inner())?;
         let mut constraints = inner.target.constraints().to_vec();
-        constraints.push(LinearConstraint::ge(
-            inner.target.objective().to_vec(),
-            *self.bound(),
-        ));
+        // Positive edge lengths bound every circuit by their total. Normalize
+        // thresholds outside that range while retaining one acceptance row.
+        let total_length: i128 = self
+            .inner()
+            .edge_lengths()
+            .iter()
+            .map(|&length| i128::from(length))
+            .sum();
+        let acceptance = if *self.bound() <= 0 {
+            LinearConstraint::ge(vec![], 0)
+        } else if i128::from(*self.bound()) > total_length {
+            LinearConstraint::ge(vec![], 1)
+        } else {
+            LinearConstraint::ge(inner.target.objective().to_vec(), *self.bound())
+        };
+        constraints.push(acceptance);
         inner.target = ILP::with_variables(
             inner.target.variables().to_vec(),
             constraints,
diff --git a/src/rules/minimumcapacitatedspanningtree_ilp.rs b/src/rules/minimumcapacitatedspanningtree_ilp.rs
index 2dbf72968..f97bc835c 100644
--- a/src/rules/minimumcapacitatedspanningtree_ilp.rs
+++ b/src/rules/minimumcapacitatedspanningtree_ilp.rs
@@ -64,13 +64,11 @@ impl ReductionResult for ReductionMinimumCapacitatedSpanningTreeToILP {
 
 #[reduction(
     transform = upper_bound {
+        max_constraint_magnitude_bits = "max_requirement_bits + num_vertices",
         num_vars = "5 * num_edges",
         num_constraints = "5 * num_edges + 2 * num_vertices + 1",
         num_nonzeros = "(5 * num_edges) * (5 * num_edges + 2 * num_vertices + 1)",
     },
-    unavailable = {
-        max_constraint_magnitude_bits = "capacity and vertex requirements are not registered source parameters",
-    },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for MinimumCapacitatedSpanningTree<SimpleGraph, i64> {
     type Result = ReductionMinimumCapacitatedSpanningTreeToILP;
diff --git a/src/rules/minimumtardinesssequencing_ilp.rs b/src/rules/minimumtardinesssequencing_ilp.rs
index 6a0951d63..1955399c7 100644
--- a/src/rules/minimumtardinesssequencing_ilp.rs
+++ b/src/rules/minimumtardinesssequencing_ilp.rs
@@ -105,14 +105,12 @@ fn build_common_constraints(
 
 // Unit-length variant
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "task deadlines and processing times are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_tasks * num_tasks + num_tasks",
         num_constraints = "2 * num_tasks + num_precedences + num_tasks",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "num_tasks + 1",
         num_nonzeros = "(num_tasks * num_tasks + num_tasks) * (2 * num_tasks + num_precedences + num_tasks)",
     },
 })]
@@ -138,7 +136,8 @@ impl ReduceTo<ILP<bool>> for MinimumTardinessSequencing<One> {
             let mut terms: Vec<(usize, i64)> =
                 (0..n).map(|p| (x_var(j, p), positions[p] + 1)).collect();
             terms.push((u_var(j), -big_m));
-            let deadline = self.deadlines()[j];
+            // Completion times lie in [1, n]; outside deadlines have the same tardy status.
+            let deadline = self.deadlines()[j].clamp(0, big_m);
             constraints.push(LinearConstraint::le(terms, deadline));
         }
 
@@ -154,14 +153,12 @@ impl ReduceTo<ILP<bool>> for MinimumTardinessSequencing<One> {
 
 // Arbitrary-length variant
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "task deadlines and processing times are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_tasks * num_tasks + num_tasks",
         num_constraints = "2 * num_tasks + num_precedences + num_tasks * num_tasks",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_processing_time_bits + num_tasks + 1",
         num_nonzeros = "(num_tasks * num_tasks + num_tasks) * (2 * num_tasks + num_precedences + num_tasks * num_tasks)",
     },
 })]
@@ -193,6 +190,17 @@ impl ReduceTo<ILP<bool>> for MinimumTardinessSequencing<i64> {
         // Tardy indicator for arbitrary lengths.
         let lengths = self.lengths();
         for j in 0..n {
+            // Positive lengths bound all completion times by total_length.
+            let rhs = self.deadlines()[j]
+                .clamp(0, total_length)
+                .checked_sub(lengths[j])
+                .and_then(|value| value.checked_add(total_length))
+                .ok_or_else(|| {
+                    crate::rules::ReductionError::integer_overflow::<
+                        MinimumTardinessSequencing<i64>,
+                        ILP<bool>,
+                    >("computing a tardiness constraint bound")
+                })?;
             for p in 0..n {
                 let mut terms: Vec<(usize, i64)> = Vec::new();
                 terms.push((x_var(j, p), big_m));
@@ -202,15 +210,6 @@ impl ReduceTo<ILP<bool>> for MinimumTardinessSequencing<i64> {
                     }
                 }
                 terms.push((u_var(j), -big_m));
-                let rhs = self.deadlines()[j]
-                    .checked_sub(lengths[j])
-                    .and_then(|value| value.checked_add(total_length))
-                    .ok_or_else(|| {
-                        crate::rules::ReductionError::integer_overflow::<
-                            MinimumTardinessSequencing<i64>,
-                            ILP<bool>,
-                        >("computing a tardiness constraint bound")
-                    })?;
                 constraints.push(LinearConstraint::le(terms, rhs));
             }
         }
diff --git a/src/rules/minmaxmulticenter_ilp.rs b/src/rules/minmaxmulticenter_ilp.rs
index a60d92f4b..ed410c8b0 100644
--- a/src/rules/minmaxmulticenter_ilp.rs
+++ b/src/rules/minmaxmulticenter_ilp.rs
@@ -66,7 +66,7 @@ fn weighted_distances_mmc(
     edge_lengths: &[i64],
     source: usize,
     n: usize,
-) -> Vec<Option<i64>> {
+) -> Result<Vec<Option<i64>>, crate::rules::ReductionError> {
     let mut adj: Vec<Vec<(usize, i64)>> = vec![Vec::new(); n];
     for (idx, &(u, v)) in graph.edges().iter().enumerate() {
         let len = edge_lengths[idx];
@@ -74,7 +74,7 @@ fn weighted_distances_mmc(
         adj[v].push((u, len));
     }
 
-    let mut dist = vec![None; n];
+    let mut dist = vec![None::<i64>; n];
     let mut visited = vec![false; n];
     dist[source] = Some(0);
 
@@ -107,7 +107,12 @@ fn weighted_distances_mmc(
             if visited[v] {
                 continue;
             }
-            let candidate = du + len;
+            let candidate = du.checked_add(len).ok_or_else(|| {
+                crate::rules::ReductionError::integer_overflow::<
+                    MinMaxMulticenter<SimpleGraph, i64>,
+                    ILP<i64, i64, Bounded>,
+                >("adding shortest-path lengths")
+            })?;
             let should_update = match dist[v] {
                 None => true,
                 Some(current) => candidate < current,
@@ -118,18 +123,16 @@ fn weighted_distances_mmc(
         }
     }
 
-    dist
+    Ok(dist)
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "weighted graph distances are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_vertices + num_vertices^2 + 1",
         num_constraints = "2 * num_vertices^2 + 3 * num_vertices + 2",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "2 * max_numeric_magnitude_bits + num_vertices",
         num_nonzeros = "(num_vertices + num_vertices^2 + 1) * (2 * num_vertices^2 + 3 * num_vertices + 2)",
     },
 })]
@@ -145,7 +148,7 @@ impl ReduceTo<ILP<i64, i64, Bounded>> for MinMaxMulticenter<SimpleGraph, i64> {
         // Precompute all-pairs weighted shortest-path distances.
         let all_dist: Vec<Vec<Option<i64>>> = (0..n)
             .map(|s| weighted_distances_mmc(self.graph(), edge_lengths, s, n))
-            .collect();
+            .collect::<Result<_, _>>()?;
 
         // Index helpers.
         let x_var = |j: usize| j;
diff --git a/src/rules/multiplechoicebranching_ilp.rs b/src/rules/multiplechoicebranching_ilp.rs
index 1580909ed..5103abecc 100644
--- a/src/rules/multiplechoicebranching_ilp.rs
+++ b/src/rules/multiplechoicebranching_ilp.rs
@@ -40,14 +40,12 @@ impl ReductionResult for ReductionMultipleChoiceBranchingToILP {
 impl crate::rules::AggregateReductionResult for ReductionMultipleChoiceBranchingToILP {}
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "arc weights and the feasibility threshold are not registered source parameters",
-    },
     exact {
         num_vars = "num_arcs + num_vertices",
         num_constraints = "2 * num_arcs + 2 * num_vertices + num_partition_groups + 1",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_weight_bits + num_vertices",
         num_nonzeros = "(num_arcs + num_vertices) * (2 * num_arcs + 2 * num_vertices + num_partition_groups + 1)",
     },
 })]
diff --git a/src/rules/multiprocessorscheduling_ilp.rs b/src/rules/multiprocessorscheduling_ilp.rs
index e38aee57e..f1e19d945 100644
--- a/src/rules/multiprocessorscheduling_ilp.rs
+++ b/src/rules/multiprocessorscheduling_ilp.rs
@@ -57,10 +57,8 @@ impl ReductionResult for ReductionMSToILP {
 impl crate::rules::AggregateReductionResult for ReductionMSToILP {}
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "task lengths and the deadline are not registered source parameters",
-    },
     exact {
+        max_constraint_magnitude_bits = "max_numeric_magnitude_bits",
         num_vars = "num_tasks * num_processors",
         num_constraints = "num_tasks + num_processors",
     },
diff --git a/src/rules/optimallineararrangement_sequencingtominimizeweightedcompletiontime.rs b/src/rules/optimallineararrangement_sequencingtominimizeweightedcompletiontime.rs
index a83378b83..a4ef67f52 100644
--- a/src/rules/optimallineararrangement_sequencingtominimizeweightedcompletiontime.rs
+++ b/src/rules/optimallineararrangement_sequencingtominimizeweightedcompletiontime.rs
@@ -56,6 +56,7 @@ impl ReductionResult for ReductionOLAToSequencingToMinimizeWeightedCompletionTim
 
 #[reduction(
     transform = exact {
+        max_processing_time_bits = "1",
         num_tasks = "num_vertices + num_edges",
         num_precedences = "2 * num_edges",
     }
diff --git a/src/rules/partiallyorderedknapsack_ilp.rs b/src/rules/partiallyorderedknapsack_ilp.rs
index b4d0a70e7..16af0e786 100644
--- a/src/rules/partiallyorderedknapsack_ilp.rs
+++ b/src/rules/partiallyorderedknapsack_ilp.rs
@@ -32,10 +32,8 @@ impl ReductionResult for ReductionPOKToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "item weights and capacity are not registered source parameters",
-    },
     exact {
+        max_constraint_magnitude_bits = "max_weight_bits",
         num_vars = "num_items",
         num_constraints = "num_precedences + 1",
     },
diff --git a/src/rules/partition_multiprocessorscheduling.rs b/src/rules/partition_multiprocessorscheduling.rs
index 6ecdc103c..5ff8a17f1 100644
--- a/src/rules/partition_multiprocessorscheduling.rs
+++ b/src/rules/partition_multiprocessorscheduling.rs
@@ -54,9 +54,14 @@ impl ReductionResult for ReductionPartitionToMPS {
 impl crate::rules::AggregateReductionResult for ReductionPartitionToMPS {}
 
 #[reduction(
-    transform = exact {
-        num_tasks = "num_elements",
-        num_processors = "2",
+    transform = {
+        exact {
+            num_tasks = "num_elements",
+            num_processors = "2",
+        },
+        upper_bound {
+            max_numeric_magnitude_bits = "max_numeric_magnitude_bits + num_elements",
+        },
     }
 )]
 impl ReduceTo<MultiprocessorScheduling> for Partition {
diff --git a/src/rules/partition_sequencingtominimizetardytaskweight.rs b/src/rules/partition_sequencingtominimizetardytaskweight.rs
index 0fca17064..74eaa761e 100644
--- a/src/rules/partition_sequencingtominimizetardytaskweight.rs
+++ b/src/rules/partition_sequencingtominimizetardytaskweight.rs
@@ -60,6 +60,7 @@ impl crate::rules::AggregateReductionResult
 
 #[reduction(
     transform = exact {
+        max_processing_time_bits = "max_numeric_magnitude_bits",
         num_tasks = "num_elements",
     })]
 impl ReduceTo<Decision<SequencingToMinimizeTardyTaskWeight>> for Partition {
diff --git a/src/rules/partitionintopathsoflength2_boundedcomponentspanningforest.rs b/src/rules/partitionintopathsoflength2_boundedcomponentspanningforest.rs
index e393cd3c1..eb7778cf8 100644
--- a/src/rules/partitionintopathsoflength2_boundedcomponentspanningforest.rs
+++ b/src/rules/partitionintopathsoflength2_boundedcomponentspanningforest.rs
@@ -52,10 +52,13 @@ impl ReductionResult for ReductionPPL2ToBCSF {
 impl crate::rules::AggregateReductionResult for ReductionPPL2ToBCSF {}
 
 #[reduction(
-    transform = upper_bound {
-        num_vertices = "num_vertices",
-        num_edges = "num_edges",
-        max_components = "num_vertices / 3 + 1",
+    transform = {
+        exact { max_weight_bits = "2", },
+        upper_bound {
+            num_vertices = "num_vertices",
+            num_edges = "num_edges",
+            max_components = "num_vertices / 3 + 1",
+        },
     }
 )]
 impl ReduceTo<BoundedComponentSpanningForest<SimpleGraph, i64>>
diff --git a/src/rules/resourceconstrainedscheduling_ilp.rs b/src/rules/resourceconstrainedscheduling_ilp.rs
index 640a5af18..c4a30fb7f 100644
--- a/src/rules/resourceconstrainedscheduling_ilp.rs
+++ b/src/rules/resourceconstrainedscheduling_ilp.rs
@@ -52,38 +52,37 @@ impl ReductionResult for ReductionRCSToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionRCSToILP {}
 
-#[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "processor capacity and resource requirements and bounds are not registered source parameters",
-    },
-    exact {
-        num_vars = "num_tasks * deadline",
-        num_constraints = "num_tasks + deadline + num_resources * deadline",
-    },
-    upper_bound {
-        num_nonzeros = "(num_tasks * deadline) * (num_tasks + deadline + num_resources * deadline)",
-    },
+#[reduction(transform = upper_bound {
+    max_constraint_magnitude_bits = "max_resource_bits + num_tasks",
+    num_vars = "num_tasks^2",
+    num_constraints = "num_tasks * (num_resources + 2)",
+    num_nonzeros = "num_tasks^3 * (num_resources + 2)",
 })]
 impl ReduceTo<ILP<bool>> for ResourceConstrainedScheduling {
     type Result = ReductionRCSToILP;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let n = self.num_tasks();
-        let d =
-            usize::try_from(self.deadline()).map_err(|_| {
+        // Unit tasks can pack occupied slots without gaps; at most n slots
+        // and n processors are needed, regardless of the numeric deadline.
+        let d = usize::try_from(self.deadline())
+            .map_err(|_| {
                 crate::rules::ReductionError::invalid_target::<
                     ResourceConstrainedScheduling,
                     ILP<bool>,
                 >("deadline does not fit the structural usize domain")
-            })?;
+            })?
+            .min(n);
         let r = self.num_resources();
         let resource_requirements = self.resource_requirements();
         let resource_bounds = self.resource_bounds();
         let num_vars = n * d;
 
         let var = |j: usize, t: usize| -> usize { j * d + t };
-        let processor_count =
-            Self::exact_i64(self.num_processors(), "encoding the processor capacity")?;
+        let processor_count = Self::exact_i64(
+            self.num_processors().min(n),
+            "encoding the processor capacity",
+        )?;
 
         let mut constraints = Vec::new();
 
diff --git a/src/rules/schedulingtominimizeweightedcompletiontime_ilp.rs b/src/rules/schedulingtominimizeweightedcompletiontime_ilp.rs
index 4b47cddfa..ab3a5e2b7 100644
--- a/src/rules/schedulingtominimizeweightedcompletiontime_ilp.rs
+++ b/src/rules/schedulingtominimizeweightedcompletiontime_ilp.rs
@@ -63,14 +63,12 @@ impl ReductionResult for ReductionSMWCTToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "processing times are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_tasks * num_processors + num_tasks + num_tasks * (num_tasks - 1) / 2",
         num_constraints = "num_tasks + num_tasks * num_processors + 2 * num_tasks + 2 * num_tasks * (num_tasks - 1) / 2 * num_processors + num_tasks * (num_tasks - 1) / 2",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_processing_time_bits + num_tasks + 2",
         num_nonzeros = "(num_tasks * num_processors + num_tasks + num_tasks * (num_tasks - 1) / 2) * (num_tasks + num_tasks * num_processors + 2 * num_tasks + 2 * num_tasks * (num_tasks - 1) / 2 * num_processors + num_tasks * (num_tasks - 1) / 2)",
     },
 })]
diff --git a/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs b/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
index f95236942..ee560f5dc 100644
--- a/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
+++ b/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
@@ -46,14 +46,12 @@ impl ReductionResult for ReductionSTMMCCToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "task costs are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_tasks^2 + 1",
         num_constraints = "num_tasks^2 + 3 * num_tasks + num_precedences + 1",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_cost_bits + num_tasks",
         num_nonzeros = "(num_tasks^2 + 1) * (num_tasks^2 + 3 * num_tasks + num_precedences + 1)",
     },
 })]
diff --git a/src/rules/sequencingtominimizetardytaskweight_ilp.rs b/src/rules/sequencingtominimizetardytaskweight_ilp.rs
index 0d13e5ea8..e1f05f4bd 100644
--- a/src/rules/sequencingtominimizetardytaskweight_ilp.rs
+++ b/src/rules/sequencingtominimizetardytaskweight_ilp.rs
@@ -47,14 +47,12 @@ impl ReductionResult for ReductionSTMTTWToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "task lengths and deadlines are not registered source parameters",
-    },
     exact {
         num_vars = "num_tasks * num_tasks + num_tasks",
         num_constraints = "2 * num_tasks + 2 * num_tasks * num_tasks",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_processing_time_bits + num_tasks + 2",
         num_nonzeros = "(num_tasks * num_tasks + num_tasks) * (2 * num_tasks + 2 * num_tasks * num_tasks)",
     },
 })]
diff --git a/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs b/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
index a2e022d15..2df4c39af 100644
--- a/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
+++ b/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
@@ -52,14 +52,12 @@ impl ReductionResult for ReductionSTMWCTToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "processing times are not bounded by registered source parameters",
-    },
     exact {
         num_vars = "num_tasks + num_tasks * (num_tasks - 1) / 2",
         num_constraints = "2 * num_tasks + 3 * num_tasks * (num_tasks - 1) / 2 + num_precedences",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_processing_time_bits + num_tasks",
         num_nonzeros = "(num_tasks + num_tasks * (num_tasks - 1) / 2) * (2 * num_tasks + 3 * num_tasks * (num_tasks - 1) / 2 + num_precedences)",
     },
 })]
diff --git a/src/rules/sequencingtominimizeweightedtardiness_ilp.rs b/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
index 96316c127..62471feb0 100644
--- a/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
+++ b/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
@@ -59,13 +59,11 @@ impl crate::rules::AggregateReductionResult for ReductionSTMWTToILP {}
 
 #[reduction(
     transform = upper_bound {
+        max_constraint_magnitude_bits = "max_numeric_magnitude_bits + num_tasks",
         num_vars = "num_tasks^2 + 2 * num_tasks",
         num_constraints = "2 * num_tasks^2 + 3 * num_tasks + 1",
         num_nonzeros = "(num_tasks^2 + 2 * num_tasks) * (2 * num_tasks^2 + 3 * num_tasks + 1)",
     },
-    unavailable = {
-        max_constraint_magnitude_bits = "processing times, deadlines, weights and the cost bound are not registered source parameters",
-    },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for SequencingToMinimizeWeightedTardiness {
     type Result = ReductionSTMWTToILP;
diff --git a/src/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs b/src/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs
index 58c35b4af..3168f0f40 100644
--- a/src/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs
+++ b/src/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs
@@ -60,13 +60,11 @@ impl crate::rules::AggregateReductionResult for ReductionSWDSTToILP {}
 
 #[reduction(
     transform = upper_bound {
+        max_constraint_magnitude_bits = "max_time_bits + num_tasks + 2",
         num_vars = "2 * num_tasks^2 + num_tasks",
         num_constraints = "2 * num_tasks + num_tasks^2 * (num_tasks - 1) + 3 * num_tasks * (num_tasks - 1) + num_tasks * num_tasks",
         num_nonzeros = "(2 * num_tasks^2 + num_tasks) * (2 * num_tasks + num_tasks^2 * (num_tasks - 1) + 3 * num_tasks * (num_tasks - 1) + num_tasks * num_tasks)",
     },
-    unavailable = {
-        max_constraint_magnitude_bits = "processing times, setup times and deadlines are not registered source parameters",
-    },
 )]
 impl ReduceTo<ILP<bool>> for SequencingWithDeadlinesAndSetUpTimes {
     type Result = ReductionSWDSTToILP;
diff --git a/src/rules/shortestweightconstrainedpath_ilp.rs b/src/rules/shortestweightconstrainedpath_ilp.rs
index 423e205c2..ee645c67d 100644
--- a/src/rules/shortestweightconstrainedpath_ilp.rs
+++ b/src/rules/shortestweightconstrainedpath_ilp.rs
@@ -58,14 +58,12 @@ impl ReductionResult for ReductionSWCPToILP {
 }
 
 #[reduction(transform = {
-    unavailable {
-        max_constraint_magnitude_bits = "edge weights and the weight bound are not registered source parameters",
-    },
     exact {
         num_vars = "2 * num_edges + num_vertices",
         num_constraints = "5 * num_edges + 4 * num_vertices + 2",
     },
     upper_bound {
+        max_constraint_magnitude_bits = "max_weight_bits + num_vertices",
         num_nonzeros = "(2 * num_edges + num_vertices) * (5 * num_edges + 4 * num_vertices + 2)",
     },
 })]
diff --git a/src/rules/threedimensionalmatching_threepartition.rs b/src/rules/threedimensionalmatching_threepartition.rs
index 68262ca45..6a506ea64 100644
--- a/src/rules/threedimensionalmatching_threepartition.rs
+++ b/src/rules/threedimensionalmatching_threepartition.rs
@@ -345,6 +345,7 @@ impl crate::rules::AggregateReductionResult for ReductionThreeDimensionalMatchin
 
 #[reduction(
     transform = upper_bound {
+        max_numeric_magnitude_bits = "4 * universe_size + 36",
         num_elements = "24 * num_triples * num_triples - 3 * num_triples + 6",
         num_groups = "8 * num_triples * num_triples - num_triples + 2",
     })]
diff --git a/src/rules/threepartition_resourceconstrainedscheduling.rs b/src/rules/threepartition_resourceconstrainedscheduling.rs
index 7b4111b58..546554b23 100644
--- a/src/rules/threepartition_resourceconstrainedscheduling.rs
+++ b/src/rules/threepartition_resourceconstrainedscheduling.rs
@@ -58,6 +58,7 @@ impl crate::rules::AggregateReductionResult for ReductionThreePartitionToRCS {}
 
 #[reduction(
     transform = exact {
+        max_resource_bits = "max_numeric_magnitude_bits",
         num_tasks = "num_elements",
         deadline = "num_groups",
         num_resources = "1",
diff --git a/src/unit_tests/ilp_overhead.rs b/src/unit_tests/ilp_overhead.rs
new file mode 100644
index 000000000..205bc9a70
--- /dev/null
+++ b/src/unit_tests/ilp_overhead.rs
@@ -0,0 +1,678 @@
+//! Numeric parameter contracts and composed ILP/QUBO workflows.
+use crate::models::algebraic::{Bounded, ILP, QUBO};
+use crate::models::graph::*;
+use crate::models::misc::*;
+use crate::parameters::ParameterRelation;
+use crate::rules::{ReduceTo, ReductionGraph, ReductionPath, ReductionResult, ReductionStep};
+use crate::solvers::{BruteForce, BruteForceProblem, ILPSolver};
+use crate::topology::{DirectedGraph, SimpleGraph};
+use crate::{
+    types::{Min, One},
+    Problem,
+};
+
+type BoundedILP = ILP<i64, i64, Bounded>;
+
+fn check_contract<S: Problem + ReduceTo<T>, T: Problem>(source: &S) {
+    let target = source.reduce_to().unwrap();
+    let entry = crate::rules::registry::reduction_entries()
+        .into_iter()
+        .find(|entry| {
+            entry.source_name == S::NAME
+                && entry.target_name == T::NAME
+                && entry.source_variant() == S::variant()
+                && entry.target_variant() == T::variant()
+        })
+        .unwrap();
+    let contract = entry.parameter_contract().unwrap();
+    assert!(
+        contract.unavailable().is_empty(),
+        "{} -> {}",
+        S::NAME,
+        T::NAME
+    );
+    let transform = contract.transform().unwrap();
+    let predicted = transform.evaluate(&source.parameters()).unwrap();
+    for (field, actual) in target.target_problem().parameters().iter() {
+        let prediction = predicted.get(field).expect(field);
+        match transform.relation(field).unwrap() {
+            ParameterRelation::Exact => assert_eq!(prediction, actual, "{}: {field}", S::NAME),
+            ParameterRelation::UpperBound => assert!(
+                prediction >= actual,
+                "{}: {field}: {prediction} < {actual}",
+                S::NAME
+            ),
+        }
+    }
+}
+
+fn step<P: Problem>() -> ReductionStep {
+    ReductionStep {
+        name: P::NAME.into(),
+        variant: ReductionGraph::variant_to_map(&P::variant()),
+    }
+}
+
+fn check_qubo<S, T>(source: S)
+where
+    S: BruteForceProblem + ReduceTo<T> + 'static,
+    S::Solution: 'static,
+    S::Value: PartialEq + std::fmt::Debug + crate::types::SolutionAggregate + 'static,
+    T: Problem,
+{
+    check_contract::<S, T>(&source);
+    let mut steps = vec![step::<S>(), step::<T>()];
+    if T::variant() != ILP::<bool>::variant() {
+        steps.push(step::<ILP<bool>>());
+    }
+    steps.push(step::<QUBO<i64>>());
+    check_path(source, ReductionPath { steps });
+}
+
+fn check_path<S>(source: S, path: ReductionPath)
+where
+    S: BruteForceProblem + 'static,
+    S::Solution: 'static,
+    S::Value: PartialEq + std::fmt::Debug + crate::types::SolutionAggregate + 'static,
+{
+    let graph = ReductionGraph::new();
+    let predicted = graph
+        .compose_path_parameter_transform(&path)
+        .unwrap()
+        .unwrap()
+        .evaluate(&source.parameters())
+        .unwrap();
+    let chain = graph.reduce_along_path(&path, &source).unwrap().unwrap();
+    let target = chain.target_problem::<QUBO<i64>>();
+    for (field, actual) in target.parameters().iter() {
+        assert!(
+            predicted.get(field).expect(field) >= actual,
+            "{}: {field}",
+            S::NAME
+        );
+    }
+    let expected = BruteForce::new().solve(&source).unwrap();
+    let solution = ILPSolver::new().solve(target).unwrap();
+    let recovered = chain.extract_solution::<S::Solution, _>(&solution);
+    match expected {
+        Some(witness) => assert_eq!(
+            source.evaluate(&recovered.unwrap()).unwrap(),
+            source.evaluate(&witness).unwrap()
+        ),
+        None => assert!(recovered.is_err()),
+    }
+}
+
+#[test]
+fn capacity_assignment_magnitude_and_qubo() {
+    for (delay, budget, bits) in [
+        (0, 0, 1),
+        (7, 1, 3),
+        (8, 1, 4),
+        (1, 8, 4),
+        (-8, 1, 4),
+        (1, -8, 4),
+        (i64::MIN, 0, 64),
+        (0, i64::MIN, 64),
+        (i64::MAX, 0, 63),
+    ] {
+        let source = CapacityAssignment::new(
+            vec![i64::MAX],
+            vec![vec![i64::MAX]],
+            vec![vec![delay]],
+            budget,
+        );
+        assert_eq!(source.parameters().get("max_delay_bits"), Some(bits));
+        check_contract::<_, ILP<bool>>(&source);
+    }
+    check_contract::<_, ILP<bool>>(&CapacityAssignment::new(vec![1], vec![], vec![], 8));
+    for budget in [-3, 0, 8] {
+        check_qubo::<_, ILP<bool>>(CapacityAssignment::new(
+            vec![1, 2],
+            vec![vec![1, 3]],
+            vec![vec![2, -2]],
+            budget,
+        ));
+    }
+}
+
+#[test]
+fn partially_ordered_knapsack_magnitude_and_qubo() {
+    for (weight, capacity, bits) in [
+        (0, 0, 1),
+        (7, 1, 3),
+        (8, 1, 4),
+        (1, 8, 4),
+        (i64::MAX, 0, 63),
+        (0, i64::MAX, 63),
+    ] {
+        let source = PartiallyOrderedKnapsack::new(vec![weight], vec![i64::MAX], vec![], capacity);
+        assert_eq!(source.parameters().get("max_weight_bits"), Some(bits));
+        check_contract::<_, ILP<bool>>(&source);
+    }
+    check_contract::<_, ILP<bool>>(&PartiallyOrderedKnapsack::new(vec![], vec![], vec![], 8));
+    check_qubo::<_, ILP<bool>>(PartiallyOrderedKnapsack::new(
+        vec![2, 3],
+        vec![1, 9],
+        vec![(0, 1)],
+        3,
+    ));
+}
+
+#[test]
+fn constrained_path_magnitude_and_qubo() {
+    for (weight, bound, bits) in [
+        (1, 1, 1),
+        (8, 1, 4),
+        (1, 8, 4),
+        (i64::MAX, 1, 63),
+        (1, i64::MAX, 63),
+    ] {
+        let source = ShortestWeightConstrainedPath::new(
+            SimpleGraph::path(2),
+            vec![i64::MAX],
+            vec![weight],
+            0,
+            1,
+            bound,
+        );
+        assert_eq!(source.parameters().get("max_weight_bits"), Some(bits));
+        check_contract::<_, BoundedILP>(&source);
+    }
+    check_contract::<_, BoundedILP>(&ShortestWeightConstrainedPath::<_, i64>::new(
+        SimpleGraph::empty(8),
+        vec![],
+        vec![],
+        0,
+        0,
+        1,
+    ));
+    for bound in [1, 2] {
+        check_qubo::<_, BoundedILP>(ShortestWeightConstrainedPath::new(
+            SimpleGraph::path(2),
+            vec![3],
+            vec![2],
+            0,
+            1,
+            bound,
+        ));
+    }
+}
+
+#[test]
+fn bounded_forest_magnitude_and_incoming_qubo() {
+    for (weights, bound, bits) in [
+        (vec![], 8, 4),
+        (vec![8], 1, 4),
+        (vec![1], 8, 4),
+        (vec![i64::MAX], 1, 63),
+        (vec![1], i64::MAX, 63),
+        (vec![0; 8], 1, 1),
+    ] {
+        let source = BoundedComponentSpanningForest::new(
+            SimpleGraph::empty(weights.len()),
+            weights,
+            1,
+            bound,
+        );
+        assert_eq!(source.parameters().get("max_weight_bits"), Some(bits));
+        check_contract::<_, BoundedILP>(&source);
+    }
+    check_qubo::<_, BoundedILP>(BoundedComponentSpanningForest::new(
+        SimpleGraph::path(2),
+        vec![1, 1],
+        1,
+        2,
+    ));
+    for graph in [SimpleGraph::empty(0), SimpleGraph::empty(3)] {
+        let source = PartitionIntoPathsOfLength2::new(graph);
+        check_contract::<_, BoundedComponentSpanningForest<SimpleGraph, i64>>(&source);
+        check_path(
+            source,
+            ReductionPath {
+                steps: vec![
+                    step::<PartitionIntoPathsOfLength2<SimpleGraph>>(),
+                    step::<BoundedComponentSpanningForest<SimpleGraph, i64>>(),
+                    step::<BoundedILP>(),
+                    step::<ILP<bool>>(),
+                    step::<QUBO<i64>>(),
+                ],
+            },
+        );
+    }
+}
+
+#[test]
+fn acyclic_partition_magnitude_and_qubo() {
+    for (weight, bound, bits) in [(0, 1, 1), (8, 1, 4), (1, -8, 4), (i64::MIN, 1, 64)] {
+        let source = AcyclicPartition::new(DirectedGraph::empty(1), vec![weight], vec![], bound, 0);
+        assert_eq!(
+            source.parameters().get("max_numeric_magnitude_bits"),
+            Some(bits)
+        );
+        check_contract::<_, ILP<bool>>(&source);
+    }
+    check_contract::<_, ILP<bool>>(&AcyclicPartition::new(
+        DirectedGraph::new(1, vec![(0, 0)]),
+        vec![1],
+        vec![1],
+        1,
+        1,
+    ));
+    for bound in [1, 3] {
+        check_qubo::<_, ILP<bool>>(AcyclicPartition::new(
+            DirectedGraph::new(2, vec![(0, 1)]),
+            vec![1, 2],
+            vec![1],
+            bound,
+            0,
+        ));
+    }
+    use crate::models::formula::{CNFClause, KSatisfiability};
+    use crate::variant::K3;
+    for clauses in [
+        vec![],
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, -1, -1]),
+        ],
+        vec![CNFClause::new(vec![1, 1, 1])],
+    ] {
+        check_contract::<_, AcyclicPartition<i64>>(&KSatisfiability::<K3>::new(1, clauses));
+    }
+}
+
+#[test]
+fn branching_magnitude_and_qubo() {
+    for (weight, threshold, bits) in [(1, 8, 4), (8, 1, 4), (i64::MIN, 0, 64), (1, i64::MIN, 64)] {
+        let source = MultipleChoiceBranching::new(
+            DirectedGraph::new(2, vec![(0, 1)]),
+            vec![weight],
+            vec![vec![0]],
+            threshold,
+        );
+        assert_eq!(source.parameters().get("max_weight_bits"), Some(bits));
+        check_contract::<_, BoundedILP>(&source);
+    }
+    for threshold in [1, 3] {
+        check_qubo::<_, BoundedILP>(MultipleChoiceBranching::new(
+            DirectedGraph::new(2, vec![(0, 1)]),
+            vec![2],
+            vec![vec![0]],
+            threshold,
+        ));
+    }
+}
+
+#[test]
+fn capacitated_tree_magnitude_and_qubo() {
+    let source = MinimumCapacitatedSpanningTree::new(
+        SimpleGraph::path(3),
+        vec![i64::MAX; 2],
+        0,
+        vec![0, 7, 7],
+        8,
+    );
+    assert_eq!(source.parameters().get("max_requirement_bits"), Some(4));
+    check_contract::<_, BoundedILP>(&source);
+    for capacity in [1, 2] {
+        check_qubo::<_, BoundedILP>(MinimumCapacitatedSpanningTree::new(
+            SimpleGraph::path(2),
+            vec![3],
+            0,
+            vec![0, 2],
+            capacity,
+        ));
+    }
+}
+
+#[test]
+fn multicenter_magnitude_products_and_qubo() {
+    let source = MinMaxMulticenter::new(SimpleGraph::path(3), vec![8; 3], vec![8; 2], 1);
+    assert_eq!(
+        source.parameters().get("max_numeric_magnitude_bits"),
+        Some(4)
+    );
+    check_contract::<_, BoundedILP>(&source);
+    for graph in [SimpleGraph::path(2), SimpleGraph::empty(2)] {
+        let lengths = vec![2; crate::topology::Graph::num_edges(&graph)];
+        check_qubo::<_, BoundedILP>(MinMaxMulticenter::new(graph, vec![2, 1], lengths, 1));
+    }
+}
+
+#[test]
+fn multicenter_distance_overflow_is_typed() {
+    let source = MinMaxMulticenter::new(SimpleGraph::path(3), vec![1; 3], vec![i64::MAX; 2], 1);
+    assert!(matches!(
+        source.evaluate(&vec![true, false, false]),
+        Err(crate::traits::EvaluationError::IntegerOverflow(_))
+    ));
+    assert!(matches!(
+        ReduceTo::<BoundedILP>::reduce_to(&source),
+        Err(crate::rules::ReductionError::IntegerOverflow { .. })
+    ));
+}
+
+#[test]
+fn flow_shop_magnitude_and_qubo() {
+    for (time, deadline, bits) in [(1, 8, 4), (8, 1, 4), (0, 0, 1), (7, 7, 3)] {
+        let source = FlowShopScheduling::new(1, vec![vec![time]; 2], deadline);
+        assert_eq!(source.parameters().get("max_time_bits"), Some(bits));
+        check_contract::<_, BoundedILP>(&source);
+    }
+    check_contract::<_, BoundedILP>(&FlowShopScheduling::new(0, vec![vec![]; 2], 8));
+    for deadline in [1, 2] {
+        check_qubo::<_, BoundedILP>(FlowShopScheduling::new(1, vec![vec![1]; 2], deadline));
+    }
+}
+
+#[test]
+fn minimum_tardiness_negative_deadlines_preserve_optimum() {
+    // Every schedule has exactly one tardy task, even for the smallest deadline.
+    for deadline in [-1, i64::MIN] {
+        let source = MinimumTardinessSequencing::<One>::new(1, vec![deadline], vec![]);
+        assert_eq!(source.evaluate(&vec![0]).unwrap(), Min(Some(1)));
+        let reduced = ReduceTo::<ILP<bool>>::reduce_to(&source).unwrap();
+        let witness = ILPSolver::new().solve(reduced.target_problem()).unwrap();
+        assert_eq!(
+            source
+                .evaluate(&reduced.extract_solution(&witness).unwrap())
+                .unwrap(),
+            Min(Some(1))
+        );
+        let source =
+            MinimumTardinessSequencing::<i64>::with_lengths(vec![2], vec![deadline], vec![]);
+        let reduced = ReduceTo::<ILP<bool>>::reduce_to(&source).unwrap();
+        let witness = ILPSolver::new().solve(reduced.target_problem()).unwrap();
+        assert_eq!(
+            source
+                .evaluate(&reduced.extract_solution(&witness).unwrap())
+                .unwrap(),
+            Min(Some(1))
+        );
+    }
+}
+
+#[test]
+fn minimum_tardiness_magnitude_and_qubo() {
+    for deadline in [i64::MIN, 0, i64::MAX] {
+        check_qubo::<_, ILP<bool>>(MinimumTardinessSequencing::<One>::new(
+            2,
+            vec![deadline, 1],
+            vec![(0, 1)],
+        ));
+        let source = MinimumTardinessSequencing::<i64>::with_lengths(
+            vec![2, 1],
+            vec![deadline, 2],
+            vec![(0, 1)],
+        );
+        assert_eq!(source.parameters().get("max_processing_time_bits"), Some(2));
+        check_qubo::<_, ILP<bool>>(source);
+    }
+}
+
+#[test]
+fn completion_time_magnitude_and_qubo() {
+    let source = SchedulingToMinimizeWeightedCompletionTime::new(vec![7, 7], vec![i64::MAX; 2], 2);
+    assert_eq!(source.parameters().get("max_processing_time_bits"), Some(3));
+    check_contract::<_, BoundedILP>(&source);
+    check_qubo::<_, BoundedILP>(SchedulingToMinimizeWeightedCompletionTime::new(
+        vec![1, 2],
+        vec![2, 1],
+        2,
+    ));
+    let source =
+        SequencingToMinimizeWeightedCompletionTime::new(vec![7, 7], vec![i64::MAX; 2], vec![]);
+    assert_eq!(source.parameters().get("max_processing_time_bits"), Some(3));
+    check_contract::<_, BoundedILP>(&source);
+    check_qubo::<_, BoundedILP>(SequencingToMinimizeWeightedCompletionTime::new(
+        vec![1, 2],
+        vec![1, 2],
+        vec![(0, 1)],
+    ));
+    let source = OptimalLinearArrangement::new(SimpleGraph::path(2));
+    check_contract::<_, SequencingToMinimizeWeightedCompletionTime>(&source);
+    check_path(
+        source,
+        ReductionPath {
+            steps: vec![
+                step::<OptimalLinearArrangement<SimpleGraph>>(),
+                step::<SequencingToMinimizeWeightedCompletionTime>(),
+                step::<BoundedILP>(),
+                step::<ILP<bool>>(),
+                step::<QUBO<i64>>(),
+            ],
+        },
+    );
+}
+
+#[test]
+fn cumulative_cost_magnitude_and_qubo() {
+    let source = SequencingToMinimizeMaximumCumulativeCost::new(vec![-8, 8], vec![]);
+    assert_eq!(source.parameters().get("max_cost_bits"), Some(4));
+    check_contract::<_, BoundedILP>(&source);
+    for costs in [vec![-2, 3], vec![-2, -1], vec![]] {
+        check_qubo::<_, BoundedILP>(SequencingToMinimizeMaximumCumulativeCost::new(
+            costs,
+            vec![],
+        ));
+    }
+}
+
+#[test]
+fn tardy_task_weight_magnitude_and_incoming_qubo() {
+    for deadlines in [vec![i64::MIN; 2], vec![i64::MAX; 2]] {
+        let source = SequencingToMinimizeTardyTaskWeight::new(vec![-1, 2], vec![1, -1], deadlines);
+        assert_eq!(source.parameters().get("max_processing_time_bits"), Some(2));
+        check_qubo::<_, ILP<bool>>(source);
+    }
+    use crate::models::Decision;
+    let source = Partition::new(vec![1, 1]).unwrap();
+    check_contract::<_, Decision<SequencingToMinimizeTardyTaskWeight>>(&source);
+    check_path(
+        source,
+        ReductionPath {
+            steps: vec![
+                step::<Partition>(),
+                step::<Decision<SequencingToMinimizeTardyTaskWeight>>(),
+                step::<SequencingToMinimizeTardyTaskWeight>(),
+                step::<ILP<bool>>(),
+                step::<QUBO<i64>>(),
+            ],
+        },
+    );
+}
+
+#[test]
+fn weighted_tardiness_magnitude_and_qubo() {
+    for (length, weight, deadline, bound) in
+        [(8, 1, 1, 1), (1, 8, 1, 1), (1, 1, 8, 1), (1, 1, 1, 8)]
+    {
+        let source = SequencingToMinimizeWeightedTardiness::new(
+            vec![length],
+            vec![weight],
+            vec![deadline],
+            bound,
+        );
+        assert_eq!(
+            source.parameters().get("max_numeric_magnitude_bits"),
+            Some(4)
+        );
+        check_contract::<_, BoundedILP>(&source);
+    }
+    for bound in [0, 2] {
+        check_qubo::<_, BoundedILP>(SequencingToMinimizeWeightedTardiness::new(
+            vec![2],
+            vec![1],
+            vec![1],
+            bound,
+        ));
+    }
+}
+
+#[test]
+fn setup_time_magnitude_and_qubo() {
+    for (length, deadline, setup) in [(8, 1, 1), (1, 8, 1), (1, 1, 8)] {
+        let source = SequencingWithDeadlinesAndSetUpTimes::new(
+            vec![length; 2],
+            vec![deadline; 2],
+            vec![0, 1],
+            vec![setup; 2],
+        );
+        assert_eq!(source.parameters().get("max_time_bits"), Some(4));
+        check_contract::<_, ILP<bool>>(&source);
+    }
+    for deadline in [2, 3] {
+        check_qubo::<_, ILP<bool>>(SequencingWithDeadlinesAndSetUpTimes::new(
+            vec![1; 2],
+            vec![deadline; 2],
+            vec![0, 1],
+            vec![1; 2],
+        ));
+    }
+}
+
+#[test]
+fn resource_scheduling_packs_slots_and_ignores_excess_processors() {
+    let source = ResourceConstrainedScheduling::new(2, vec![2], vec![vec![1]; 2], 1000).unwrap();
+    let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source).unwrap();
+    assert!(reduction.target_problem().num_vars() <= 4);
+    // These instances must not allocate or iterate through the numeric deadline.
+    let source =
+        ResourceConstrainedScheduling::new(usize::MAX, vec![2], vec![vec![1]; 2], i64::MAX)
+            .unwrap();
+    let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source).unwrap();
+    assert!(reduction.target_problem().num_vars() <= 4);
+    assert!(
+        source
+            .evaluate(&vec![0, (i64::MAX - 1) as usize])
+            .unwrap()
+            .0
+    );
+    let witness = ILPSolver::new().solve(reduction.target_problem()).unwrap();
+    assert!(
+        source
+            .evaluate(&reduction.extract_solution(&witness).unwrap())
+            .unwrap()
+            .0
+    );
+    let empty = ResourceConstrainedScheduling::new(0, vec![0], vec![], i64::MAX).unwrap();
+    assert!(empty.evaluate(&vec![]).unwrap().0);
+    assert_eq!(
+        ReduceTo::<ILP<bool>>::reduce_to(&empty)
+            .unwrap()
+            .target_problem()
+            .num_vars(),
+        0
+    );
+}
+
+#[test]
+fn resource_magnitude_and_incoming_predictions() {
+    for (requirement, bound, bits) in [
+        (0, 0, 1),
+        (8, 1, 4),
+        (1, 8, 4),
+        (i64::MAX, 0, 63),
+        (0, i64::MAX, 63),
+    ] {
+        let source =
+            ResourceConstrainedScheduling::new(2, vec![bound], vec![vec![requirement]], 2).unwrap();
+        assert_eq!(source.parameters().get("max_resource_bits"), Some(bits));
+        check_contract::<_, ILP<bool>>(&source);
+    }
+    for processors in [0, 1, 2] {
+        check_qubo::<_, ILP<bool>>(
+            ResourceConstrainedScheduling::new(processors, vec![1], vec![vec![1]; 2], 2).unwrap(),
+        );
+    }
+    let source = ThreePartition::new(vec![1; 3], 3);
+    check_contract::<_, ResourceConstrainedScheduling>(&source);
+    check_path(
+        source,
+        ReductionPath {
+            steps: vec![
+                step::<ThreePartition>(),
+                step::<ResourceConstrainedScheduling>(),
+                step::<ILP<bool>>(),
+                step::<QUBO<i64>>(),
+            ],
+        },
+    );
+    use crate::models::set::ThreeDimensionalMatching;
+    for (size, triples) in [
+        (0, vec![]),
+        (1, vec![]),
+        (1, vec![(0, 0, 0)]),
+        (2, vec![(0, 0, 0), (1, 1, 1)]),
+    ] {
+        let source = ThreeDimensionalMatching::new(size, triples);
+        check_contract::<_, ThreePartition>(&source);
+        let path = ReductionPath {
+            steps: vec![
+                step::<ThreeDimensionalMatching>(),
+                step::<ThreePartition>(),
+                step::<ResourceConstrainedScheduling>(),
+                step::<ILP<bool>>(),
+                step::<QUBO<i64>>(),
+            ],
+        };
+        let predicted = ReductionGraph::new()
+            .compose_path_parameter_transform(&path)
+            .unwrap()
+            .unwrap()
+            .evaluate(&source.parameters())
+            .unwrap();
+        assert!(predicted.get("num_vars").is_some());
+        assert!(predicted.get("num_quadratic_terms").is_some());
+    }
+}
+
+#[test]
+fn circuit_threshold_normalization_and_incoming_qubo() {
+    use crate::models::Decision;
+    for threshold in [i64::MIN, 0, 3, 4, i64::MAX] {
+        let source = Decision::new(
+            LongestCircuit::new(SimpleGraph::cycle(3), vec![1i64; 3]),
+            threshold,
+        );
+        assert_eq!(source.parameters().get("max_length_bits"), Some(1));
+        check_contract::<_, ILP<bool>>(&source);
+        let reduced = ReduceTo::<ILP<bool>>::reduce_to(&source).unwrap();
+        assert!(reduced.target_problem().max_constraint_magnitude_bits() <= 5);
+        assert_eq!(
+            ILPSolver::new().solve(reduced.target_problem()).is_ok(),
+            threshold <= 3
+        );
+    }
+    let source = HamiltonianCircuit::new(SimpleGraph::cycle(3));
+    check_contract::<_, Decision<LongestCircuit<SimpleGraph, i64>>>(&source);
+    check_path(
+        source,
+        ReductionPath {
+            steps: vec![
+                step::<HamiltonianCircuit<SimpleGraph>>(),
+                step::<Decision<LongestCircuit<SimpleGraph, i64>>>(),
+                step::<ILP<bool>>(),
+                step::<QUBO<i64>>(),
+            ],
+        },
+    );
+}
+
+#[test]
+fn multiprocessor_predictions_compose_and_recover_through_qubo() {
+    for sizes in [vec![1, 1], vec![3; 4], vec![1, 2], vec![2]] {
+        check_path(
+            Partition::new(sizes).unwrap(),
+            ReductionPath {
+                steps: vec![
+                    step::<Partition>(),
+                    step::<MultiprocessorScheduling>(),
+                    step::<ILP<bool>>(),
+                    step::<QUBO<i64>>(),
+                ],
+            },
+        );
+    }
+}
diff --git a/src/unit_tests/models/graph/acyclic_partition.rs b/src/unit_tests/models/graph/acyclic_partition.rs
index 85dd33d8b..1d00e1008 100644
--- a/src/unit_tests/models/graph/acyclic_partition.rs
+++ b/src/unit_tests/models/graph/acyclic_partition.rs
@@ -243,7 +243,10 @@ fn test_acyclic_partition_declares_problem_parameters() {
         .iter()
         .copied()
         .collect();
-    assert_eq!(fields, HashSet::from(["num_vertices", "num_arcs"]));
+    assert_eq!(
+        fields,
+        HashSet::from(["num_vertices", "num_arcs", "max_numeric_magnitude_bits"])
+    );
 }
 #[test]
 fn create_spec_maps_weight_inputs_to_canonical_fields() {
diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs
index 032f525d6..f3bbca2af 100644
--- a/src/unit_tests/reduction_graph.rs
+++ b/src/unit_tests/reduction_graph.rs
@@ -37,30 +37,21 @@ fn domination_magnitude_predictions_account_for_parallel_edges() {
 }
 
 #[test]
-fn decision_ilp_contracts_distinguish_bounded_and_unrepresented_numeric_data() {
-    for (name, magnitude_available) in [
-        ("DecisionLongestCircuit", false),
-        ("DecisionOpenShopScheduling", true),
-    ] {
+fn decision_ilp_contracts_cover_numeric_bounds() {
+    for name in ["DecisionLongestCircuit", "DecisionOpenShopScheduling"] {
         let entry = crate::rules::registry::reduction_entries()
             .into_iter()
             .find(|entry| entry.source_name == name && entry.target_name == "ILP")
             .unwrap();
         let contract = entry.parameter_contract().unwrap();
         let transform = contract.transform().unwrap();
-        assert_eq!(
-            contract
-                .unavailable()
-                .iter()
-                .any(|field| field.field == "max_constraint_magnitude_bits"),
-            !magnitude_available,
-            "{name}"
-        );
-        assert_eq!(
-            transform.get("max_constraint_magnitude_bits").is_some(),
-            magnitude_available
-        );
-        for field in ["num_vars", "num_constraints", "num_nonzeros"] {
+        assert!(contract.unavailable().is_empty(), "{name}");
+        for field in [
+            "max_constraint_magnitude_bits",
+            "num_vars",
+            "num_constraints",
+            "num_nonzeros",
+        ] {
             assert!(transform.get(field).is_some(), "{name}: {field}");
         }
     }
diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs
index e7e0ee35a..a979f536b 100644
--- a/src/unit_tests/symbolic_parameter_contracts.rs
+++ b/src/unit_tests/symbolic_parameter_contracts.rs
@@ -441,6 +441,42 @@ fn exact_parameter_formulas_cover_sparse_and_boundary_instances() {
         .any(|field| field.field == "num_edges"));
 }
 
+#[test]
+fn multiprocessor_magnitude_predictions_cover_lengths_and_deadlines() {
+    use crate::models::algebraic::ILP;
+    use crate::models::misc::{MultiprocessorScheduling, Partition};
+
+    for (lengths, deadline, bits) in [
+        (vec![], 0, 1),
+        (vec![], 8, 4),
+        (vec![0], 0, 1),
+        (vec![7], 1, 3),
+        (vec![8], 1, 4),
+        (vec![1], 8, 4),
+        (vec![i64::MAX], 0, 63),
+        (vec![0], i64::MAX, 63),
+    ] {
+        let source = MultiprocessorScheduling::new(lengths, 2, deadline);
+        assert_eq!(
+            source.parameters().get("max_numeric_magnitude_bits"),
+            Some(bits)
+        );
+        check_reduced_parameters::<_, ILP<bool>>(
+            source,
+            &["max_constraint_magnitude_bits"],
+            ParameterRelation::Exact,
+        );
+    }
+    // The deadline can require more bits than any individual input size.
+    for sizes in [vec![1], vec![3; 4], vec![1, 2], vec![i64::MAX]] {
+        check_reduced_parameters::<_, MultiprocessorScheduling>(
+            Partition::new(sizes).unwrap(),
+            &["num_tasks", "num_processors"],
+            ParameterRelation::Exact,
+        );
+    }
+}
+
 #[test]
 fn augmentation_magnitude_predictions_cover_weights_and_budgets() {
     use crate::models::algebraic::ILP;