We have merged #244 to upgrade integer types used in OPB (Pseudo-Boolean) file parsing from int to int64_t to support larger coefficient and cost values that may exceed 32-bit integer limits.
I asked Claude Code to perform additional analysis on the code to identify any cases where bit width might increase during preprocessing. The results are as follows. We may need to check the handling of soft constraints.
Background
OPB/WBO files declare intsize, defined per spec as:
intsize = max_i (1 + ⌊log2(|d_i| + Σ_j |c^i_j|)⌋)
i.e., the bit width needed to hold |degree| + sum of |coefficients| for any constraint. A solver using ≥ intsize-bit unsigned (or intsize+1-bit signed) integers will not overflow when naively summing coefficients of true literals minus the degree.
PRINTEMPS performs internal computation in IEEE 754 double, which represents integers exactly only up to 2⁵³. We currently reject files with intsize > 53. The question is whether PRINTEMPS preprocessing can produce intermediate values that exceed 2⁵³ even when the input satisfies intsize ≤ 53.
Findings
Preprocessing that does NOT grow coefficients
-
problem_size_reducer (preprocess/problem_size_reducer.h)
- Only fixes variables or tightens variable bounds.
- Does not modify any coefficient. Safe.
-
gf2_solver (preprocess/gf2_solver.h)
- Only fixes binary variables via GF(2) Gaussian elimination.
- Does not modify coefficients. Safe.
-
dependent_variable_extractor + Expression::solve() / Expression::substitute() (preprocess/dependent_variable_extractor.h, model_component/expression.h:334-357)
solve() divides by the key variable's coefficient; substitute(v, e) performs this += sensitivities[v] * e, which is a coefficient-by-coefficient product.
- In principle this could multiply two arbitrary coefficients and explode.
- However,
Constraint::categorize() (model_component/constraint.h) only sets key_variable_ptr for patterns where the key variable's coefficient is ±1:
- Binary XOR / XNOR (lines 317–333): all coefficients ±1.
- Integer
constant_ratio / intermediate (lines 380–401): key coefficient ±1.
- Soft selection (lines 606–612): key coefficient ±1.
- For PB problems (all variables binary), only the XOR/XNOR and soft-selection cases apply, both with key coefficient ±1.
- Therefore
1.0 / ±1 = ±1 and substitution does not grow coefficients. Safe for PB.
Preprocessing that DOES grow coefficients
Model::import_opb soft-constraint transformation (model/model.h:3811-3886)
A soft constraint Σ c_i x_i ≤ rhs is rewritten as a hard constraint:
expression - UPPER_BOUND * slack ≤ 0
where expression = Σ c_i x_i - rhs
UPPER_BOUND = expression.upper_bound()
= Σ_{c_i > 0} c_i - rhs (bounded by Σ|c_i| + |rhs|)
The transformed constraint's "intsize" in the spec's sense is:
- before:
Σ|c_i| + |rhs| < 2^intsize
- after:
Σ|c_i| + |rhs| + |UPPER_BOUND| ≤ 2 * (Σ|c_i| + |rhs|) < 2^(intsize+1)
Consequence: an input with intsize = 53 can produce a post-transform effective intsize of 54, breaking exact representability in double.
Objective penalty accumulation (model/model.h:3893-3914)
objective_penalty += SOFT_CONSTRAINT.weight * slack
Summed over all soft constraints, the maximum value is sumcost (a WBO metadata field). If sumcost > 2⁵³, the objective value cannot be represented exactly in double, regardless of intsize.
shrink_global_penalty_coefficient (model/model.h:1626-1651)
Uses objective.expression().upper_bound() - lower_bound() + 1.0. Each of upper_bound / lower_bound is a single double summed from coefficients, bounded by ~2^intsize. The subtraction is ≤ 2 * 2^intsize = 2^(intsize+1). Stored as a double constant (no precision loss in storage at this magnitude), but used downstream as a penalty multiplier.
Summary table
| Component |
Operation |
Coefficient growth |
Risk for intsize ≤ 53 |
problem_size_reducer |
fix/bound variables |
none |
none |
gf2_solver |
fix variables |
none |
none |
dependent_variable_extractor (PB) |
substitute with ±1 key coef |
none |
none |
import_opb (hard only) |
expression -= rhs |
none |
none |
import_opb (soft → hard) |
introduces UPPER_BOUND * slack |
+1 bit |
intsize=53 → effective 54 |
import_opb (soft → objective) |
Σ weight_i * slack_i |
up to sumcost |
if sumcost > 2⁵³ |
Implications for the intsize > 53 UNSUPPORTED threshold
- Pure OPB (no soft constraints):
intsize ≤ 53 is correct and tight. Preprocessing does not push magnitudes past 2⁵³.
- WBO (soft constraints present):
intsize ≤ 53 is not sufficient.
- Soft → hard transformation may push effective intsize to 54.
- Independently,
sumcost > 2⁵³ makes objective evaluation imprecise.
Possible mitigations
- Option A — Uniformly conservative: reject
intsize > 52 regardless of file type.
- Simple, safe; rejects some valid pure-OPB files with
intsize = 53.
- Option B — File-type-aware:
- pure OPB:
intsize > 53 → UNSUPPORTED.
- WBO:
intsize > 52 → UNSUPPORTED and sumcost > 2⁵³ → UNSUPPORTED.
- Tighter, but more complex; the
OPB::check_metadata path runs before read_opb, so the soft-constraint presence has to be inferred from metadata (#soft=) or the full read.
- Option C — Option A + sumcost guard:
intsize > 52 → UNSUPPORTED, plus sumcost > 2⁵³ → UNSUPPORTED for WBO. Simple and covers both risks.
Open questions / caveats
- Does the OPB/WBO competition spec impose constraints on
sumcost analogous to intsize? If sumcost ≤ 2^intsize is guaranteed by the spec, the dedicated sumcost check is redundant. (Not verified from the spec text the user shared.)
- The soft → hard transformation always adds exactly one slack term per constraint, so the +1 bit growth is a sharp bound — there is no additional accumulation beyond that.
- All non-soft preprocessing paths are safe for PB because all variables are binary; if PRINTEMPS is later used with integer variables of larger bounds, the
dependent_variable_extractor analysis would need to be revisited (constant_ratio_integers, intermediate, etc., can substitute with non-±1 effective scaling once mapped through variable bounds, though the key variable's coefficient is still ±1).
We have merged #244 to upgrade integer types used in OPB (Pseudo-Boolean) file parsing from
inttoint64_tto support larger coefficient and cost values that may exceed 32-bit integer limits.I asked Claude Code to perform additional analysis on the code to identify any cases where bit width might increase during preprocessing. The results are as follows. We may need to check the handling of soft constraints.
Background
OPB/WBO files declare
intsize, defined per spec as:i.e., the bit width needed to hold
|degree| + sum of |coefficients|for any constraint. A solver using ≥intsize-bit unsigned (orintsize+1-bit signed) integers will not overflow when naively summing coefficients of true literals minus the degree.PRINTEMPS performs internal computation in IEEE 754
double, which represents integers exactly only up to 2⁵³. We currently reject files withintsize > 53. The question is whether PRINTEMPS preprocessing can produce intermediate values that exceed 2⁵³ even when the input satisfiesintsize ≤ 53.Findings
Preprocessing that does NOT grow coefficients
problem_size_reducer(preprocess/problem_size_reducer.h)gf2_solver(preprocess/gf2_solver.h)dependent_variable_extractor+Expression::solve()/Expression::substitute()(preprocess/dependent_variable_extractor.h,model_component/expression.h:334-357)solve()divides by the key variable's coefficient;substitute(v, e)performsthis += sensitivities[v] * e, which is a coefficient-by-coefficient product.Constraint::categorize()(model_component/constraint.h) only setskey_variable_ptrfor patterns where the key variable's coefficient is ±1:constant_ratio/intermediate(lines 380–401): key coefficient ±1.1.0 / ±1 = ±1and substitution does not grow coefficients. Safe for PB.Preprocessing that DOES grow coefficients
Model::import_opbsoft-constraint transformation (model/model.h:3811-3886)A soft constraint
Σ c_i x_i ≤ rhsis rewritten as a hard constraint:The transformed constraint's "intsize" in the spec's sense is:
Σ|c_i| + |rhs| < 2^intsizeΣ|c_i| + |rhs| + |UPPER_BOUND| ≤ 2 * (Σ|c_i| + |rhs|) < 2^(intsize+1)Consequence: an input with
intsize = 53can produce a post-transform effective intsize of 54, breaking exact representability indouble.Objective penalty accumulation (
model/model.h:3893-3914)Summed over all soft constraints, the maximum value is
sumcost(a WBO metadata field). Ifsumcost > 2⁵³, the objective value cannot be represented exactly indouble, regardless ofintsize.shrink_global_penalty_coefficient(model/model.h:1626-1651)Uses
objective.expression().upper_bound() - lower_bound() + 1.0. Each ofupper_bound/lower_boundis a single double summed from coefficients, bounded by~2^intsize. The subtraction is ≤2 * 2^intsize = 2^(intsize+1). Stored as a double constant (no precision loss in storage at this magnitude), but used downstream as a penalty multiplier.Summary table
intsize ≤ 53problem_size_reducergf2_solverdependent_variable_extractor(PB)import_opb(hard only)expression -= rhsimport_opb(soft → hard)UPPER_BOUND * slackimport_opb(soft → objective)Σ weight_i * slack_isumcostsumcost > 2⁵³Implications for the
intsize > 53UNSUPPORTED thresholdintsize ≤ 53is correct and tight. Preprocessing does not push magnitudes past 2⁵³.intsize ≤ 53is not sufficient.sumcost > 2⁵³makes objective evaluation imprecise.Possible mitigations
intsize > 52regardless of file type.intsize = 53.intsize > 53→ UNSUPPORTED.intsize > 52→ UNSUPPORTED andsumcost > 2⁵³→ UNSUPPORTED.OPB::check_metadatapath runs beforeread_opb, so the soft-constraint presence has to be inferred from metadata (#soft=) or the full read.intsize > 52→ UNSUPPORTED, plussumcost > 2⁵³→ UNSUPPORTED for WBO. Simple and covers both risks.Open questions / caveats
sumcostanalogous tointsize? Ifsumcost ≤ 2^intsizeis guaranteed by the spec, the dedicatedsumcostcheck is redundant. (Not verified from the spec text the user shared.)dependent_variable_extractoranalysis would need to be revisited (constant_ratio_integers,intermediate, etc., can substitute with non-±1 effective scaling once mapped through variable bounds, though the key variable's coefficient is still ±1).