Exact symbolic growth, unified reduction size contracts, and deterministic solver backends

[isPANN]

Closes #1075, #1078, #1076, #788, and #1090.

Systematic API changes

The main API changes are: problems accept their own solution types, solvers return a solution or explicit failure, and reductions report named input/output parameters. The cross-cutting changes come first; individual model and reduction fixes follow separately. This is a breaking API change.

1. Problem::evaluate: pass a mathematical solution

Why needed: A Boolean selection, a signed lattice coefficient, and a pair of factors are different kinds of solutions. Encoding all of them as usize arrays makes callers understand solver-specific encodings and leaves malformed inputs indistinguishable from ordinary candidates.

Previously every problem accepted &[usize], and evaluate() returned a value directly. Now each problem defines type Solution, and evaluation returns Result<Value, EvaluationError>.

For a unit-weight path with edges 0–1–2–3:

Call	Result
mis.evaluate(&vec![true, false, true, false])	Ok(Max(Some(2))): vertices 0 and 2 are independent
mis.evaluate(&vec![true, true, false, false])	Ok(Max(None)): adjacent vertices were selected
mis.evaluate(&vec![true])	Err(EvaluationError::InvalidConfiguration(...)): wrong solution length

This separates an infeasible candidate from a malformed input or arithmetic failure. The corresponding CLI input is now Boolean JSON, for example --config '[true,false,true,false]'.

Requiring every problem to expose a finite Cartesian search space also forces artificial restrictions on models such as unbounded CVP. Problem::dims() is removed from the base trait. Models that support finite enumeration implement BruteForceProblem::dimensions() and register that solver separately.

Numeric handling is updated because a wrapped objective or rounded integer can change which solution is optimal. Using one signed integer domain also avoids inconsistent model/reduction boundaries; a wider type alone does not replace checked arithmetic. Across models, signed integer fields change from i32 to i64. Overflow, non-finite float results, and inexact integer-to-float conversions return errors. Arbitrary precision remains available where the problem requires it, including factoring.

2. solve: return a witness, distinguish infeasibility from failure

Why needed: A reduction needs a target witness to reconstruct a source solution; an objective value alone is insufficient. Callers also need to distinguish “no solution exists” from “the solver failed,” rather than treating both as an absent witness.

BruteForce::solve(&problem) now returns Result<Option<P::Solution>, SolveError>:

Return	Meaning
Ok(Some(solution))	An optimal or satisfying solution was found
Ok(None)	Exhaustive search proved infeasibility
Err(error)	Execution or evaluation failed

Deterministic pred solve pipeline

Previously, automatic solving used the same reduction-path search as pred path to choose a route to ILP. This coupled solver behavior to path discovery: future optimizations to pred path could change the reduction chain used by pred solve, even when the input and solver request stayed the same.

pred solve now uses an explicitly registered pipeline for each exact problem variant:

1. Resolve the input's exact model and numeric/graph variant.
2. Select the first registered capability in the fixed order: customized solver, fixed ILP pipeline, then brute force. An explicit --solver selects only that backend.
3. For ILP, execute the declared reduction chain, solve the target ILP, and extract the source solution through that same chain. For example, the registered BicliqueCover pipeline is BicliqueCover -> BMF -> ILP<bool, i64> -> ILP<bool, f64>.
4. Return the solution and its source evaluation, proven infeasibility, or an explicit error. Once selected, a backend's failure is returned without trying another backend.

The shared solve(problem, SolverRequest) API does not search the reduction graph at solve time. pred path remains a path-exploration command; changes to its search or ordering do not alter the registered solve pipeline. Changing a solve route requires explicitly updating its pipeline declaration. A graph route to ILP alone does not establish solver availability for a variant.

pred inspect problem.json shows the registered capabilities and ILP path; solve results identify the selected backend and, for ILP, the executed reduction path. pred solve problem.json --solver brute-force explicitly selects brute force.

Dynamic results contain Optimal { solution, evaluation } or Infeasible; successful solves do not return a value without a solution.

3. ILP: separate variable and coefficient types, check backend answers

Why needed: Variable integrality and coefficient representation are independent: an integer variable may appear in a row with fractional coefficients. Keeping these choices separate lets reductions express the intended domain and makes the conversion to the floating-point backend explicit.

ILP<bool, i64> describes Boolean variables with integer coefficients; ILP<i64, f64> describes integer variables with floating-point coefficients. Variables store explicit lower/upper bounds, including unbounded sides. Constraints and objectives use sparse coefficients.

• Rounded HiGHS assignments are checked against the ILP before being returned, because rounding can violate a constraint even when the backend reported an optimum.
• When the backend cannot distinguish infeasibility from unboundedness, a zero-objective feasibility solve determines which result applies. This prevents a feasible problem with an unbounded objective from being reported as having no feasible assignment.
• Decision pipelines compare the mapped source objective with the decision bound before returning a witness. A feasible target ILP alone does not imply that the source decision is true: for example, finding a clique partition using four cliques does not satisfy a request for at most three.

