[Critical] Fix reduction result recovery and reference validation contracts

[isPANN]

Summary

Fix reduction result recovery, model validation, and reference-solver correctness while retaining the existing Problem, SolutionAggregate, and typed witness/value reduction interfaces.

API and behavior changes

• Keep witness extraction and completed aggregate mapping separate. Register value mappings beside their implementations and reuse the constructed reduction for both mappings. Dynamic aggregate extraction is fallible; chains expose extract_value.
• Enforce decision thresholds during recovery. Established target or intermediate infeasibility propagates without a witness; extraction errors and worker failures remain errors, not NO answers.
• Use pred extract bundle.json --config '<target config>' to map a target witness through the rules' solution mapping, or --value <completed aggregate> to map a completed target value. Extraction does not solve the target or establish optimality or exhaustive NO.
• Model decision thresholds explicitly with Decision<P>. Direct bounded OpenShopScheduling and LongestCircuit ILP encodings add a bound constraint and use a zero objective; their optimization versions retain their objectives.
• Enforce construction constraints through Rust and JSON, with explicit numeric and representation errors. Correct rule edge cases, signed TSP costs, and malformed witness extraction.
• Make CVP integer-only with squared-distance Min<i64> values and the coefficient variant key. Persist QUBO as num_vars plus sparse entries. Register KColoring KN/K2/K3 variants and provide a direct bipartite solver for K2.
• Isolate HiGHS conversion and execution in a concrete adapter; native integer ILPs go directly to it. Numerical solver guarantees remain subject to HiGHS tolerances.
• Remove the total-cardinality requirement from Cartesian enumeration. Use existing Lehmer decoding for CyclicOrdering, Betweenness, and MinimumCodeGenerationUnlimitedRegisters instead of enumerating invalid position vectors.

Core Problem and solver return interfaces are not migrated. Model-specific getters/parameters, dynamic extraction signatures, persisted formats, and supported variants do change; this is a critical API review. P → Decision<P> remains a Turing edge (binary search over the decision bound).

Scope

Against main at head 31bdb314: 404 files changed, 14,058 additions, 4,712 deletions. No website changes. The obsolete SteinerTreeInGraphs removal is already in main and is not part of this diff.

Validation

• CI at 31bdb314: Test, Clippy, Rustfmt, coverage, RISC-V, Windows x86_64, and macOS ARM64 checks passed; Codecov checks passed.
• Local all-feature workspace library/binary/integration tests at ef634c2b: 6,727 passed, 2 ignored. Workspace Clippy with warnings denied, formatting, and paper build passed.
• After the test-only simplification at 67715f12: all 19 solver-registry tests passed.
• Local follow-up recovered all 597 original corpus recovery-error cases as infeasible with unchanged source truth.
• Two previously timed-out full-bundle examples passed locally: Partition → bounded OpenShopScheduling in 0.80 s (NO), and DecisionMinimumVertexCover → HamiltonianCircuit in 0.57 s (YES with a valid recovered cover). These are debug-build examples, not HPC-wide performance claims.

[codecov]

Codecov Report

❌ Patch coverage is 97.87598% with 87 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.73%. Comparing base (5a35ce7) to head (be05d56).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/solvers/ilp/adapter.rs	91.61%	14 Missing ⚠️
src/rules/ksatisfiability_qubo.rs	74.35%	10 Missing ⚠️
src/rules/coloring_qubo.rs	59.09%	9 Missing ⚠️
src/models/graph/spin_glass.rs	75.75%	8 Missing ⚠️
src/rules/satisfiability_maximum2satisfiability.rs	64.70%	6 Missing ⚠️
src/solvers/customized/solver.rs	81.81%	6 Missing ⚠️
...s/misc/consistency_of_database_frequency_tables.rs	83.33%	4 Missing ⚠️
src/registry/dyn_problem.rs	83.33%	2 Missing ⚠️
src/rules/acyclicpartition_ilp.rs	92.00%	2 Missing ⚠️
src/rules/ksatisfiability_timetabledesign.rs	71.42%	2 Missing ⚠️
... and 22 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1171      +/-   ##
==========================================
+ Coverage   96.22%   96.73%   +0.50%     
==========================================
  Files        1070     1069       -1     
  Lines      133605   138549    +4944     
==========================================
+ Hits       128564   134023    +5459     
+ Misses       5041     4526     -515     

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

Agentic Review Report

