Skip to content

feat: batch add 14 reduction rules (hard rules phase 2)#1028

Merged
GiggleLiu merged 25 commits intomainfrom
jg/hard-rules-2
Apr 10, 2026
Merged

feat: batch add 14 reduction rules (hard rules phase 2)#1028
GiggleLiu merged 25 commits intomainfrom
jg/hard-rules-2

Conversation

@GiggleLiu
Copy link
Copy Markdown
Contributor

Summary

  • Add 14 new reduction rules connecting isolated/sparse problem nodes in the reduction graph
  • Fix bounded path search in domination analysis to prevent SIGKILL on large graphs
  • Add affine relation regression test for MAX-2-SAT → MaxCut

New reductions (by category):

Decision wrapper reductions (Batch 2):

Connecting isolated nodes (Batch 3):

Adding density:

Bug fixes:

  • Fix MaximumLikelihoodRanking to allow negative matrix entries (c=0 skew-symmetric)
  • Bound domination analysis path search to prevent OOM/SIGKILL

Test plan

  • cargo fmt --check passes
  • cargo clippy clean (0 warnings)
  • cargo test passes (4976+ tests)
  • All new reductions have closed-loop tests
  • Paper entries for new reductions (follow-up)
  • make regenerate-fixtures for canonical examples (follow-up)

🤖 Generated with Claude Code

GiggleLiu and others added 17 commits April 8, 2026 11:18
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>
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines 683 to 687
Vec<NodeIndex>,
_,
std::hash::RandomState,
>(&self.graph, src, dst, 0, None)
>(&self.graph, src, dst, 0, max_intermediate_nodes)
.take(limit)
Copy link

Copilot AI Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copilot uses AI. Check for mistakes.
GiggleLiu and others added 6 commits April 10, 2026 16:29
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
Copy link
Copy Markdown

codecov bot commented Apr 10, 2026

Codecov Report

❌ Patch coverage is 95.21136% with 145 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.97%. Comparing base (a784239) to head (9fa0c6c).
⚠️ Report is 4 commits behind head on main.

Files with missing lines Patch % Lines
src/models/graph/minimum_dominating_set.rs 56.86% 66 Missing ⚠️
...s/decisionminimumvertexcover_hamiltoniancircuit.rs 90.58% 29 Missing ⚠️
src/rules/graph.rs 54.54% 10 Missing ⚠️
src/models/misc/register_sufficiency.rs 90.52% 9 Missing ⚠️
...s/ksatisfiability_quadraticdiophantineequations.rs 89.06% 7 Missing ⚠️
...odels/algebraic/quadratic_diophantine_equations.rs 96.63% 4 Missing ⚠️
...rtexset_minimumcodegenerationunlimitedregisters.rs 95.50% 4 Missing ⚠️
...s/partitionintocliques_minimumcoveringbycliques.rs 97.88% 4 Missing ⚠️
src/unit_tests/reduction_graph.rs 94.59% 4 Missing ⚠️
src/models/decision.rs 84.21% 3 Missing ⚠️
... and 2 more
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.
📢 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 and others added 2 commits April 11, 2026 00:13
…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>
@GiggleLiu GiggleLiu merged commit 0f9db3c into main Apr 10, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants