feat: add QUBO→ILP and CircuitSAT→ILP reductions

docs/paper/reductions.typ

@@ -608,6 +608,57 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Solution extraction._ Discard slack variables: return $bold(x)' [0..n]$.
 ]
 
+#let qubo_ilp = load-example("qubo_to_ilp")
+#let qubo_ilp_r = load-results("qubo_to_ilp")
+#let qubo_ilp_sol = qubo_ilp_r.solutions.at(0)
+#reduction-rule("QUBO", "ILP",
+  example: true,
+  example-caption: [4-variable QUBO with 3 quadratic terms],
+  extra: [
+    Source: $n = #qubo_ilp.source.instance.num_vars$ binary variables, 3 off-diagonal terms \
+    Target: #qubo_ilp.target.instance.num_vars ILP variables ($#qubo_ilp.source.instance.num_vars$ original $+ #(qubo_ilp.target.instance.num_vars - qubo_ilp.source.instance.num_vars)$ auxiliary), 9 McCormick constraints \
+    Optimal: $bold(x) = (#qubo_ilp_sol.source_config.map(str).join(", "))$ ($#qubo_ilp_r.solutions.len()$-fold degenerate) #sym.checkmark
+  ],
+)[
+  McCormick linearization: for each product $x_i x_j$ ($i < j$) with $Q_(i j) != 0$, introduce auxiliary $y_(i j)$ with three linear constraints.
+][
+  _Diagonal terms._ For binary $x_i$: $Q_(i i) x_i^2 = Q_(i i) x_i$, which is directly linear.
+
+  _Off-diagonal terms._ For each non-zero $Q_(i j)$ ($i < j$), introduce binary $y_(i j) = x_i dot x_j$ with McCormick constraints:
+  $ y_(i j) <= x_i, quad y_(i j) <= x_j, quad y_(i j) >= x_i + x_j - 1 $
+  These constraints enforce $y_(i j) = x_i x_j$ for binary variables.
+
+  _ILP formulation._ Minimize $sum_i Q_(i i) x_i + sum_(i < j) Q_(i j) y_(i j)$ subject to the McCormick constraints and $x_i, y_(i j) in {0, 1}$.
+
+  _Solution extraction._ Return the first $n$ variables (discard auxiliary $y_(i j)$).
+]
+
+#let cs_ilp = load-example("circuitsat_to_ilp")
+#let cs_ilp_r = load-results("circuitsat_to_ilp")
+#reduction-rule("CircuitSAT", "ILP",
+  example: true,
+  example-caption: [1-bit full adder to ILP],
+  extra: [
+    Circuit: #cs_ilp.source.instance.num_gates gates (2 XOR, 2 AND, 1 OR), #cs_ilp.source.instance.num_variables variables \
+    Target: #cs_ilp.target.instance.num_vars ILP variables (circuit vars $+$ auxiliary), trivial objective \
+    #cs_ilp_r.solutions.len() feasible solutions ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
+  ],
+)[
+  Each gate maps to linear constraints over binary variables; any feasible ILP solution is a satisfying circuit assignment.
+][
+  _Tseitin flattening._ Recursively assign an ILP variable to each expression node. Named circuit variables keep their identity; internal nodes get auxiliary variables.
+
+  _Gate encodings_ (output $c$, inputs $a_1, ..., a_k$, all binary):
+  - NOT: $c + a = 1$
+  - AND: $c <= a_i$ ($forall i$), $c >= sum a_i - (k - 1)$
+  - OR: $c >= a_i$ ($forall i$), $c <= sum a_i$
+  - XOR (binary, chained pairwise): $c <= a + b$, $c >= a - b$, $c >= b - a$, $c <= 2 - a - b$
+
+  _Objective._ Minimize $0$ (feasibility problem): any feasible solution satisfies the circuit.
+
+  _Solution extraction._ Return values of the named circuit variables.
+]
+
 == Non-Trivial Reductions
 
 #let sat_mis = load-example("satisfiability_to_maximumindependentset")

docs/src/reductions/reduction_graph.json

