feat: batch add 14 reduction rules (hard rules phase 2)#1028
feat: batch add 14 reduction rules (hard rules phase 2)#1028
Conversation
Implements Sethi's Reduction I / Theorem 3.11 for KSatisfiability<K3> → RegisterSufficiency with corrected extraction (stop at w[n], read x_pos[k], "at most one"). Also adds RegisterSufficiency → ILP companion rule. Closes #872 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…metric) The GJ definition uses "antisymmetric" which means a_ij + a_ji = c including c=0 (skew-symmetric with negative entries). Remove the non-negative constraint, keep constant-sum validation. Add test for c=0 encoding of a directed 3-cycle. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Fix manual_memcpy and needless_range_loop in FVS→CodeGen reduction - Fix manual_div_ceil in QuadraticDiophantineEquations - Allow too_many_arguments for bounded path search - Relax find_paths_up_to test assertion for bounded search behavior - Apply rustfmt to touched files Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds a second batch of reduction rules to connect previously sparse/isolated nodes in the reduction graph, and hardens reduction-graph domination analysis to avoid runaway path enumeration on large graphs. It also expands unit/integration coverage around the new rules and updates a few affected models (FaultDetection semantics, MaximumLikelihoodRanking matrix validation, QuadraticDiophantineEquations bigint encoding).
Changes:
- Add multiple new reductions (incl. decision-wrapper reductions and “density” edges) with closed-loop/unit tests and example-db specs.
- Fix/limit reduction-graph path enumeration used in domination analysis to prevent OOM/SIGKILL on dense graphs.
- Update several models/test suites to support the new reductions (e.g., QDE BigUint witness encoding, MLR allowing negative/skew-symmetric matrices, FaultDetection internal-vertex semantics).
Reviewed changes
Copilot reviewed 50 out of 50 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| tests/suites/register_assignment_reductions.rs | Formatting-only updates to assertions for readability. |
| tests/suites/reductions.rs | Adds integration tests for PartitionIntoCliques -> MinimumCoveringByCliques. |
| tests/main.rs | Ensures reductions suite is always included (not feature-gated). |
| src/unit_tests/rules/registersufficiency_ilp.rs | Unit tests for RegisterSufficiency -> ILP (structure + closed-loop + example-db spec). |
| src/unit_tests/rules/partitionintocliques_minimumcoveringbycliques.rs | Unit tests for Orlin reduction correctness and extraction behavior. |
| src/unit_tests/rules/minimumvertexcover_minimumweightandorgraph.rs | Unit tests for MinimumVertexCover -> MinimumWeightAndOrGraph (incl. weighted sink-arc charging). |
| src/unit_tests/rules/minimumfeedbackvertexset_minimumcodegenerationunlimitedregisters.rs | Closed-loop test for MinimumFeedbackVertexSet -> MinimumCodeGenerationUnlimitedRegisters. |
| src/unit_tests/rules/minimumfeedbackarcset_maximumlikelihoodranking.rs | Unit tests for MinimumFeedbackArcSet -> MaximumLikelihoodRanking (matrix + extraction + constraints). |
| src/unit_tests/rules/maximum2satisfiability_maxcut.rs | Adds affine-relation regression test over all MaxCut partitions for the issue instance. |
| src/unit_tests/rules/ksatisfiability_registersufficiency.rs | Unit tests for 3SAT -> RegisterSufficiency (structure + extraction + optional ILP loop). |
| src/unit_tests/rules/ksatisfiability_quadraticdiophantineequations.rs | Closed-loop tests for 3SAT -> QuadraticDiophantineEquations and reference-witness encoding. |
| src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs | Formatting-only updates to assertions for readability. |
| src/unit_tests/rules/kcoloring_clustering.rs | Unit tests for KColoring(K=3) -> Clustering (distance matrix + edge cases). |
| src/unit_tests/rules/exactcoverby3sets_minimumfaultdetectiontestset.rs | Unit tests for X3C -> MinimumFaultDetectionTestSet (gap + structure + identity extraction). |
| src/unit_tests/rules/exactcoverby3sets_minimumaxiomset.rs | Unit tests for X3C -> MinimumAxiomSet (gap + structure + extraction behavior). |
| src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs | Unit tests for Decision<MVC> -> HamiltonianCircuit (counts + witness + corner cases). |
| src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs | Unit tests for Decision<MDS> -> MinMaxMulticenter (structure + closed-loop). |
| src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs | Unit tests for Decision<MDS> -> MinimumSumMulticenter (YES/NO instances). |
| src/unit_tests/reduction_graph.rs | Adds discovery tests for newly registered reductions + adjusts path-limit test expectations. |
| src/unit_tests/models/misc/minimum_fault_detection_test_set.rs | Updates tests to reflect “internal vertices only” semantics + adds a boundary-only case. |
| src/unit_tests/models/misc/maximum_likelihood_ranking.rs | Adds tests for comparison_count and skew-symmetric matrices. |
| src/unit_tests/models/algebraic/quadratic_diophantine_equations.rs | Updates tests for BigUint-based encoding/serialization and witness round-trips. |
| src/rules/registersufficiency_ilp.rs | Implements RegisterSufficiency -> ILP<i32> reduction with overhead metadata and example-db spec. |
| src/rules/partitionintocliques_minimumcoveringbycliques.rs | Implements Orlin reduction PartitionIntoCliques -> MinimumCoveringByCliques + extraction logic. |
| src/rules/mod.rs | Registers the new rule modules and wires canonical example specs. |
| src/rules/minimumvertexcover_minimumweightandorgraph.rs | Implements MinimumVertexCover -> MinimumWeightAndOrGraph reduction + example-db spec. |
| src/rules/minimumfeedbackvertexset_minimumcodegenerationunlimitedregisters.rs | Implements Aho–Johnson–Ullman chain gadget reduction for unlimited-register codegen. |
| src/rules/minimumfeedbackarcset_maximumlikelihoodranking.rs | Implements unit-weight FAS -> MLR via skew-symmetric (c=0) matrix encoding. |
| src/rules/ksatisfiability_registersufficiency.rs | Implements Sethi 3SAT -> RegisterSufficiency reduction with corrected extraction rule. |
| src/rules/ksatisfiability_quadraticdiophantineequations.rs | Implements 3SAT -> QDE by translating existing quadratic congruence construction. |
| src/rules/ksatisfiability_feasibleregisterassignment.rs | Minor formatting change in extraction logic for readability. |
| src/rules/kcoloring_clustering.rs | Implements 3-Coloring -> Clustering reduction (0/1 distances, K=3, B=0). |
| src/rules/graph.rs | Adds bounded path enumeration API used by domination analysis and find_paths_up_to*. |
| src/rules/feasibleregisterassignment_ilp.rs | Minor formatting change (constraint vec construction) for readability. |
| src/rules/exactcoverby3sets_minimumfaultdetectiontestset.rs | Implements X3C -> MinimumFaultDetectionTestSet reduction (single-output DAG). |
| src/rules/exactcoverby3sets_minimumaxiomset.rs | Implements X3C -> MinimumAxiomSet reduction (4 implications per subset). |
| src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs | Implements G&J Thm 3.4 gadget reduction for decision MVC to Hamiltonian circuit. |
| src/rules/decisionminimumdominatingset_minmaxmulticenter.rs | Implements Decision<MDS> -> MinMaxMulticenter (unit weights/lengths, radius-1 equivalence). |
| src/rules/decisionminimumdominatingset_minimumsummulticenter.rs | Implements Decision<MDS> -> MinimumSumMulticenter (unit weights/lengths, sum bound property). |
| src/rules/analysis.rs | Uses bounded path enumeration to avoid blowups during dominated-rule detection. |
| src/models/misc/register_sufficiency.rs | Adds num_sinks() helper used in reduction overhead/counts. |
| src/models/misc/mod.rs | Updates model docs to reflect FaultDetection “internal vertices” semantics. |
| src/models/misc/minimum_fault_detection_test_set.rs | Changes objective feasibility to cover internal vertices only and updates schema/notes. |
| src/models/misc/maximum_likelihood_ranking.rs | Validates constant pairwise sum (c) and exposes comparison_count(). |
| src/models/graph/minimum_dominating_set.rs | Adds One weight variant and registers decision variant inventory entries for One. |
| src/models/graph/min_max_multicenter.rs | Adds One weight variant declaration. |
| src/models/formula/ksat.rs | Adds register_sufficiency_padding() accessor for overhead expressions. |
| src/models/algebraic/quadratic_diophantine_equations.rs | Switches to BigUint coefficients and binary witness encoding; updates schema/size fields/variants. |
| docs/paper/references.bib | Adds bibliography entries supporting new reductions (Brucker/Orlin/Kou-Stockmeyer-Wong). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| Vec<NodeIndex>, | ||
| _, | ||
| std::hash::RandomState, | ||
| >(&self.graph, src, dst, 0, None) | ||
| >(&self.graph, src, dst, 0, max_intermediate_nodes) | ||
| .take(limit) |
There was a problem hiding this comment.
petgraph::algo::all_simple_paths interprets the last argument as a maximum path length in edges (hops), not “max intermediate nodes”. Passing max_intermediate_nodes directly will undercount by ~1 (intermediate_nodes = hops - 1), and the doc comment is currently misleading. Consider either (a) renaming this parameter to max_hops and updating the doc, or (b) translating via max_hops = max_intermediate_nodes.map(|k| k + 1) before calling all_simple_paths so the bound matches the stated semantics.
The KSat→RS canonical example builds a 70-vertex RegisterSufficiency instance. Solving it through the RS→ILP chain (17K vars, 52K constraints) took 50+ seconds locally and timed out CI at 56 minutes. Add solve_exact() to RegisterSufficiency: a branch-and-bound solver with heuristic candidate ordering (prefer vertices that free the most registers). YES instances resolve instantly on the first greedy path without backtracking. For NO instances the full search tree must be explored, so the ILP path is kept for infeasibility proofs. Test time for KSat→RS suite: 278s → 9s. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Clustering→ILP: binary assignment variables x[i,c], exact-one-cluster constraints per element, conflict constraints for violated distance pairs. Feasibility formulation (minimize 0). O(n·K) variables, O(n + n²·K) constraints. MinimumFaultDetectionTestSet→ILP: binary selection variables per input-output pair, covering constraints requiring each internal vertex appears in at least one selected pair's coverage set. Minimize total selected pairs. O(|I|·|O|) variables, O(internal vertices) constraints. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Fix Clustering→ILP overhead: use n*(n-1)/2 instead of n² for pair count - Fix MFDTS→ILP overhead: num_constraints covers internal vertices only - Add num_edges to Decision<MDS>→MinSumMulticenter overhead - Add 3 missing paper reduction-rule entries (KSat→QDE, FVS→CodeGen, MVC→AndOrGraph) - Rename DecisionMVC→HC test to include closed_loop - Replace slow KSat→RS UNSAT test (ILP on 17K vars) with BF + structural check - Add 5s test time limit rule to CLAUDE.md Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Use ILP solver on target + brute force on source instead of brute-force enumerating all 2^24 ILP configurations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The new DecisionMVC→HamiltonianCircuit reduction created a path DecisionMVC → HC(50 verts) → QA(2500 vars) → ILP that HiGHS can't solve in reasonable time. Fix: try brute force first for small instances (≤2^20 configs) before falling back to ILP via reduction. DecisionMVC with 4 vertices has only 16 configs — instant via brute force. Also add CLAUDE.md note: overhead expressions describe scaling, not exact sizes — read reduce_to() code for actual sizes. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Previously Decision<P> → P was aggregate-only, forcing witness-mode path search through expensive chains (e.g., DecisionMVC → HC → QA → ILP). Now the edge supports both witness and aggregate modes — a P-witness meeting the bound is directly a Decision<P> witness (identity config). - Add DecisionToOptimizationWitnessResult and ReduceTo<P> for Decision<P> - Merge register_decision_variant! macro to emit single both() edge - Add witness edge + canonical example for Decision<MDS<SG,One>> variant - Update dominated rules allow-list (KSat→MVC now dominated via DecisionMVC) - Fix CLI truncation test (MIS→QUBO path count changed due to new edges) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #1028 +/- ##
==========================================
- Coverage 98.12% 97.97% -0.15%
==========================================
Files 949 979 +30
Lines 98044 100912 +2868
==========================================
+ Hits 96201 98868 +2667
- Misses 1843 2044 +201 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
…l_value keys - Cast a/b/c from JSON strings to int for QuadraticDiophantineEquations example - Compute MVC→AndOrGraph target weight from arc_weights instead of missing optimal_value - Compute FVS→CodeGen instruction count from target_config length instead of missing optimal_value Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Exercises the bounded path search with tight and zero intermediate-node limits, covering the previously-untested function body in graph.rs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Summary
New reductions (by category):
Decision wrapper reductions (Batch 2):
Connecting isolated nodes (Batch 3):
Adding density:
Bug fixes:
Test plan
cargo fmt --checkpassescargo clippyclean (0 warnings)cargo testpasses (4976+ tests)make regenerate-fixturesfor canonical examples (follow-up)🤖 Generated with Claude Code