Conversation
isPANN
added this pull request to stack #1181
September 27, 2026 16:56
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## fix/exact-reduction-parameters #1180 +/- ##
==================================================================
+ Coverage 96.75% 96.76% +0.01%
==================================================================
Files 1070 1072 +2
Lines 139440 140453 +1013
==================================================================
+ Hits 134914 135911 +997
- Misses 4526 4542 +16 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Propagate magnitude bounds through incoming reductions, normalize irrelevant thresholds, and restore composable size predictions with explicit rule-local contracts. Add magnitude parameters for BinPacking, Partition, and SubsetSum and verify composed reductions through QUBO.
…al ILP Encode cluster membership with pair variables and degree constraints. Preserve optimal edge deletion, declare composable polynomial size bounds, and remove obsolete subset-enumeration helpers. Update the proof and verify exhaustive small graphs, decoding, large graph construction, and QUBO recovery.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
While investigating unavailable predictions along ILP → binary ILP → QUBO paths, we found a more fundamental problem: the registered integer-to-binary edge did not express its mathematical precondition. It accepted general
ILP<i64>in the graph, but its implementation required explicit finite lower and upper bounds for every variable. Path discovery could therefore advertise a route that failed when constructed. Improving parameter formulas alone cannot repair that mismatch.The reduction graph must describe applicability independently of backend realization. General integer ILP permits infinite variable intervals, and constraints may imply bounds without storing them explicitly. A backend's ability to solve that instance or discover bounds should not determine whether this encoding edge exists. Each rule needs an explicit, local source contract that future rules can rely on.
This PR makes that contract a separate bounds dimension: binary encoding starts from
ILP<i64, i64, Bounded>, whose constructor validates finite endpoints. General ILP remains the default. Because ILP represents optimization, restricting its domain must preserve the optimum; silently imposing an arbitrary finite search range would be incorrect.Incoming reductions also need to retain the domain guarantees they already establish. Rules constructing finite integer intervals now target bounded ILP, and rules using only binary variables target binary ILP directly. This preserves valid downstream encoding paths. A bounded → general embedding retains the full instance for rules that accept general ILP.
Summary
Add
ILP<V, C, B = General>, register only the needed bounded integer variant, migrate the affected graph edges and incoming rules, and update solver dispatch, CLI handling, examples, and documentation. The PR also restores composable ILP size predictions using intrinsic magnitude parameters and rule-local formulas, and normalizes input thresholds where their original magnitude is irrelevant.This PR is stacked on #1174 (
fix/exact-reduction-parameters). The comparison contains the bounded-ILP migration and the related parameter-prediction fixes; retarget tomainafter that dependency lands.Resolution of #1176
This PR and its dependency #1174 together resolve #1176: reductions that stored bounds only as constraint rows produced integer ILP instances that the binary encoder could not encode.
ILP::with_variablesand adds a registry-wide encoding regression test plus a feedback-arc-set → integer ILP → binary ILP → QUBO solution-recovery test.The regression test checks every registered incoming bounded-ILP edge using a representative source instance. Both PRs must land before closing #1176. This resolves the missing-domain failure; it does not make every symbolic parameter prediction available.
API and graph changes
Before/after comparisons below are based on the comparison branch's source and the regression tests.
ILP<V, C>ILP<V, C, B = General>ILP<i64, i64, Bounded>; construction and deserialization enforce finite endpointsILP<bool>; 38 problem edges target bounded integer ILPOmitted bounds always mean
general, includingILP<bool>. Binary variable domains remain[0, 1]independently of the bounds dimension. The only additional concrete registration isILP<i64, i64, Bounded>; no bounded-binary or bounded-float variants are registered.The five binary-only migrations are AcyclicPartition, BiconnectivityAugmentation, BottleneckTravelingSalesman, EnsembleComputation, and StrongConnectivityAugmentation. Existing finite variable intervals and constraint formulations are retained throughout the migration.
Callers of migrated typed reductions must select their new target types. Exact variant maps now include
bounds; CLI problem references with omitted trailing dimensions still default to general. Explicit bounded CLI references includeILP/i64/i64/bounded. CLI help uses unambiguous names that round-trip across every registered variant.Fixed solver pipelines and native dispatch support the bounded terminal directly. Graph reachability remains independent of solver capability registration. Documentation, examples, fixtures, and dependent reduction chains are updated.
Verified example
For the bounded integer problem
maximize 3x, with-2 <= x <= 3andx <= 1, real CLI executions produced:x = 1Max(3)x = 1Max(3)x = 1Max(3)The same instance without a bounds dimension loads as general ILP. An explicitly bounded instance with an infinite endpoint is rejected. A graph regression confirms that general integer ILP has no path to binary ILP.
ILP overhead predictions
The domain contract makes binary encoding applicable, but end-to-end size predictions also need bounds on the numeric data that the encoder uses. This PR replaces the machine-width constant in binary ILP → QUBO with source-dependent upper bounds and propagates the required information through incoming rules.
max_constraint_magnitude_bits: the smallesth >= 1such that normalized constraint coefficients, right-hand sides, and finite variable endpoints have magnitude below2^h. Objective coefficients are excluded; infinite endpoints do not establish boundedness.nvariables andmconstraints, useU = n + m(n+h)and predict at mostUvariables andU²quadratic terms. These are deliberately coarse bounds.zsource nonzeros, predict at mostn(h+1)variables,z(h+1)nonzeros, and magnitude bits at most2h+n+1; the constraint count is unchanged.max_numeric_magnitude_bits: it measures their input sizes plus capacity or target where applicable. Local formulas propagate it through 3-SAT → SubsetSum → Partition → BinPacking → binary ILP → QUBO and Partition → SubsetSum. SubsetSum retains arbitrary-precision inputs.These additions extend the public parameter schemas. Each formula uses only source parameters and remains local to its rule. No model-level inference is introduced. Some predictions remain unavailable where registered source parameters do not bound the required numeric data or the symbolic evaluator cannot express the needed bound.
Verified prediction and recovery example
For BinPacking with item sizes
[1, 1]and capacity1, the explicit BinPacking → binary ILP → QUBO route was exercised through CLI path discovery, reduction, brute-force solving, and source recovery:[1, 0]Min(2)At the comparison source, the BinPacking → ILP contract has no magnitude field and binary ILP → QUBO uses a fixed 63-bit slack bound. The new contracts derive the bounds above entirely from BinPacking's two source parameters. Boundary tests cover signed integer extremes, floating-point power-of-two boundaries, arbitrary-precision SubsetSum values, and composed solution recovery.
Verification
Latest overhead changes
make test: 6,891 passed.Earlier bounded-variant migration
example-db: 6,707 passed, 2 ignored, run undercargo llvm-cov --workspace --features example-db --lcov.cargo test -p problemreductions-cli --all-features --bin pred: 205 passed, including MCP.cargo clippy --workspace --all-targets --all-features -- -D warnings: passed.cargo fmt --all -- --checkandgit diff --check: passed.make paper: passed after updating all explicit ILP example selectors for the bounds dimension.Finite intervals are a mathematical precondition, not a guarantee that every encoding fits machine arithmetic. Existing checked-overflow errors and HiGHS numerical limitations still apply.