4. Reduction parameters: report sizes by name and compose formulas

Why needed: A number such as “size = 10” does not identify whether it counts vertices, edges, or variables. Path composition needs the same named quantities at both ends of every edge. It must also distinguish equalities from bounds: substituting m <= n^2 into 10 - m as though it were equality would produce an unsound upper bound.

Problem::parameters() reports named u64 values such as num_vertices and num_edges. Reduction declarations specify how those values change using transform = exact, upper_bound, or unavailable.

ParameterTransform::evaluate() applies one relation; compose() combines consecutive relations:

Relations	Composed result
Exact m = 4, then k = 10 - m	Exact k = 6
Bound m <= n^2, then k = 10 - m	Bound k <= 10

Each target parameter must have a formula or a stated reason it is unavailable. Unknown parameter names are rejected when declarations compile, so a typo cannot silently disconnect a formula from its model. Runtime and macro expressions share exact integer/rational arithmetic to avoid parser disagreement and floating-point rounding in symbolic calculations; symbolic Big-O analysis reports unsupported cases explicitly instead of presenting an unjustified estimate.

ReductionGraph::path_parameter_transforms() returns the individual relations, and compose_path_parameter_transform() returns their composition.

5. CLI/MCP: construct the selected variant and inspect bounded path lists

Why needed: Separate model-specific parsers in CLI and MCP duplicate field definitions and validation. Selecting construction fields from the concrete variant prevents the two entry points from accepting different versions of the same instance.

Creation flags come from the selected model's construction fields. CLI and MCP call the same registered constructor, so they apply the same validation. For example:

pred create MIS --graph 0-1,1-2,2-3 -o mis.json
pred inspect mis.json
pred solve mis.json --solver brute-force
pred path MIS QUBO --limit 50
pred path MIS QUBO mis.json --limit 50

Path output is bounded because the number of simple reduction paths can grow combinatorially; inspecting a route should not require listing or executing all of them. The truncated field prevents a partial list from being mistaken for a complete one.

The fourth command lists up to 50 reduction paths; the fifth also executes those paths on the instance and reports the constructed problems' parameters. The default limit is 20, the maximum is 999, and --limit all means 999. JSON includes paths and truncated to indicate whether more paths exist.

Saved-route replay, evaluation, and extraction carry the model's typed solution. Direct reduction extractors validate the target solution before decoding it, so malformed target data cannot become an apparently valid source witness through indexing or decoding.

Concrete model changes

Factoring and ClosestVectorProblem

Why needed: To factor 15, a caller should supply 15 without first choosing a bit encoding. For CVP, guessed coefficient bounds can exclude the true closest lattice point and thereby change the problem being solved. These constructors now take the mathematical input; explicit factoring widths remain available when the caller actually wants that restriction.

API	Before	Now
Factoring	Factoring::new(2, 3, 15); solutions encode factor bits	Factoring::new(15) derives widths 2 and 3; the solution is the ordered BigUint pair (3, 5)
Explicit factor widths	Supplied to every constructor call	Factoring::with_factor_bits(15, 2, 4) when widths are part of the requested instance; these widths also admit (1, 15)
Closest vector	Constructor requires coefficient bounds; configurations encode offsets within them	ClosestVectorProblem::new(basis, target); a solution directly contains signed integer coefficients

For CVP with basis columns [2,0,0], [1,2,0] and target [3,3,1], evaluating coefficients [1,1] gives distance sqrt(2). Coefficients [11,-12] are also valid candidates—there is no artificial enumeration box. A registered sphere-enumeration solver handles this model.

Other model fixes

Model	Change	Why needed
OpenShopScheduling	Replaces per-machine job permutations with explicit operation start times; checks both job and machine overlap.	A machine order alone does not specify the timing of an open-shop schedule. The witness must represent the schedule that is evaluated and extracted from ILP.
UndirectedTwoCommodityIntegralFlow	Checks conservation separately for each commodity at every vertex other than that commodity's own terminals.	The other commodity's source/sink must not become a place where flow can appear or disappear.
BiconnectivityAugmentation	Checks the budget after summing all selected edge weights.	With signed weights, an intermediate sum can exceed the budget even though later negative weights bring the final total within it.
MixedChinesePostman	Checks connectivity on vertices incident to available arcs/edges.	An unrelated isolated vertex must not invalidate a tour covering the required edges.
KColoring<K, G>	Rejects persisted num_colors values that disagree with fixed K.	Loading a three-color variant with a different color count would change its mathematical meaning while retaining the same registered type.
MinimumCostMaximumFlow	Validates terminals, vector lengths, capacities, and costs during deserialization.	Loading JSON must not bypass the conditions enforced by construction.
SteinerTree	Validates edge-weight counts and requires at least two distinct, in-range terminals, including when loading JSON.	The registered model and its reductions require a valid terminal set; unchecked persisted data could violate those assumptions.
IsomorphicSpanningTree	Validates equal vertex counts and the connected-tree condition during deserialization.	A loaded target that is not a tree cannot represent the declared problem.
DecisionMaximumIndependentSet and MinimumFeedbackVertexSet	Registers unit-weight variants used by their reductions.	Cardinality-based constructions must refer to an actual unit-weight variant rather than advertising support for arbitrary weights.