Reviewed head 29097e9b against main 5a35ce7f. make check passes locally: fmt, clippy with -D warnings, and all workspace tests.

Note: the QUBO allocation guard added in 29097e9b (try_reserve_exact) does not hold on Linux, because the kernel overcommits memory. An 82-byte {"num_vars":20000,"entries":[]} still reaches 3.2 GB RSS, and 100k variables reach 34 GB. A real fix needs an explicit cap or sparse storage. See Quality #2 and Feature F1.

Structural Check

#	Check	Status
1	No blacklisted generated files	PASS
2	Every Or-source witness rule with a non-Or target has a value mapping (static scan of 272 impls)	PASS
3	AggregateMappingEntry attaches to exactly one witness edge	PASS
4	New Decision variant registrations and example-db specs	PASS
5	CVP coefficient key rename, no stale target key	PASS
6	KColoring K2/K3/KN declarations and complexity	PASS
7	K2 customized solver (solve_two_coloring) has a direct test	FAIL
8	Removed K4/K5 variants have no stale references	FAIL (minor): docs/src/static/variant-hierarchy.typ:50-51
9	Removal of ksatisfiability_minimumvertexcover.rs leaves nothing dangling	PASS
10	Extraction contract (validate once, typed errors, no clamp or panic)	PASS

Verified bugs

1. MAJOR: TSP→QUBO can produce a target whose valid tours overflow (src/rules/travelingsalesman_qubo.rs:226-231). Only the offset 2nA + n·s is checked to fit i64, but a tour's energy is H_C − 2nA. Example: a triangle with all weights −6e17. The reduction succeeds, but evaluating or brute-force solving the target fails with an integer overflow, so a feasible source maps to a target no solver can evaluate. The paper understates the requirement.
2. MINOR/design: brute force aborts on penalty QUBOs. The optimum fits in i64, but a non-optimal configuration overflows, and brute force stops at the first evaluation error. Example: K4 TSP with all weights 5e16. Files: qubo.rs:260-273, brute_force.rs:184/206/227.
3. MINOR: the CVP solver can pick a tied optimum whose distance overflows (src/solvers/customized/closest_vector_problem.rs:113). Example: basis 2, target i64::MAX. It returns a typed error, not a wrong answer.

Stale paper text

• KSAT→DecisionQUBO (~12127) and KColoring→DecisionQUBO (~12103) still describe the old equality mappings; the code now checks a decision bound.
• Partition→DecisionOSS (~18963) says "equal to D"; the code checks ≤ D.
• HC→DecisionLongestCircuit (~15636) never states the decision bound n.
• TSP→QUBO example (~14030) says "diagonal −7"; it should be −2A.

Minor

• The KSAT→DecisionMVC short-clause and empty-clause branches are untested.
• SolveError::SearchSpaceOverflow is now unused, so a huge brute-force space loops instead of failing fast.
• The test test_find_rule_example_ksatisfiability_to_minimumvertexcover is misnamed; it now targets DecisionMVC.

Checked OK:

• The recovery core: infeasibility propagation, witness-vs-value checks, and extraction errors staying errors.
• Decision<P>→P bound enforcement and the HiGHS adapter.
• CVP model, CVP→QUBO and SubsetSum→Decision.
• The OSS and LongestCircuit decision ILP encodings, the K2 solver (agrees with brute force on 80 random graphs), and Lehmer decoding.
• About 20 further rules traced on small examples.

---

Quality Check

Important

1. Recovery algorithm written twice, and the copies differ. src/solvers/registry.rs:121-175 and problemreductions-cli/src/dispatch.rs:370-427 both implement it, but only the CLI copy checks that the mapped aggregate equals the re-evaluated witness. Move one implementation next to ReductionChain and have both callers use it.
2. Sparse QUBO JSON with a large num_vars allocates n² memory. Observed 31 GB RSS (qubo.rs:104-137). The try_reserve_exact guard is ineffective under overcommit.
3. Recovery boilerplate across ~140 rules:
   • About 130 copied feasibility guards; "target ILP assignment is infeasible" appears 51 times.
   • 133 near-identical AggregateReductionResult impls: 78 identity Or→Or, 55 ILP Or(value.is_some()).
   • Suggested fix: a shared "validate, then require the value map to say YES" helper, plus an identity / ILP-feasibility registration shorthand. The old aggregate = identity shorthand was removed.
