Skip to content

Add bounded ILP variants and composable overhead predictions - #1180

Draft
isPANN wants to merge 5 commits into
fix/exact-reduction-parametersfrom
fix/bounded-ilp-variants
Draft

isPANN wants to merge 5 commits into
fix/exact-reduction-parametersfrom
fix/bounded-ilp-variants

Conversation

@isPANN

@isPANN isPANN commented Sep 27, 2026 •

Copy link
Copy Markdown
Collaborator

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 to main after 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.

  • Make derivable reduction parameters exact #1174 supplies the finite intervals through ILP::with_variables and adds a registry-wide encoding regression test plus a feedback-arc-set → integer ILP → binary ILP → QUBO solution-recovery test.
  • This PR makes the contract explicit in the graph: the encoding edge accepts only bounded integer ILP, and incoming rules target bounded or binary ILP according to the domains they construct.
  • Existing bound constraints are retained, preserving their row counts. Bounds are not inferred from constraint rows; each incoming rule declares its own finite intervals. General integer ILP has no binary-encoding edge.

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.

Contract Before After
ILP type ILP<V, C> ILP<V, C, B = General>
Integer → binary edge General integer ILP; infinite endpoints rejected during reduction Only ILP<i64, i64, Bounded>; construction and deserialization enforce finite endpoints
Binary → integer edge Targets general integer ILP Targets bounded integer ILP
Bounded → general edge No separate variant Identity embedding retains intervals, rows, objective, direction, and completed values
Incoming integer ILP rules All target general integer ILP Five binary-only rules target ILP<bool>; 38 problem edges target bounded integer ILP

Omitted bounds always mean general, including ILP<bool>. Binary variable domains remain [0, 1] independently of the bounds dimension. The only additional concrete registration is ILP<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 include ILP/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 <= 3 and x <= 1, real CLI executions produced:

Workflow Recovered solution Source objective
Native bounded ILP solve x = 1 Max(3)
Bounded ILP → binary ILP → QUBO, brute-force solve, extraction x = 1 Max(3)
Bounded ILP → general ILP, solve, extraction x = 1 Max(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.

  • ILP gains max_constraint_magnitude_bits: the smallest h >= 1 such that normalized constraint coefficients, right-hand sides, and finite variable endpoints have magnitude below 2^h. Objective coefficients are excluded; infinite endpoints do not establish boundedness.
  • Binary ILP → QUBO: with n variables and m constraints, use U = n + m(n+h) and predict at most U variables and U² quadratic terms. These are deliberately coarse bounds.
  • Bounded integer ILP → binary ILP: with z source nonzeros, predict at most n(h+1) variables, z(h+1) nonzeros, and magnitude bits at most 2h+n+1; the constraint count is unchanged.
  • Incoming rules: normalize redundant thresholds, omit oversized knapsack coefficients while retaining their forced-zero variables, and deduplicate set membership or neighborhoods where required. Every incoming ILP rule explicitly supplies the new field or explains why it is unavailable.
  • BinPacking, Partition, and SubsetSum gain 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 capacity 1, the explicit BinPacking → binary ILP → QUBO route was exercised through CLI path discovery, reduction, brute-force solving, and source recovery:

Result Value
Composed upper bound on QUBO variables 34
Constructed QUBO variables 8
Composed upper bound on quadratic terms 1,156
Constructed quadratic terms 14
Recovered bin assignment [1, 0]
Source objective 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.
  • Workspace Clippy with all targets and features, formatting, and diff checks: passed.
  • After the final behavior-preserving cleanup: magnitude boundary tests, reduction-graph tests (including composed solution recovery), Clippy, formatting, and diff checks passed.
  • Real CLI BinPacking → ILP → QUBO prediction, solve, and recovery: passed as shown above.

Earlier bounded-variant migration

  • Workspace tests with example-db: 6,707 passed, 2 ignored, run under cargo 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 -- --check and git diff --check: passed.
  • make paper: passed after updating all explicit ILP example selectors for the bounds dimension.
  • New bounds validation, embedding, solver dispatch, example-helper, and CLI behavior: 156/156 added executable lines covered. Across the entire diff, including mechanical target-type edits in existing overflow handlers, coverage is 285/315 lines (90.48%); those existing error branches remain uncovered.

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.

@isPANN
isPANN added this pull request to stack #1181 September 27, 2026 16:56
@codecov

codecov Bot commented Sep 27, 2026 •

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.90819% with 36 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.76%. Comparing base (f743491) to head (6029c33).

Files with missing lines Patch % Lines
src/rules/mixedchinesepostman_ilp.rs 27.27% 8 Missing ⚠️
src/rules/openshopscheduling_ilp.rs 61.53% 5 Missing ⚠️
src/rules/flowshopscheduling_ilp.rs 33.33% 4 Missing ⚠️
.../schedulingtominimizeweightedcompletiontime_ilp.rs 40.00% 3 Missing ⚠️
src/rules/highlyconnecteddeletion_ilp.rs 96.29% 2 Missing ⚠️
...s/sequencingtominimizemaximumcumulativecost_ilp.rs 50.00% 2 Missing ⚠️
src/rules/acyclicpartition_ilp.rs 75.00% 1 Missing ⚠️
src/rules/ensemblecomputation_ilp.rs 50.00% 1 Missing ⚠️
src/rules/factoring_ilp.rs 91.66% 1 Missing ⚠️
src/rules/ilp_i64_ilp_bool.rs 66.66% 1 Missing ⚠️
... and 8 more
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.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

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.
@isPANN isPANN changed the title Add explicit bounded ILP variants and migrate reduction rules Add bounded ILP variants and composable overhead predictions Sep 28, 2026
…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

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

ILP<i64> rules declare bounds as constraints, so ILP<i64> → ILP<bool> always fails

1 participant