Concrete reduction-rule changes

These changes repair particular constructions or decoders, separately from the shared API migration above.

Rule	Change	Why needed
EnsembleComputation -> ILP	Adds a circuit-slot formulation and fixed solver pipeline.	Makes the operation-sequence problem executable through ILP instead of requiring full sequence enumeration.
MultipleChoiceBranching -> ILP	Adds a direct formulation.	Supplies an explicit executable route to the ILP backend for this model.
PartitionIntoCliques -> ILP	Adds a direct formulation.	Encodes the clique-partition decision for the fixed ILP solver workflow.
DecisionMaximumIndependentSet -> IntegralFlowBundles	Replaces the optimization-source rule with a unit-weight decision rule and handles empty graphs/nonpositive thresholds.	The construction answers one cardinality question; one flow query does not recover the maximum independent-set size.
DecisionMinimumDominatingSet -> MinimumSumMulticenter	Adds forced isolated centers and checks the target objective against the source threshold.	Preserves the decision for negative, zero, and oversized bounds; a feasible center placement alone is insufficient.
SteinerTree -> ILP	Links selected vertices and edges, enforces connectivity, and requires edges = vertices - 1.	Negative edge weights can make extra cycles attractive, so minimizing cost alone cannot enforce a tree.
BiconnectivityAugmentation -> ILP	Enforces connectivity both before deletion and after each vertex deletion.	The target must encode the full biconnectivity condition, including small-graph cases.
UndirectedTwoCommodityIntegralFlow -> ILP	Matches the model's per-commodity conservation constraints.	A terminal of one commodity is still an ordinary conservation vertex for the other.
OpenShopScheduling -> ILP	Uses the explicit start-time solution representation.	The ILP assignment and source witness must describe the same schedule without reconstructing timing from machine orders.
Partition -> OpenShopScheduling	Maps the target makespan back to the partition decision and rejects schedules missing the required threshold.	A feasible schedule need not certify an equal-sum partition.
HamiltonianCircuit -> LongestCircuit	Requires the target circuit to certify the Hamiltonian threshold before extraction.	A shorter valid circuit must not be returned as a Hamiltonian witness.
HamiltonianPathBetweenTwoVertices -> LongestPath	Checks the spanning-path threshold and walks the selected edges to return the vertex order.	An edge-selection vector is not the source's ordered path, and a short path does not certify Hamiltonicity.
KColoring -> QUBO	Tracks the zero-penalty energy and checks it before decoding.	QUBO always has an optimum, even when the source graph is not colorable with the requested number of colors.
CircuitSAT -> SpinGlass	Tracks gate/equality ground-energy offsets and checks the combined zero-penalty threshold.	A minimum-energy spin configuration does not necessarily satisfy an unsatisfiable circuit; omitted constants also affect the threshold.
ILP<bool> -> QUBO	Restores the omitted penalty constant and maps feasible target energies back using the source objective sense.	A penalized QUBO optimum must not be confused with a feasible ILP solution or its original objective value.
TravelingSalesman -> QUBO	Decodes matrix entries as vertex * n + position.	Reading the transposed indexing can reconstruct the wrong tour from a correct target assignment.
SpinGlass -> MaxCut	Normalizes the auxiliary spin to +1 before removing it.	The opposite normalization reverses the contribution of source local fields.
Factoring -> CircuitSAT	Checks multiplication-circuit dimensions, handles zero-width multiplier rows, and requires a satisfying target assignment.	Empty rows must not reference gates that were never created, and an unsatisfied circuit must not decode into claimed factors.
SubsetSum -> ClosestVectorProblem	Uses a binary-carry lattice and checks its target-distance certificate.	The reduction must encode subset choices in the unbounded CVP model without relying on removed coefficient bounds.
MinimumVertexCover -> EnsembleComputation	Extracts a cover from the evaluated operation prefix, without assuming a special program ordering.	The target solver may return any valid optimal program, not just the constructor's preferred form.
PartitionIntoCliques -> MinimumCoveringByCliques	Adds private vertices for forced side cliques and adjusts the objective threshold for distinct non-loop adjacencies.	The forced cliques and threshold must remain valid for empty inputs and repeated/loop adjacencies.
QUBO, ILP, and CVP numeric variant conversions	Adds explicit checked conversion edges.	Changing numeric types can lose information and must be a visible, fallible reduction step.
MinimumFeedbackArcSet -> MaximumLikelihoodRanking	Removes the rule.	Its declared weighted source domain exceeds the implementation's unit-weight restriction; path execution could select an edge that cannot handle a valid source.
ThreeDimensionalMatching -> ThreeMatroidIntersection	Removes the rule along with the removed target model.	The catalog must not retain a route whose target is unavailable.

