Fix #138: [Rule] SubsetSum to Knapsack

[GiggleLiu]

Summary

Add the SubsetSum -> Knapsack reduction rule and execute the implementation plan.

Fixes #138

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 97.49%. Comparing base (e70b661) to head (594ee63).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #710   +/-   ##
=======================================
  Coverage   97.49%   97.49%           
=======================================
  Files         359      361    +2     
  Lines       45584    45657   +73     
=======================================
+ Hits        44440    44514   +74     
+ Misses       1144     1143    -1     

☔ View full report in Codecov by Sentry.
📢 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.

[GiggleLiu]

Implementation Summary

Changes

• Added src/rules/subsetsum_knapsack.rs implementing the SubsetSum -> Knapsack reduction with identity solution extraction, num_items = num_elements overhead registration, and checked BigUint -> i64 conversion.
• Added src/unit_tests/rules/subsetsum_knapsack.rs covering satisfiable round-trip behavior, target structure, UNSAT extraction, overflow handling, and canonical example export.
• Registered the rule and canonical example in src/rules/mod.rs.
• Added the SubsetSum -> Knapsack theorem and worked example to docs/paper/reductions.typ.

Deviations from Plan

• Implemented the rule execution locally with review checkpoints rather than dispatching a separate implementer worker, to keep the blocking path moving in this session.
• Added one extra paper compatibility fix in docs/paper/reductions.typ: replaced a stale x.samples.at(0) access with x.optimal_config so make paper succeeds against the current exported example schema.
• The reduction was implemented against the existing optimization Knapsack model, not a decision-threshold variant, and it explicitly enforces the i64 representation boundary noted in the issue discussion.

Open Questions

• None.

[GiggleLiu]

Agentic Review Report

Structural Check

Structural Review: rule subsetsum_knapsack

Structural Completeness

#	Check	Status
1	Rule file exists	PASS
2	#[reduction(...)] macro present	PASS
3	ReductionResult impl present	PASS
4	ReduceTo impl present	PASS
5	#[cfg(test)] + #[path = "..."] test link	PASS
6	Test file exists	PASS
7	Closed-loop test present	PASS
8	Registered in rules/mod.rs	PASS
9	Canonical rule example registered	PASS
10	Example-db lookup tests exist	PASS
11	Paper reduction-rule entry	PASS

Build Status

• make test: PASS
• make clippy: PASS

Semantic Review

• extract_solution(): OK
• overhead = { num_items = "num_elements" }: OK
• example quality: OK
• paper proof soundness: OK
• BigUint -> i64 domain handling: ISSUE - the reduction is only defined for instances whose sizes and target fit in i64; biguint_to_i64() panics on larger valid SubsetSum inputs instead of producing a reduction, so the implementation is not total over the stated source problem domain (src/rules/subsetsum_knapsack.rs:41-43).

Issue Compliance

#	Check	Status
1	Source/target match issue	OK
2	Reduction algorithm matches	OK
3	Solution extraction matches	OK
4	Correctness preserved	ISSUE - correctness is contingent on an unstated representability precondition; the code rejects valid SubsetSum instances outside i64, so the reduction does not cover the full mathematical problem (src/rules/subsetsum_knapsack.rs:41-43, docs/paper/reductions.typ:4299-4303).
5	Overhead expressions match	OK
6	Example matches	OK

Summary

• 11/11 structural checks passed
• 5/6 issue compliance checks passed
• ISSUE: BigUint -> i64 conversion makes the reduction partial for valid SubsetSum inputs outside signed 64-bit range.

---

Quality Check

Quality Review

Design Principles

• DRY: OK
• KISS: OK
• HC/LC: OK

Test Quality

• Naive test detection: ISSUE - src/unit_tests/rules/subsetsum_knapsack.rs:45-53 only checks the single-value overflow panic path; it does not exercise the more realistic aggregate-overflow case introduced by Knapsack::evaluate (src/models/misc/knapsack.rs:139-153).

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• src/rules/subsetsum_knapsack.rs:31-43 converts arbitrary-precision SubsetSum inputs into i64, and src/models/misc/knapsack.rs:139-153 sums weights and values in i64 without overflow checks. That makes the new reduction partial and still vulnerable to panics for valid SubsetSum instances whose item weights fit individually but overflow in aggregate during target evaluation.
• Confirmed locally with a direct repro: reducing SubsetSum::new(vec![i64::MAX, 1], i64::MAX) succeeds, but evaluating the target Knapsack config [1, 1] panics with attempt to add with overflow.
• src/unit_tests/rules/subsetsum_knapsack.rs:45-53 does not cover that aggregate-overflow failure mode, so the new tests give false confidence about the rule’s behavior on large instances.

Minor (Nice to Have)

None.

Summary

• Important: src/rules/subsetsum_knapsack.rs:31-43 and src/models/misc/knapsack.rs:139-153 make the reduction partial and overflow-prone.
• Important: src/unit_tests/rules/subsetsum_knapsack.rs:45-53 misses the aggregate-overflow edge case.

---

Agentic Feature Tests

Agentic Feature Tests

Verdict: pass
Critical Issues: 0

I exercised the full user path for the new SubsetSum -> Knapsack rule with the shipped CLI/docs. The rule is discoverable in the catalog, both endpoint problem views show the direct reduction, canonical examples generate correctly, and the reduction solves back to the original SubsetSum witness as expected.

Step	Command	Result
Catalog discovery	pred list --rules	Worked. The output includes SubsetSum -> Knapsack and shows it as a direct rule.
Source show	pred show SubsetSum	Worked. It lists Knapsack as the outgoing reduction target.
Target show	pred show Knapsack	Worked. It lists SubsetSum as an incoming reduction source.
Source example	pred create --example SubsetSum -o ...	Worked. It produced a valid SubsetSum instance with sizes = [3,7,1,8,2,4] and target = 11.
Rule example target	pred create --example SubsetSum --to Knapsack --example-side target -o ...	Worked. It produced a valid Knapsack instance with matching weights/values and capacity = 15.
Source solve	pred solve <subsetsum.json>	Worked. It returned evaluation: true with solution [0,1,0,0,0,1].
Reduce	pred reduce <subsetsum.json> --to Knapsack -o ...	Worked. It wrote a reduction bundle with source, target, and path.
Reduced solve	pred solve <reduced.json>	Worked. It solved the bundle and mapped back the same witness through the Knapsack intermediate.

Friction was low. The only minor thing worth noting is that pred reduce outputs a reduction bundle rather than a plain Knapsack problem JSON, which is consistent with the docs but worth keeping in mind when manually inspecting files. I did not find any reproducible issue in this worktree.

---

Generated by review-pipeline