feat: batch implement reduction rules (phases 1-3)#1017
Merged
Conversation
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…905) Implements Sethi's Reduction 3 / Theorem 5.11 with p/q/r/rbar clause gadgets, cyclic links, and shared-register variable leaf pairs. Also adds the companion FeasibleRegisterAssignment → ILP rule. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR expands the reduction catalog by implementing multiple new polynomial-time reductions (including SAT-branch connectivity, 3SAT gadgets, and several ILP companion formulations), and updates the paper/test suite to cover the new edges—including explicitly “proof-only” embeddings that are intentionally not solver-executable.
Changes:
- Add new reductions: CircuitSAT→SAT (Tseitin), SAT→MAX-2-SAT (GJS gadget), MAX-2-SAT→MaxCut, and several 3SAT-based constructions (e.g., →Decision MVC, →MonochromaticTriangle, →FeasibleRegisterAssignment, →DirectedTwoCommodityIntegralFlow).
- Add ILP companion reductions for MonochromaticTriangle, MinimumCoveringByCliques, IntegerKnapsack, and FeasibleRegisterAssignment; adjust D2CIF→ILP conservation semantics to match the model definition.
- Add proof-only edges (e.g., SubsetSum→IntegerKnapsack, MVC→MinimumMaximalMatching) and integrate them into example-db/paper + tests.
Reviewed changes
Copilot reviewed 43 out of 43 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/suites/register_assignment_reductions.rs | New integration tests for KSAT→FRA and FRA→ILP closed loops |
| tests/suites/reductions.rs | Add integration tests for MinimumCoveringByCliques→ILP and MAX-2-SAT→MaxCut |
| tests/main.rs | Register the new integration test suite module |
| src/unit_tests/rules/subsetsum_integerknapsack.rs | Unit tests demonstrating forward embedding + backward gap |
| src/unit_tests/rules/satisfiability_maximum2satisfiability.rs | Unit tests for SAT→MAX-2-SAT structure/closed-loop/gaps |
| src/unit_tests/rules/registry.rs | Extend EdgeCapabilities tests for none() |
| src/unit_tests/rules/monochromatictriangle_ilp.rs | Unit tests for MonochromaticTriangle→ILP constraints and feasibility |
| src/unit_tests/rules/minimumvertexcover_minimummaximalmatching.rs | Unit tests validating proof-only MVC→MMM relationship/gap |
| src/unit_tests/rules/minimumcoveringbycliques_ilp.rs | Unit tests for MinimumCoveringByCliques→ILP formulation and round-trip |
| src/unit_tests/rules/maximum2satisfiability_maxcut.rs | Unit tests for MAX-2-SAT→MaxCut correctness and edge weights |
| src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs | Unit tests for 3SAT→MonochromaticTriangle gadget + extraction |
| src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs | Unit tests for 3SAT→FRA gadget structure/extraction/ILP loop |
| src/unit_tests/rules/ksatisfiability_directedtwocommodityintegralflow.rs | Unit tests for 3SAT→D2CIF structure, encoding, and ILP loop |
| src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs | Unit tests for 3SAT→Decision MVC wrapper reduction |
| src/unit_tests/rules/integerknapsack_ilp.rs | Unit tests for IntegerKnapsack→ILP bounds/objective extraction |
| src/unit_tests/rules/graph.rs | Registry/path existence tests for new reductions |
| src/unit_tests/rules/feasibleregisterassignment_ilp.rs | Unit tests for FRA→ILP structure/round-trip/infeasibility |
| src/unit_tests/rules/directedtwocommodityintegralflow_ilp.rs | Update tests for revised conservation constraints; add regression |
| src/unit_tests/rules/circuit_sat.rs | Unit tests for CircuitSAT→SAT (Tseitin) correctness/counts |
| src/unit_tests/reduction_graph.rs | Assert new proof-only edges and runtime witness edges are correctly flagged |
| src/unit_tests/models/misc/feasible_register_assignment.rs | Add tests for num_same_register_pairs() |
| src/unit_tests/models/graph/directed_two_commodity_integral_flow.rs | Regression test: disallow using other commodity’s source |
| src/unit_tests/example_db.rs | Allow example-db consistency checks to tolerate proof-only edges |
| src/rules/subsetsum_integerknapsack.rs | Register SubsetSum→IntegerKnapsack as proof-only edge + canonical example |
| src/rules/satisfiability_maximum2satisfiability.rs | Implement SAT→MAX-2-SAT reduction (normalization + GJS gadget) |
| src/rules/registry.rs | Add EdgeCapabilities::none() helper |
| src/rules/monochromatictriangle_ilp.rs | Implement MonochromaticTriangle→ILP feasibility formulation |
| src/rules/mod.rs | Wire up new rule modules and canonical examples |
| src/rules/minimumvertexcover_minimummaximalmatching.rs | Register MVC→MMM as proof-only identity edge |
| src/rules/minimumcoveringbycliques_ilp.rs | Implement MinimumCoveringByCliques→ILP with McCormick linearization |
| src/rules/maximum2satisfiability_maxcut.rs | Implement MAX-2-SAT→MaxCut reduction via accumulated signed weights |
| src/rules/ksatisfiability_monochromatictriangle.rs | Implement 3SAT→MonochromaticTriangle gadget + symmetry-aware extraction |
| src/rules/ksatisfiability_feasibleregisterassignment.rs | Implement Sethi Reduction 3: 3SAT→FeasibleRegisterAssignment |
| src/rules/ksatisfiability_directedtwocommodityintegralflow.rs | Implement padded occurrence-lobe 3SAT→D2CIF reduction + encoding helper |
| src/rules/ksatisfiability_decisionminimumvertexcover.rs | Implement 3SAT→Decision wrapper |
| src/rules/integerknapsack_ilp.rs | Implement IntegerKnapsack→ILP with explicit multiplicity upper bounds |
| src/rules/feasibleregisterassignment_ilp.rs | Implement FRA→ILP formulation (ordering + live-range non-overlap) |
| src/rules/directedtwocommodityintegralflow_ilp.rs | Fix D2CIF→ILP conservation to exclude only own source/sink per commodity |
| src/rules/circuit_sat.rs | Implement CircuitSAT→SAT Tseitin encoding + normalization/constant folding |
| src/models/misc/feasible_register_assignment.rs | Add num_same_register_pairs() helper used by ILP overhead/tests |
| src/models/graph/monochromatic_triangle.rs | Add num_triangles() helper |
| src/models/graph/directed_two_commodity_integral_flow.rs | Adjust model definition/evaluation for commodity-specific terminals |
| docs/paper/reductions.typ | Document new rules (including proof-only notes) and update paper text/examples |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
6
to
+12
| use problemreductions::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; | ||
| use problemreductions::models::graph::MinimumCoveringByCliques; | ||
| use problemreductions::prelude::*; | ||
| use problemreductions::rules::{Minimize, ReductionGraph}; | ||
| use problemreductions::solvers::ILPSolver; | ||
| use problemreductions::topology::{Graph, SimpleGraph}; | ||
| use problemreductions::types::Min; |
There was a problem hiding this comment.
ILPSolver is only re-exported when the ilp-solver feature is enabled (see problemreductions::solvers), but this file imports it unconditionally. This will break compilation of the test suite when ilp-solver is disabled. Gate the ILPSolver import (and any code that needs it) behind #[cfg(feature = "ilp-solver")], or move the import inside the already-cfgd module.
Comment on lines
+1
to
+7
| use problemreductions::models::algebraic::ILP; | ||
| use problemreductions::models::formula::{CNFClause, KSatisfiability}; | ||
| use problemreductions::models::misc::FeasibleRegisterAssignment; | ||
| use problemreductions::prelude::*; | ||
| use problemreductions::rules::{MinimizeSteps, ReductionGraph, ReductionPath}; | ||
| use problemreductions::solvers::ILPSolver; | ||
| use problemreductions::types::{Or, ProblemSize}; |
There was a problem hiding this comment.
This integration test suite uses ILPSolver and ILP reductions but is not gated behind #[cfg(feature = "ilp-solver")]. Since ILPSolver is only available with that feature, the crate’s tests will fail to compile in non-ILP builds. Consider gating the whole file (or at least both tests + the ILPSolver import) behind feature = "ilp-solver", similar to other suites.
Comment on lines
10
to
14
| mod ksatisfiability_simultaneous_incongruences; | ||
| #[path = "suites/register_assignment_reductions.rs"] | ||
| mod register_assignment_reductions; | ||
| #[path = "suites/reductions.rs"] | ||
| mod reductions; |
There was a problem hiding this comment.
tests/suites/register_assignment_reductions.rs appears to require the ilp-solver feature, but this module is included unconditionally. If ilp-solver is disabled, the test build will fail due to missing ILPSolver/ILP reductions. Gate this mod register_assignment_reductions; behind #[cfg(feature = "ilp-solver")] (or gate the module contents).
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #1017 +/- ##
==========================================
- Coverage 98.12% 98.12% -0.01%
==========================================
Files 923 949 +26
Lines 95916 98044 +2128
==========================================
+ Hits 94120 96201 +2081
- Misses 1796 1843 +47 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Add reduction-rule entries for KSatisfiability → FeasibleRegisterAssignment (Sethi Reduction 3) and FeasibleRegisterAssignment → ILP. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Address Copilot review comments: ILPSolver and related imports in integration tests were unconditional but only used in feature-gated blocks. Gate them with #[cfg(feature = "ilp-solver")]. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Witness-capable reductions (Phase 1)
Phase 2 (investigate and fix)
Phase 3 (one-directional)
Issues updated
Test plan
make testpassesmake clippypassesmake papercompiles🤖 Generated with Claude Code