feat: batch implement reduction rules (phases 1-3) (#1017)

* Add CircuitSAT to Satisfiability reduction (#970)

* Add Maximum2Satisfiability to MaxCut reduction

* feat: add satisfiability to maximum2satisfiability reduction

* feat: add KSAT to decision MVC reduction

* feat: add 3sat to directed two-commodity flow

* Add MonochromaticTriangle reductions

* style: format ksatisfiability_directedtwocommodityintegralflow

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* feat: add proof-only mvc to mmm rule

* feat: add MinimumCoveringByCliques to ILP

* feat: add SubsetSum and IntegerKnapsack reductions

* feat: add 3SAT to FeasibleRegisterAssignment + FRA to ILP reductions (#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>

* docs: add paper entries for FRA reductions (#905)

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>

* fix: gate ILPSolver imports behind ilp-solver feature

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>

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: GiggleLiu

docs/paper/reductions.typ

@@ -39,7 +39,7 @@ inventory::submit! {
 /// whether two integral flow functions f_1, f_2: A -> Z_0^+ exist such that:
 /// 1. Joint capacity: f_1(a) + f_2(a) <= c(a) for all a in A
 /// 2. Flow conservation: for each commodity i, flow is conserved at every
-///    vertex except the four terminals
+///    vertex except its own source and sink
 /// 3. Requirements: net flow into t_i under f_i is at least R_i
 ///
 /// # Variables
@@ -191,8 +191,6 @@ impl DirectedTwoCommodityIntegralFlow {
             return false;
         }
         let arcs = self.graph.arcs();
-        let terminals = [self.source_1, self.sink_1, self.source_2, self.sink_2];
-
         // (1) Joint capacity constraint
         for a in 0..m {
             let f1 = config[a] as u64;
@@ -216,8 +214,18 @@ impl DirectedTwoCommodityIntegralFlow {
         }
 
         for (commodity, commodity_balances) in balances.iter().enumerate() {
+            let src = if commodity == 0 {
+                self.source_1
+            } else {
+                self.source_2
+            };
             for (v, &balance) in commodity_balances.iter().enumerate() {
-                if !terminals.contains(&v) && balance != 0 {
+                let snk = if commodity == 0 {
+                    self.sink_1
+                } else {
+                    self.sink_2
+                };
+                if v != src && v != snk && balance != 0 {
                     return false;
                 }
             }

src/models/graph/directed_two_commodity_integral_flow.rs

@@ -125,6 +125,11 @@ impl<G: Graph> MonochromaticTriangle<G> {
         &self.triangles
     }
 
+    /// Get the number of triangles in the graph.
+    pub fn num_triangles(&self) -> usize {
+        self.triangles.len()
+    }
+
     /// Get the ordered edge list.
     pub fn edge_list(&self) -> &[(usize, usize)] {
         &self.edge_list

src/models/graph/monochromatic_triangle.rs

@@ -187,6 +187,18 @@ impl FeasibleRegisterAssignment {
         self.num_registers
     }
 
+    /// Count unordered vertex pairs that share a register.
+    pub fn num_same_register_pairs(&self) -> usize {
+        let mut counts = vec![0usize; self.num_registers];
+        for &register in &self.assignment {
+            counts[register] += 1;
+        }
+        counts
+            .into_iter()
+            .map(|count| count.saturating_sub(1) * count / 2)
+            .sum()
+    }
+
     /// Get the arcs.
     pub fn arcs(&self) -> &[(usize, usize)] {
         &self.arcs