4. Breaking persisted-format changes without migration hints: CVP target→coefficient (f64 variant dropped, objective changed to squared distance) and QUBO matrix→entries. Old files fail with unhelpful errors. Needs a semver-major / changelog note.
5. Empty help for the 15 new Decision variants. Their FieldInfo arrays have 22 empty descriptions (e.g. max_cut.rs:362-364), so pred create Decision* --help shows blank flags. They should reuse the inner CreateSpec FIELDS.
6. QUBO entries below the diagonal are accepted but silently ignored by evaluation and reductions. Reject them or fold them into the upper triangle.

Minor
7. Aggregate mappings joined at runtime (src/rules/registry.rs:270-315). A misregistration panics on first access instead of failing to compile, and ReductionEntry has two overlapping aggregate fields.
8. 41 hand-written Deserialize impls where #[serde(try_from)] is the codebase idiom. Length-check messages are copy-pasted and lost their actual/expected counts (MaxCut).
9. pred extract --value formatting: input and output use raw JSON rather than Min(2)/Or(false) wrapper formatting, and the help doesn't explain the encoding.
10. Extract cleanup: the text output drops "Solver: external" but the JSON keeps it; the stdin example was removed from help; the .context at extract.rs:31 is unreachable.
11. Test hygiene:
- cli.rs:578 tests the undefined flags --result/--status.
- The 5-cycle brute-force cross-check in decision_search.rs was removed.
- A test fixture registers a fake Decision variant in the global inventory.
12. Leftover CVP dimension: coefficient has a single value, ["i64"].
13. Generic Decision descriptions: the new variants don't say whether the bound is ≤ or ≥.

Positives:

• The HiGHS adapter cleanly isolates the backend, and dropping good_lp is a net simplification.
• Shared worker-timeout error handling between the CLI and MCP.
• CLAUDE.md and design.md match the code.
• No test assertions were weakened relative to main.

---

Agentic Feature Tests

Feature	Scenarios	Result
Recovery	DecisionMVC→MVC NO; KColoring→DecisionQUBO→QUBO YES/NO; Partition→DecisionOSS; DMVC/One→HC; malformed --config/--value	PASS: NO reported as infeasible; bound enforced; clear errors
QUBO	create/inspect/solve; out-of-range, duplicate, legacy matrix, num_vars 1e10/2^32/u64::MAX	PASS
QUBO	num_vars 20000 / 100000 with empty entries	FAIL (F1)
CVP	show/create/solve/example; CVP→QUBO; invalid inputs	PASS
KColoring	KN/K2/K3 listing; K2 bipartite solver vs brute force; k=0 via JSON and via PartitionIntoCliques	PASS
Decision/ILP	DecisionOSS bound 8/7; DecisionLongestCircuit bound 18/19 (ILP and brute force)	PASS
Checklist	list, list --rules, show, create --example, solve, reduce --via, inspect	PASS (see notes)

Findings, all reproduced

• F1 HIGH: an 82-byte QUBO JSON (num_vars: 20000) makes pred inspect take 66 s and 3.2 GB RSS; 100k variables reach 34 GB. The guard in qubo.rs:122-136 is bypassed by overcommit.
• F2 LOW (docs): pred create QUBO --matrix '1,0.5;0.5,2' in docs/src/cli-commands.md fails because the default variant is now QUBO/i64.
• F3 LOW-MEDIUM (docs/UX): the doc's MIS→QUBO pred extract reduced.json --value 2 example fails with "Bundle requires an aggregate-capable reduction path". Nothing tells the user which paths support --value, and pred solve prints Min(2) while --value accepts only raw JSON.
• F4 LOW: pred create KColoring --k 0 is rejected, but JSON with num_colors: 0 is accepted and solved correctly. CLI and serde enforce different ranges (kcoloring.rs:141 vs :152).
• F5 LOW: --example has no canonical example for DecisionOSS, DecisionLongestCircuit or DecisionMVC/One, or for default KColoring (KN).
• F6 LOW: a legacy CVP variant key gives "must specify a prefix of its dimensions" without naming coefficient.
• F7 minor:
  • pred path DecisionMVC HamiltonianCircuit finds no path for the default variant, with no hint to use /One.
  • --edge-weights vs edge_lengths and --num-processors vs num_machines naming mismatches (these predate the PR).
  • Brute force on the OSS example runs over 6 minutes with no size warning.
  • Feasibility problems report "status": "optimal".
  • O(?) complexity is shown for CVP, OSS and DecisionOSS.

---

Generated by review-pipeline (PR is not on the project board, so no column move was made).