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