Documentation and build changes

• Updates paper definitions/proofs, examples, API guides, and CLI recordings because the old constructors, solution encodings, and reduction statements no longer describe the implementation.
• Uses native MathML for website equations and registry expressions so fractions, powers, and roots display as mathematical notation.
• Updates HiGHS build configuration and macOS ARM64, Windows x86_64, and RISC-V build/run checks to verify that the required native backend builds and executes on the supported platforms.

Verification

All seven checks passed at 0227c24788ec2aeebecd1b06704328599cfcbbf9: Rustfmt, Clippy, Test, Code Coverage, and macOS ARM64 / Windows x86_64 / RISC-V build-and-run jobs.

Examples in this description were checked against the current implementation and existing tests. No local test suite was rerun for this body-only edit.

Note: The Reduction fixes are not yet complete. This PR currently includes only a subset of them, together with the package-system refactoring.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 95.93%. Comparing base (9bcda92) to head (e1a45a7).

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1137      +/-   ##
==========================================
- Coverage   98.00%   95.93%   -2.08%     
==========================================
  Files        1044     1074      +30     
  Lines      107380   132106   +24726     
==========================================
+ Hits       105234   126730   +21496     
- Misses       2146     5376    +3230     

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

[GiggleLiu]

Fixed all eight findings from the parallel review in e1a45a77d9552a43e47d15fe41e9b47f510f17a0. A fresh review of the fixes found no additional issues.

Finding	Fix and regression evidence
CVP reported a suboptimal lattice point as optimal	Gram-Schmidt projections and sphere bounds now use exact rational arithmetic. The large translated target now returns coefficients [100000000000000,100000000000000] and Min(0), with integer/float, negative-translation, and nearly parallel basis regressions. Existing transport limits remain enforced.
Bundle solving labeled an unsatisfiable source optimal	Shared bundle extraction checks typed source feasibility and returns an extraction error for an infeasible witness. This covers CLI/MCP solving and external extraction. The contradictory 3-SAT/MVC bundle is rejected; the satisfiable counterpart still succeeds. Failure to extract a witness is not treated as proof of infeasibility.
CVP-to-QUBO determinant calculation took factorial time	Replaced recursive cofactor expansion with pivoted Bareiss elimination using the existing BigInt dependency. Added a 12-dimensional identity reduction and pivoting, singularity, cancellation, and overflow checks.
Valid schedule start times were rejected	Removed the task-count restriction on time slots. Deadline validation remains. A one-task instance with deadline 3 now accepts start time 1 and completes witness enumeration.
Schedule extraction rejected valid optimal target assignments	Added one equality fixing all slots beyond individual deadlines to zero and updated exact constraint metadata. Exhaustively checked all 16 target assignments for the two-task regression.
Printed symbolic expressions changed meaning	Fractional exponents and negative bases now retain required parentheses. Round-trip checks cover n^(1/3), (2/3)^n, (-2)^n, and negative fractional bases.
Intersection-basis solving overflowed machine-word masks	Replaced edge-mask dynamic programming with exact clique-cover search over boolean coverage vectors. K8 and K12 return optimum 1 without the overflowing masks or exponential edge table.
Factorial complexity callbacks panicked above 170	Approximate complexity overflow now returns infinity, consistent with other approximate operators. Checked 5!, 170!, and 171!; typed runtime factorial evaluation still reports overflow.

Validation: make check paper mcp-test and git diff --check passed. This includes 5,800 library tests, workspace integration and documentation tests, paper compilation, 53 MCP unit tests, and 2 MCP integration tests. The original CVP and unsatisfiable-bundle counterexamples were also rerun through the CLI.

The original review covered the main changed subsystems with three subagents and was risk-focused rather than exhaustive over all 1,183 files. The fix diff changes 18 files, adds no dependencies, and updates the affected paper descriptions. The independent follow-up review also checked 560 determinant matrices and 2,000 cover systems.

All nine checks passed on e1a45a77d9552a43e47d15fe41e9b47f510f17a0: Rustfmt, Clippy, Test, Code Coverage, macOS ARM64, Windows x86_64, RISC-V, codecov/patch, and codecov/project. PR #1137 was then squash-merged as 7dd5fcdf.