@@ -208,6 +208,21 @@
     }
   ],
   "edges": [
+    {
+      "source": 0,
+      "target": 2,
+      "overhead": [
+        {
+          "field": "num_vars",
+          "formula": "num_variables + num_assignments"
+        },
+        {
+          "field": "num_constraints",
+          "formula": "num_variables + num_assignments"
+        }
+      ],
+      "doc_path": "rules/circuit_ilp/index.html"
+    },
     {
       "source": 0,
       "target": 23,
@@ -762,6 +777,21 @@
       ],
       "doc_path": "rules/minimumvertexcover_qubo/index.html"
     },
+    {
+      "source": 20,
+      "target": 2,
+      "overhead": [
+        {
+          "field": "num_vars",
+          "formula": "num_vars^2"
+        },
+        {
+          "field": "num_constraints",
+          "formula": "num_vars^2"
+        }
+      ],
+      "doc_path": "rules/qubo_ilp/index.html"
+    },
     {
       "source": 20,
       "target": 22,

examples/reduction_circuitsat_to_ilp.rs

@@ -0,0 +1,169 @@
+// # Circuit-SAT to ILP Reduction
+//
+// ## Mathematical Equivalence
+// Each logic gate (AND, OR, NOT, XOR) is encoded as linear constraints over
+// binary variables. The expression tree is flattened by introducing an auxiliary
+// variable per internal node (Tseitin-style). Any feasible ILP solution is a
+// satisfying circuit assignment.
+//
+// ## This Example
+// - Instance: 1-bit full adder circuit (a, b, cin -> sum, cout)
+//   - sum = a XOR b XOR cin (via intermediate t = a XOR b)
+//   - cout = (a AND b) OR (cin AND t)
+//   - 5 gates (2 XOR, 2 AND, 1 OR), ~8 variables
+// - Source: CircuitSAT with 3 inputs
+// - Target: ILP (feasibility, trivial objective)
+//
+// ## Output
+// Exports `docs/paper/examples/circuitsat_to_ilp.json` and `circuitsat_to_ilp.result.json`.
+//
+// ## Usage
+// ```bash
+// cargo run --example reduction_circuitsat_to_ilp --features ilp-solver
+// ```
+
+use problemreductions::export::*;
+use problemreductions::models::optimization::ILP;
+use problemreductions::models::specialized::{Assignment, BooleanExpr, Circuit};
+use problemreductions::prelude::*;
+
+pub fn run() {
+    // 1. Create CircuitSAT instance: 1-bit full adder
+    //    sum = a XOR b XOR cin, cout = (a AND b) OR (cin AND (a XOR b))
+    //    Decomposed into 5 gates with intermediate variables t, ab, cin_t.
+    let circuit = Circuit::new(vec![
+        // Intermediate: t = a XOR b
+        Assignment::new(
+            vec!["t".to_string()],
+            BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
+        ),
+        // sum = t XOR cin
+        Assignment::new(
+            vec!["sum".to_string()],
+            BooleanExpr::xor(vec![BooleanExpr::var("t"), BooleanExpr::var("cin")]),
+        ),
+        // ab = a AND b
+        Assignment::new(
+            vec!["ab".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
+        ),
+        // cin_t = cin AND t
+        Assignment::new(
+            vec!["cin_t".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("cin"), BooleanExpr::var("t")]),
+        ),
+        // cout = ab OR cin_t
+        Assignment::new(
+            vec!["cout".to_string()],
+            BooleanExpr::or(vec![BooleanExpr::var("ab"), BooleanExpr::var("cin_t")]),
+        ),
+    ]);
+    let circuit_sat = CircuitSAT::new(circuit);
+
+    println!("=== Circuit-SAT to ILP Reduction ===\n");
+    println!("Source circuit: 1-bit full adder (a, b, cin -> sum, cout)");
+    println!(
+        "  {} variables: {:?}",
+        circuit_sat.num_variables(),
+        circuit_sat.variable_names()
+    );
+
+    // 2. Reduce to ILP
+    let reduction = ReduceTo::<ILP>::reduce_to(&circuit_sat);
+    let ilp = reduction.target_problem();
+
+    println!("\n=== Problem Transformation ===");
+    println!(
+        "Source: CircuitSAT with {} variables",
+        circuit_sat.num_variables()
+    );
+    println!(
+        "Target: ILP with {} variables, {} constraints",
+        ilp.num_variables(),
+        ilp.constraints.len()
+    );
+    println!("  Each logic gate becomes a set of linear constraints.");
+    println!("  XOR gates use 4 constraints each; AND/OR use k+1 constraints.");
+    println!("  Objective is trivial (minimize 0): feasibility = satisfying assignment.");
+
+    // 3. Solve the target ILP problem
+    let solver = BruteForce::new();
+    let ilp_solutions = solver.find_all_best(ilp);
+    println!("\n=== Solution ===");
+    println!(
+        "Target ILP feasible solutions found: {}",
+        ilp_solutions.len()
+    );
+
+    // 4. Extract and verify source solutions
+    println!("\nAll extracted CircuitSAT solutions:");
+    let mut valid_count = 0;
+    let mut solutions = Vec::new();
+    for ilp_sol in &ilp_solutions {
+        let circuit_sol = reduction.extract_solution(ilp_sol);
+        let valid = circuit_sat.evaluate(&circuit_sol);
+        let var_names = circuit_sat.variable_names();
+        let assignment_str: Vec<String> = var_names
+            .iter()
+            .zip(circuit_sol.iter())
+            .map(|(name, &val)| format!("{}={}", name, val))
+            .collect();
+        println!(
+            "  ILP config {:?} -> Circuit: [{}], valid: {}",
+            ilp_sol,
+            assignment_str.join(", "),
+            valid
+        );
+        if valid {
+            valid_count += 1;
+            solutions.push(SolutionPair {
+                source_config: circuit_sol,
+                target_config: ilp_sol.clone(),
+            });
+        }
+    }
+    println!(
+        "\n{}/{} ILP solutions map to valid circuit assignments",
+        valid_count,
+        ilp_solutions.len()
+    );
+    assert!(
+        valid_count > 0,
+        "At least one ILP solution must be a valid circuit assignment"
+    );
+
+    println!("\nReduction verified successfully");
+
+    // 5. Export JSON
+    let source_variant = variant_to_map(CircuitSAT::variant());
+    let target_variant = variant_to_map(ILP::variant());
+    let overhead = lookup_overhead("CircuitSAT", &source_variant, "ILP", &target_variant)
+        .expect("CircuitSAT -> ILP overhead not found");
+
+    let data = ReductionData {
+        source: ProblemSide {
+            problem: CircuitSAT::NAME.to_string(),
+            variant: source_variant,
+            instance: serde_json::json!({
+                "num_gates": circuit_sat.circuit().num_assignments(),
+                "num_variables": circuit_sat.num_variables(),
+            }),
+        },
+        target: ProblemSide {
+            problem: ILP::NAME.to_string(),
+            variant: target_variant,
+            instance: serde_json::json!({
+                "num_vars": ilp.num_variables(),
+            }),
+        },
+        overhead: overhead_to_json(&overhead),
+    };
+
+    let results = ResultData { solutions };
+    let name = "circuitsat_to_ilp";
+    write_example(name, &data, &results);
+}
+
+fn main() {
+    run()
+}

examples/reduction_qubo_to_ilp.rs

@@ -0,0 +1,121 @@
+// # QUBO to ILP Reduction (McCormick Linearization)
+//
+// ## Mathematical Relationship
+// A QUBO problem:
+//
+//   minimize x^T Q x,   x ∈ {0,1}^n
+//
+// is linearized by replacing each product x_i·x_j (i < j) with an
+// auxiliary binary variable y_ij and three McCormick constraints:
+//   y_ij ≤ x_i,  y_ij ≤ x_j,  y_ij ≥ x_i + x_j - 1
+//
+// Diagonal terms Q_ii·x_i² = Q_ii·x_i are directly linear.
+//
+// ## This Example
+// - Instance: 4-variable QUBO with a few quadratic terms
+//   Q = diag(-2, -3, -1, -4) with Q_{01}=1, Q_{12}=2, Q_{23}=-1
+// - Expected: optimal binary assignment minimizing x^T Q x
+//
+// ## Outputs
+// - `docs/paper/examples/qubo_to_ilp.json` — reduction structure
+// - `docs/paper/examples/qubo_to_ilp.result.json` — solutions
+//
+// ## Usage
+// ```bash
+// cargo run --example reduction_qubo_to_ilp --features ilp-solver
+// ```
+
+use problemreductions::export::*;
+use problemreductions::models::optimization::ILP;
+use problemreductions::prelude::*;
+
+pub fn run() {
+    println!("=== QUBO -> ILP Reduction (McCormick) ===\n");
+
+    // 4-variable QUBO: diagonal (linear) + off-diagonal (quadratic) terms
+    let mut matrix = vec![vec![0.0; 4]; 4];
+    matrix[0][0] = -2.0;
+    matrix[1][1] = -3.0;
+    matrix[2][2] = -1.0;
+    matrix[3][3] = -4.0;
+    matrix[0][1] = 1.0; // x0·x1 coupling
+    matrix[1][2] = 2.0; // x1·x2 coupling
+    matrix[2][3] = -1.0; // x2·x3 coupling
+    let qubo = QUBO::from_matrix(matrix);
+
+    // Reduce to ILP
+    let reduction = ReduceTo::<ILP>::reduce_to(&qubo);
+    let ilp = reduction.target_problem();
+
+    println!("Source: QUBO with {} variables", qubo.num_variables());
+    println!("  Q diagonal: [-2, -3, -1, -4]");
+    println!("  Q off-diagonal: (0,1)=1, (1,2)=2, (2,3)=-1");
+    println!(
+        "Target: ILP with {} variables ({} original + {} auxiliary)",
+        ilp.num_variables(),
+        qubo.num_variables(),
+        ilp.num_variables() - qubo.num_variables()
+    );
+    println!(
+        "  {} constraints (3 McCormick per auxiliary variable)",
+        ilp.constraints.len()
+    );
+
+    // Solve ILP with brute force
+    let solver = BruteForce::new();
+    let ilp_solutions = solver.find_all_best(ilp);
+
+    println!("\nOptimal solutions:");
+    let mut solutions = Vec::new();
+    for sol in &ilp_solutions {
+        let extracted = reduction.extract_solution(sol);
+        let qubo_val = qubo.evaluate(&extracted);
+        println!("  x = {:?}, QUBO value = {}", extracted, qubo_val);
+
+        // Closed-loop verification
+        assert!(
+            qubo_val < f64::MAX,
+            "Solution must be valid in source problem"
+        );
+
+        solutions.push(SolutionPair {
+            source_config: extracted,
+            target_config: sol.clone(),
+        });
+    }
+
+    println!("\nVerification passed: all solutions are feasible and optimal");
+
+    // Export JSON
+    let source_variant = variant_to_map(QUBO::<f64>::variant());
+    let target_variant = variant_to_map(ILP::variant());
+    let overhead = lookup_overhead("QUBO", &source_variant, "ILP", &target_variant)
+        .expect("QUBO -> ILP overhead not found");
+
+    let data = ReductionData {
+        source: ProblemSide {
+            problem: QUBO::<f64>::NAME.to_string(),
+            variant: source_variant,
+            instance: serde_json::json!({
+                "num_vars": qubo.num_vars(),
+                "matrix": qubo.matrix(),
+            }),
+        },
+        target: ProblemSide {
+            problem: ILP::NAME.to_string(),
+            variant: target_variant,
+            instance: serde_json::json!({
+                "num_vars": ilp.num_variables(),
+            }),
+        },
+        overhead: overhead_to_json(&overhead),
+    };
+
+    let results = ResultData { solutions };
+    let name = "qubo_to_ilp";
+    write_example(name, &data, &results);
+}
+
+fn main() {
+    run()
+}