Fix #126: Add KSatisfiability to SubsetSum reduction#599
Conversation
Co-Authored-By: Claude Opus 4.6 <[email protected]>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #599 +/- ##
==========================================
+ Coverage 96.49% 96.52% +0.03%
==========================================
Files 204 208 +4
Lines 28397 28661 +264
==========================================
+ Hits 27401 27665 +264
Misses 996 996 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
…reduction - Add SubsetSum satisfaction problem model (src/models/misc/subset_sum.rs) - Add KSatisfiability<K3> → SubsetSum reduction using Karp's base-10 digit encoding - Add comprehensive unit tests (12 model tests, 6 rule tests) - Add example program with JSON export - Register in CLI dispatch, problem aliases, schemas, and reduction graph - Add paper entries: SubsetSum problem-def and KSatisfiability→SubsetSum reduction-rule Co-Authored-By: Claude Opus 4.6 <[email protected]>
Co-Authored-By: Claude Opus 4.6 <[email protected]>
Implementation SummaryChanges
Deviations from Plan
Open Questions
Review Results
|
There was a problem hiding this comment.
Pull request overview
Adds the SubsetSum satisfaction-model to the misc model set and introduces a classical Karp-style reduction from KSatisfiability<K3> (3-SAT) to SubsetSum, including tests, an executable example, CLI JSON dispatch support, and documentation/paper updates.
Changes:
- Introduce
SubsetSumas a new satisfaction problem model (schema, variants, prelude exports, unit tests). - Add
KSatisfiability<K3> → SubsetSumreduction rule + rule unit tests + runnable example. - Register
SubsetSumin CLI JSON load/serialize and update generated docs/paper artifacts to include the new model and reduction.
Reviewed changes
Copilot reviewed 15 out of 15 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/suites/examples.rs | Adds the new reduction example to the examples test suite. |
| src/unit_tests/rules/ksatisfiability_subsetsum.rs | Adds closed-loop and structure tests for the 3-SAT → SubsetSum reduction. |
| src/unit_tests/models/misc/subset_sum.rs | Adds unit tests for the new SubsetSum model (evaluate/serialization/bruteforce). |
| src/rules/mod.rs | Registers the new ksatisfiability_subsetsum rule module. |
| src/rules/ksatisfiability_subsetsum.rs | Implements the Karp base-10 digit encoding reduction and solution extraction. |
| src/models/mod.rs | Re-exports SubsetSum at the models module top-level. |
| src/models/misc/subset_sum.rs | Implements the SubsetSum model + schema entry + variants + tests hook. |
| src/models/misc/mod.rs | Wires subset_sum into the misc module and docs list. |
| src/lib.rs | Re-exports SubsetSum in the crate prelude. |
| problemreductions-cli/src/problem_name.rs | Adds subsetsum alias resolution to SubsetSum. |
| problemreductions-cli/src/dispatch.rs | Adds JSON load/serialize support for SubsetSum. |
| examples/reduction_ksatisfiability_to_subsetsum.rs | Adds a runnable example that reduces, solves, and exports example JSON. |
| docs/src/reductions/reduction_graph.json | Updates the generated reduction graph to include SubsetSum and the new edge. |
| docs/src/reductions/problem_schemas.json | Updates generated problem schema docs with SubsetSum. |
| docs/paper/reductions.typ | Adds Subset Sum definition and the new KSAT→SubsetSum reduction rule entry. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| let n = self.num_vars(); | ||
| let m = self.num_clauses(); | ||
| let num_digits = n + m; | ||
| assert!( | ||
| num_digits <= 18, | ||
| "3-SAT to SubsetSum reduction requires n + m <= 18 for i64 encoding \ | ||
| (got n={n}, m={m}, n+m={num_digits})" | ||
| ); |
There was a problem hiding this comment.
reduce_to() currently assert!(n + m <= 18) to keep the base-10 encoding within i64. This makes the reduction panic on larger (but still valid) 3-SAT instances, which is a functional limitation for a general reduction rule. Consider switching the encoding to an arbitrary-precision integer representation (e.g., num_bigint) or otherwise representing the base-10 digit vectors without truncation so the reduction works for any n,m.
| // Variable integers are the first 2n elements: y_1, z_1, y_2, z_2, ... | ||
| // If y_i is selected (index 2*(i-1) = 1), set x_i = 1 | ||
| // If z_i is selected (index 2*(i-1)+1 = 1), set x_i = 0 |
There was a problem hiding this comment.
The inline comments describing the selected indices are incorrect/misleading (e.g., index 2*(i-1) = 1 reads like the index equals 1). Since this is the core of solution extraction, please correct the comments to clearly reflect the 0-based indexing used (y_i at 2*i, z_i at 2*i+1).
| // Variable integers are the first 2n elements: y_1, z_1, y_2, z_2, ... | |
| // If y_i is selected (index 2*(i-1) = 1), set x_i = 1 | |
| // If z_i is selected (index 2*(i-1)+1 = 1), set x_i = 0 | |
| // Variable integers are the first 2n elements in 0-based indexing: | |
| // for variable i (0 <= i < n), y_i is stored at index 2*i and z_i at index 2*i + 1. | |
| // If y_i is selected (target_solution[2*i] == 1), set x_i = 1; otherwise x_i = 0. |
| fn test_ksatisfiability_to_subsetsum_extract_solution_example() { | ||
| // Verify the specific example from the issue: | ||
| // x1=T, x2=T, x3=T → select y1, y2, y3, g1, h2, g2 | ||
| let ksat = KSatisfiability::<K3>::new( | ||
| 3, | ||
| vec![ | ||
| CNFClause::new(vec![1, 2, 3]), | ||
| CNFClause::new(vec![-1, -2, 3]), | ||
| ], | ||
| ); | ||
| let reduction = ReduceTo::<SubsetSum>::reduce_to(&ksat); | ||
|
|
||
| // Config: y1=1, z1=0, y2=1, z2=0, y3=1, z3=0, g1=1, h1=0, g2=0, h2=1 | ||
| // But we also need g2=1 to make it work. Let's verify with BruteForce. | ||
| let target = reduction.target_problem(); | ||
| let solver = BruteForce::new(); | ||
| let solution = solver.find_satisfying(target).unwrap(); | ||
| let extracted = reduction.extract_solution(&solution); | ||
| assert!(ksat.evaluate(&extracted)); |
There was a problem hiding this comment.
test_ksatisfiability_to_subsetsum_extract_solution_example is labeled as verifying the specific example assignment, but it only asks BruteForce for any satisfying SubsetSum solution and then checks that the extracted assignment satisfies the formula. This doesn't validate that the known example subset/assignment is extractable (and the comment above suggests uncertainty about the needed slack picks). Consider constructing the expected SubsetSum selection for the published example and asserting the extracted assignment matches the intended one (e.g., [1,1,1]), so the test actually pins down example correctness.
| _ => deser_opt::<ClosestVectorProblem<i32>>(data), | ||
| }, | ||
| "Knapsack" => deser_opt::<Knapsack>(data), | ||
| "SubsetSum" => deser_sat::<SubsetSum>(data), | ||
| _ => bail!("{}", crate::problem_name::unknown_problem_error(&canonical)), |
There was a problem hiding this comment.
The PR description mentions "CLI registration", but the CLI pred create path still doesn't support constructing SubsetSum instances from flags (no SubsetSum match arm in problemreductions-cli/src/commands/create.rs, and example_for() has no SubsetSum usage string). If CLI creation is intended as part of this PR, please add SubsetSum handling there (e.g., parse --sizes and --target), or adjust the PR description/scope to clarify that only JSON dispatch/alias registration is included.
- Fix misleading comments in extract_solution to use correct 0-based indexing description - Improve extract_solution test to construct the specific expected subset selection and verify the known assignment x1=T, x2=T, x3=T Co-Authored-By: Claude Opus 4.6 <[email protected]>
PR #599 (KSat→SubsetSum): Fix imprecise Karp 1972 attribution — the direct 3-SAT→SubsetSum digit encoding follows Sipser (2012, Thm 7.56) and CLRS (2022, §34.5.5), not Karp's original reduction tree. Add bib entries for both textbooks. PR #570 (GraphPartitioning): Add proper @Citations for Garey, Johnson & Stockmeyer (1976) and Arora, Rao & Vazirani (2009) instead of plain-text references. Add bib entries for both papers. Regenerate problem_schemas.json and reduction_graph.json. Co-Authored-By: Claude Opus 4.6 <[email protected]>
* fix: address issue review comments for #126 and #117 PR #599 (KSat→SubsetSum): Fix imprecise Karp 1972 attribution — the direct 3-SAT→SubsetSum digit encoding follows Sipser (2012, Thm 7.56) and CLRS (2022, §34.5.5), not Karp's original reduction tree. Add bib entries for both textbooks. PR #570 (GraphPartitioning): Add proper @Citations for Garey, Johnson & Stockmeyer (1976) and Arora, Rao & Vazirani (2009) instead of plain-text references. Add bib entries for both papers. Regenerate problem_schemas.json and reduction_graph.json. Co-Authored-By: Claude Opus 4.6 <[email protected]> * fix: add FPT complexity citation for GraphPartitioning (#117) Address review comment: explicitly state that brute-force O*(2^n) is the best known unconditional exact algorithm, and cite Cygan et al. (STOC 2014 / SICOMP 2019) for the FPT result parameterized by bisection width. Co-Authored-By: Claude Opus 4.6 <[email protected]> * fix: use sort_by_key per clippy unnecessary_sort_by lint Co-Authored-By: Claude Opus 4.6 <[email protected]> * feat: add merge-with-main conflict resolution step to review-pipeline Add Step 1a between checkout and Copilot fixes to merge origin/main into the PR branch. Resolves simple conflicts automatically; aborts and reports for complex conflicts needing manual resolution. Co-Authored-By: Claude Opus 4.6 <[email protected]> * update pipeline skills: eligibility-first sorting, merge-with-main project-pipeline: Reorder Steps 0c/0d so eligibility check (source and target models exist) runs before scoring. Only eligible issues get scored. review-pipeline: Add Step 1a to merge origin/main into the PR branch before fixing Copilot comments, catching conflicts early. Co-Authored-By: Claude Opus 4.6 <[email protected]> --------- Co-authored-by: Claude Opus 4.6 <[email protected]>
Summary
src/models/misc/Fixes #126