From 79ce3e14d7d7334c4316be7a4b3dfc01622f8087 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 18 Feb 2026 22:06:57 +0800 Subject: [PATCH 1/4] =?UTF-8?q?docs:=20add=20design=20and=20plan=20for=20Q?= =?UTF-8?q?UBO=E2=86=92ILP=20and=20CircuitSAT=E2=86=92ILP=20reductions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses issue #83 — adds ILP reduction paths for QUBO, SpinGlass, MaxCut, and CircuitSAT. Co-Authored-By: Claude Opus 4.6 --- .../2026-02-18-ilp-reduction-paths-design.md | 78 ++ .../2026-02-18-ilp-reduction-paths-impl.md | 726 ++++++++++++++++++ 2 files changed, 804 insertions(+) create mode 100644 docs/plans/2026-02-18-ilp-reduction-paths-design.md create mode 100644 docs/plans/2026-02-18-ilp-reduction-paths-impl.md diff --git a/docs/plans/2026-02-18-ilp-reduction-paths-design.md b/docs/plans/2026-02-18-ilp-reduction-paths-design.md new file mode 100644 index 000000000..8f6d504c6 --- /dev/null +++ b/docs/plans/2026-02-18-ilp-reduction-paths-design.md @@ -0,0 +1,78 @@ +# ILP Reduction Paths for QUBO and CircuitSAT + +**Issue:** #83 — Add ILP reduction paths for CircuitSAT, MaxCut, QUBO, SpinGlass +**Date:** 2026-02-18 + +## Problem + +Four problem types have no reduction path to ILP, causing `pred solve` to fail with the default ILP solver: QUBO, SpinGlass, MaxCut, CircuitSAT. + +## Solution + +Two new reductions: + +1. **QUBO → ILP** — Covers QUBO, SpinGlass (via SpinGlass→QUBO→ILP), and MaxCut (via MaxCut→SpinGlass→QUBO→ILP) +2. **CircuitSAT → ILP** — Direct 1-step path (more efficient than the 3-step CircuitSAT→SpinGlass→QUBO→ILP chain) + +## Reduction 1: QUBO → ILP (McCormick Linearization) + +QUBO minimizes `x^T Q x` where `x ∈ {0,1}^n` and Q is upper-triangular. + +**Linearization:** For each non-zero off-diagonal `Q_ij` (i < j), introduce binary auxiliary `y_ij = x_i · x_j`: +- `y_ij ≤ x_i` +- `y_ij ≤ x_j` +- `y_ij ≥ x_i + x_j - 1` + +Diagonal terms are already linear: `Q_ii · x_i² = Q_ii · x_i` for binary x. + +**ILP:** +- Variables: `n` original + `m` auxiliary (m = non-zero off-diagonal count) +- All binary bounds +- Objective: `minimize Σ_i Q_ii · x_i + Σ_{i **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Add QUBO→ILP and CircuitSAT→ILP reductions so all problem types can reach ILP (fixes #83). + +**Architecture:** Two independent reductions following existing patterns: McCormick linearization for QUBO→ILP, Tseitin-style gate encoding for CircuitSAT→ILP. Both are feature-gated behind `ilp-solver`. + +**Tech Stack:** Rust, `#[reduction]` macro, `inventory` crate for registration, `ILP` model types from `src/models/optimization/ilp.rs`. + +--- + +## Task 1: QUBO → ILP Reduction + +**Files:** +- Create: `src/rules/qubo_ilp.rs` +- Modify: `src/rules/mod.rs` (add module declaration) +- Test: `src/unit_tests/rules/qubo_ilp.rs` + +**Reference:** `src/rules/maximumindependentset_ilp.rs` for ILP reduction pattern, `src/rules/factoring_ilp.rs` for McCormick pattern. + +### Step 1: Write the failing test + +Create `src/unit_tests/rules/qubo_ilp.rs`: + +```rust +use super::*; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use std::collections::HashSet; + +#[test] +fn test_qubo_to_ilp_closed_loop() { + // QUBO: minimize 2*x0 - 3*x1 + x0*x1 + // Q = [[2, 1], [0, -3]] + // x=0,0 -> 0, x=1,0 -> 2, x=0,1 -> -3, x=1,1 -> 0 + // Optimal: x = [0, 1] with obj = -3 + let qubo = QUBO::from_matrix(vec![vec![2.0, 1.0], vec![0.0, -3.0]]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_best(&qubo).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_qubo_to_ilp_diagonal_only() { + // No quadratic terms: minimize 3*x0 - 2*x1 + // Optimal: x = [0, 1] with obj = -2 + let qubo = QUBO::from_matrix(vec![vec![3.0, 0.0], vec![0.0, -2.0]]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + // No auxiliary variables when no off-diagonal terms + assert_eq!(ilp.num_variables(), 2); + assert!(ilp.constraints.is_empty()); + + let solver = BruteForce::new(); + let best = solver.find_all_best(ilp); + let extracted = reduction.extract_solution(&best[0]); + assert_eq!(extracted, vec![0, 1]); +} + +#[test] +fn test_qubo_to_ilp_3var() { + // QUBO: minimize -x0 - x1 - x2 + 4*x0*x1 + 4*x1*x2 + // Penalty on adjacent pairs → optimal is [1, 0, 1] + let qubo = QUBO::from_matrix(vec![ + vec![-1.0, 4.0, 0.0], + vec![0.0, -1.0, 4.0], + vec![0.0, 0.0, -1.0], + ]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + // 3 original + 2 auxiliary (for two off-diagonal terms) + assert_eq!(ilp.num_variables(), 5); + // 3 constraints per auxiliary = 6 + assert_eq!(ilp.constraints.len(), 6); + + let solver = BruteForce::new(); + let best = solver.find_all_best(ilp); + let extracted = reduction.extract_solution(&best[0]); + assert_eq!(extracted, vec![1, 0, 1]); +} +``` + +### Step 2: Run test to verify it fails + +Run: `cargo test --features ilp-solver test_qubo_to_ilp -- --nocapture 2>&1 | head -30` +Expected: Compilation error (module doesn't exist yet) + +### Step 3: Write the reduction implementation + +Create `src/rules/qubo_ilp.rs`: + +```rust +//! Reduction from QUBO to ILP via McCormick linearization. +//! +//! QUBO minimizes x^T Q x where x ∈ {0,1}^n and Q is upper-triangular. +//! +//! ## Linearization +//! - Diagonal: Q_ii · x_i² = Q_ii · x_i (linear for binary x) +//! - Off-diagonal: For each non-zero Q_ij (i < j), introduce y_ij = x_i · x_j +//! with McCormick constraints: y_ij ≤ x_i, y_ij ≤ x_j, y_ij ≥ x_i + x_j - 1 +//! +//! ## Variables +//! - x_i ∈ {0,1} for i = 0..n-1 (original QUBO variables) +//! - y_k ∈ {0,1} for each non-zero off-diagonal Q_ij (auxiliary products) +//! +//! ## Objective +//! minimize Σ_i Q_ii · x_i + Σ_{i; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.num_original].to_vec() + } +} + +#[reduction( + overhead = { + ReductionOverhead::new(vec![ + ("num_vars", poly!(num_vars ^ 2)), + ("num_constraints", poly!(num_vars ^ 2)), + ]) + } +)] +impl ReduceTo for QUBO { + type Result = ReductionQUBOToILP; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vars(); + let matrix = self.matrix(); + + // Collect non-zero off-diagonal entries (i < j) + let mut off_diag: Vec<(usize, usize, f64)> = Vec::new(); + for i in 0..n { + for j in (i + 1)..n { + let q_ij = matrix[i][j]; + if q_ij != 0.0 { + off_diag.push((i, j, q_ij)); + } + } + } + + let m = off_diag.len(); + let total_vars = n + m; + + // All variables are binary + let bounds = vec![VarBounds::binary(); total_vars]; + + // Objective: minimize Σ Q_ii · x_i + Σ Q_ij · y_k + let mut objective: Vec<(usize, f64)> = Vec::new(); + for i in 0..n { + let q_ii = matrix[i][i]; + if q_ii != 0.0 { + objective.push((i, q_ii)); + } + } + for (k, &(_, _, q_ij)) in off_diag.iter().enumerate() { + objective.push((n + k, q_ij)); + } + + // McCormick constraints: 3 per auxiliary variable + let mut constraints = Vec::with_capacity(3 * m); + for (k, &(i, j, _)) in off_diag.iter().enumerate() { + let y_k = n + k; + // y_k ≤ x_i + constraints.push(LinearConstraint::le( + vec![(y_k, 1.0), (i, -1.0)], + 0.0, + )); + // y_k ≤ x_j + constraints.push(LinearConstraint::le( + vec![(y_k, 1.0), (j, -1.0)], + 0.0, + )); + // y_k ≥ x_i + x_j - 1 + constraints.push(LinearConstraint::ge( + vec![(y_k, 1.0), (i, -1.0), (j, -1.0)], + -1.0, + )); + } + + let target = ILP::new(total_vars, bounds, constraints, objective, ObjectiveSense::Minimize); + ReductionQUBOToILP { + target, + num_original: n, + } + } +} + +#[cfg(test)] +#[path = "../unit_tests/rules/qubo_ilp.rs"] +mod tests; +``` + +### Step 4: Register module in `src/rules/mod.rs` + +Add after the existing `ilp_qubo` line: + +```rust +#[cfg(feature = "ilp-solver")] +mod qubo_ilp; +``` + +### Step 5: Run tests to verify they pass + +Run: `cargo test --features ilp-solver test_qubo_to_ilp -- --nocapture` +Expected: All 3 tests pass + +### Step 6: Commit + +```bash +git add src/rules/qubo_ilp.rs src/rules/mod.rs src/unit_tests/rules/qubo_ilp.rs +git commit -m "feat: add QUBO → ILP reduction via McCormick linearization + +Closes the ILP path for QUBO, SpinGlass, and MaxCut (issue #83)." +``` + +--- + +## Task 2: CircuitSAT → ILP Reduction + +**Files:** +- Create: `src/rules/circuit_ilp.rs` +- Modify: `src/rules/mod.rs` (add module declaration) +- Test: `src/unit_tests/rules/circuit_ilp.rs` + +**Reference:** `src/rules/circuit_spinglass.rs` for expression tree walking, `src/rules/maximumindependentset_ilp.rs` for ILP reduction structure. + +### Step 1: Write the failing test + +Create `src/unit_tests/rules/circuit_ilp.rs`: + +```rust +use super::*; +use crate::models::specialized::{Assignment, BooleanExpr, Circuit, CircuitSAT}; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use std::collections::HashSet; + +#[test] +fn test_circuitsat_to_ilp_and_gate() { + // c = x AND y, constrain c = true → only x=1, y=1 satisfies + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); + assert!(!extracted.is_empty()); +} + +#[test] +fn test_circuitsat_to_ilp_or_gate() { + // c = x OR y, constrain c = true → x=1,y=0 or x=0,y=1 or x=1,y=1 + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::or(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_circuitsat_to_ilp_xor_gate() { + // c = x XOR y, constrain c = true → x=1,y=0 or x=0,y=1 + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); + assert_eq!(extracted.len(), 2); // exactly x=1,y=0 and x=0,y=1 +} + +#[test] +fn test_circuitsat_to_ilp_nested() { + // d = (x AND y) OR z, constrain d = true + let circuit = Circuit::new(vec![Assignment::new( + vec!["d".to_string()], + BooleanExpr::or(vec![ + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + BooleanExpr::var("z"), + ]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_circuitsat_to_ilp_closed_loop() { + // Multi-assignment circuit: a = x AND y, b = NOT a, constrain b = false + // Satisfying: x=1, y=1 → a=true → b=false ✓ + // x=0, y=0 → a=false → b=true ✗ (b must be false) + // etc. + let circuit = Circuit::new(vec![ + Assignment::new( + vec!["a".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + ), + Assignment::new( + vec!["b".to_string()], + BooleanExpr::not(BooleanExpr::var("a")), + ), + ]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} +``` + +### Step 2: Run test to verify it fails + +Run: `cargo test --features ilp-solver test_circuitsat_to_ilp -- --nocapture 2>&1 | head -30` +Expected: Compilation error + +### Step 3: Write the reduction implementation + +Create `src/rules/circuit_ilp.rs`: + +```rust +//! Reduction from CircuitSAT to ILP via gate constraint encoding. +//! +//! Each boolean gate is encoded as linear constraints over binary variables. +//! The expression tree is flattened by introducing an auxiliary variable per +//! internal node (Tseitin-style). +//! +//! ## Gate Encodings (all variables binary) +//! - NOT(a) = c: c + a = 1 +//! - AND(a₁,...,aₖ) = c: c ≤ aᵢ (∀i), c ≥ Σaᵢ - (k-1) +//! - OR(a₁,...,aₖ) = c: c ≥ aᵢ (∀i), c ≤ Σaᵢ +//! - XOR(a, b) = c: c ≤ a+b, c ≥ a-b, c ≥ b-a, c ≤ 2-a-b +//! - Const(v) = c: c = v +//! +//! ## Objective +//! Trivial (minimize 0): any feasible ILP solution is a satisfying assignment. + +use crate::models::optimization::{LinearConstraint, ObjectiveSense, VarBounds, ILP}; +use crate::models::specialized::{BooleanExpr, BooleanOp, CircuitSAT}; +use crate::poly; +use crate::reduction; +use crate::rules::registry::ReductionOverhead; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use std::collections::HashMap; + +/// Result of reducing CircuitSAT to ILP. +#[derive(Debug, Clone)] +pub struct ReductionCircuitToILP { + target: ILP, + source_variables: Vec, + variable_map: HashMap, +} + +impl ReductionResult for ReductionCircuitToILP { + type Source = CircuitSAT; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + self.source_variables + .iter() + .map(|name| target_solution[self.variable_map[name]]) + .collect() + } +} + +/// Builder that accumulates ILP variables and constraints. +struct ILPBuilder { + num_vars: usize, + constraints: Vec, + variable_map: HashMap, +} + +impl ILPBuilder { + fn new() -> Self { + Self { + num_vars: 0, + constraints: Vec::new(), + variable_map: HashMap::new(), + } + } + + /// Get or create a variable index for a named circuit variable. + fn get_or_create_var(&mut self, name: &str) -> usize { + if let Some(&idx) = self.variable_map.get(name) { + idx + } else { + let idx = self.num_vars; + self.variable_map.insert(name.to_string(), idx); + self.num_vars += 1; + idx + } + } + + /// Allocate an anonymous auxiliary variable. + fn alloc_aux(&mut self) -> usize { + let idx = self.num_vars; + self.num_vars += 1; + idx + } + + /// Recursively process a BooleanExpr, returning the ILP variable index + /// that holds the expression's value. + fn process_expr(&mut self, expr: &BooleanExpr) -> usize { + match &expr.op { + BooleanOp::Var(name) => self.get_or_create_var(name), + BooleanOp::Const(value) => { + let c = self.alloc_aux(); + let v = if *value { 1.0 } else { 0.0 }; + self.constraints.push(LinearConstraint::eq(vec![(c, 1.0)], v)); + c + } + BooleanOp::Not(inner) => { + let a = self.process_expr(inner); + let c = self.alloc_aux(); + // c + a = 1 + self.constraints + .push(LinearConstraint::eq(vec![(c, 1.0), (a, 1.0)], 1.0)); + c + } + BooleanOp::And(args) => { + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + let c = self.alloc_aux(); + let k = inputs.len() as f64; + // c ≤ a_i for all i + for &a_i in &inputs { + self.constraints + .push(LinearConstraint::le(vec![(c, 1.0), (a_i, -1.0)], 0.0)); + } + // c ≥ Σa_i - (k - 1) + let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; + for &a_i in &inputs { + terms.push((a_i, -1.0)); + } + self.constraints + .push(LinearConstraint::ge(terms, -(k - 1.0))); + c + } + BooleanOp::Or(args) => { + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + let c = self.alloc_aux(); + // c ≥ a_i for all i + for &a_i in &inputs { + self.constraints + .push(LinearConstraint::ge(vec![(c, 1.0), (a_i, -1.0)], 0.0)); + } + // c ≤ Σa_i + let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; + for &a_i in &inputs { + terms.push((a_i, -1.0)); + } + self.constraints.push(LinearConstraint::le(terms, 0.0)); + c + } + BooleanOp::Xor(args) => { + // Chain pairwise: XOR(a1, a2, a3) = XOR(XOR(a1, a2), a3) + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + assert!(!inputs.is_empty()); + let mut result = inputs[0]; + for &next in &inputs[1..] { + let c = self.alloc_aux(); + let a = result; + let b = next; + // c ≤ a + b + self.constraints.push(LinearConstraint::le( + vec![(c, 1.0), (a, -1.0), (b, -1.0)], + 0.0, + )); + // c ≥ a - b + self.constraints.push(LinearConstraint::ge( + vec![(c, 1.0), (a, -1.0), (b, 1.0)], + 0.0, + )); + // c ≥ b - a + self.constraints.push(LinearConstraint::ge( + vec![(c, 1.0), (a, 1.0), (b, -1.0)], + 0.0, + )); + // c ≤ 2 - a - b + self.constraints.push(LinearConstraint::le( + vec![(c, 1.0), (a, 1.0), (b, 1.0)], + 2.0, + )); + result = c; + } + result + } + } + } +} + +#[reduction( + overhead = { + ReductionOverhead::new(vec![ + ("num_vars", poly!(num_variables + num_assignments)), + ("num_constraints", poly!(num_variables + num_assignments)), + ]) + } +)] +impl ReduceTo for CircuitSAT { + type Result = ReductionCircuitToILP; + + fn reduce_to(&self) -> Self::Result { + let mut builder = ILPBuilder::new(); + + // Pre-register all circuit variables to preserve ordering + for name in self.variable_names() { + builder.get_or_create_var(name); + } + + // Process each assignment + for assignment in &self.circuit().assignments { + let expr_var = builder.process_expr(&assignment.expr); + // Constrain each output to equal the expression result + for output_name in &assignment.outputs { + let out_var = builder.get_or_create_var(output_name); + if out_var != expr_var { + // out = expr_var + builder.constraints.push(LinearConstraint::eq( + vec![(out_var, 1.0), (expr_var, -1.0)], + 0.0, + )); + } + } + } + + let bounds = vec![VarBounds::binary(); builder.num_vars]; + // Trivial objective: minimize 0 (satisfaction problem) + let objective = vec![]; + let target = ILP::new( + builder.num_vars, + bounds, + builder.constraints, + objective, + ObjectiveSense::Minimize, + ); + + ReductionCircuitToILP { + target, + source_variables: self.variable_names().to_vec(), + variable_map: builder.variable_map, + } + } +} + +#[cfg(test)] +#[path = "../unit_tests/rules/circuit_ilp.rs"] +mod tests; +``` + +### Step 4: Register module in `src/rules/mod.rs` + +Add after the `coloring_ilp` line in the `#[cfg(feature = "ilp-solver")]` block: + +```rust +#[cfg(feature = "ilp-solver")] +mod circuit_ilp; +``` + +### Step 5: Run tests to verify they pass + +Run: `cargo test --features ilp-solver test_circuitsat_to_ilp -- --nocapture` +Expected: All 5 tests pass + +### Step 6: Commit + +```bash +git add src/rules/circuit_ilp.rs src/rules/mod.rs src/unit_tests/rules/circuit_ilp.rs +git commit -m "feat: add CircuitSAT → ILP reduction via gate constraint encoding + +Direct 1-step path, more efficient than CircuitSAT→SpinGlass→QUBO→ILP (issue #83)." +``` + +--- + +## Task 3: Integration Verification + +### Step 1: Run full test suite + +Run: `make test clippy` +Expected: All tests pass, no clippy warnings + +### Step 2: Verify reduction graph has new paths + +Run: `cargo test --features ilp-solver test_reduction_graph -- --nocapture 2>&1 | grep -i "qubo\|circuit"` or check the graph test file at `src/unit_tests/rules/graph.rs` for existing assertions and add new ones if needed. + +### Step 3: Test CLI integration (if on the cli-tool-design branch) + +Run: +```bash +echo '{"problem":"QUBO","instance":{"matrix":[[2.0,1.0],[0.0,-3.0]]}}' > /tmp/qubo_test.json +cargo run --features ilp-solver -- solve /tmp/qubo_test.json +``` +Expected: Solution found (not "No reduction path" error) + +### Step 4: Commit any fixes + +--- + +## Task 4: Examples and Documentation (Optional — can be a follow-up PR) + +**Files:** +- Create: `examples/reduction_qubo_to_ilp.rs` +- Create: `examples/reduction_circuitsat_to_ilp.rs` +- Modify: `tests/suites/examples.rs` (register new examples) +- Modify: `docs/paper/reductions.typ` (add reduction-rule entries) + +### Step 1: Create QUBO → ILP example + +Follow pattern from `examples/reduction_ilp_to_qubo.rs`: +- Create a small QUBO instance (e.g., 3-variable) +- Reduce to ILP, print transformation details +- Solve with BruteForce, extract and verify +- Export JSON to `docs/paper/examples/` + +### Step 2: Create CircuitSAT → ILP example + +Follow pattern from `examples/reduction_circuitsat_to_spinglass.rs`: +- Create a small circuit (e.g., AND + NOT) +- Reduce to ILP, print transformation details +- Solve, extract and verify +- Export JSON + +### Step 3: Register examples in test suite + +Add to `tests/suites/examples.rs`: +```rust +example_test!(reduction_qubo_to_ilp); +example_test!(reduction_circuitsat_to_ilp); +example_fn!(test_qubo_to_ilp, reduction_qubo_to_ilp); +example_fn!(test_circuitsat_to_ilp, reduction_circuitsat_to_ilp); +``` + +### Step 4: Add paper entries + +In `docs/paper/reductions.typ`, add `reduction-rule` entries for both new reductions. + +### Step 5: Commit + +```bash +git add examples/ tests/suites/examples.rs docs/ +git commit -m "docs: add examples and paper entries for QUBO→ILP and CircuitSAT→ILP" +``` From 014886e172b74d356ae55e5ac3127dba6b18ed00 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 18 Feb 2026 22:18:23 +0800 Subject: [PATCH 2/4] =?UTF-8?q?feat:=20add=20QUBO=20=E2=86=92=20ILP=20redu?= =?UTF-8?q?ction=20via=20McCormick=20linearization?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implement reduction from QUBO to ILP using McCormick linearization for binary quadratic terms. Diagonal Q_ii terms become linear x_i terms, and each non-zero off-diagonal Q_ij (i --- src/rules/mod.rs | 2 + src/rules/qubo_ilp.rs | 117 +++++++++++++++++++++++++++++++ src/unit_tests/rules/qubo_ilp.rs | 65 +++++++++++++++++ 3 files changed, 184 insertions(+) create mode 100644 src/rules/qubo_ilp.rs create mode 100644 src/unit_tests/rules/qubo_ilp.rs diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 678cd0a46..9cff61490 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -56,6 +56,8 @@ mod minimumsetcovering_ilp; #[cfg(feature = "ilp-solver")] mod minimumvertexcover_ilp; #[cfg(feature = "ilp-solver")] +mod qubo_ilp; +#[cfg(feature = "ilp-solver")] mod travelingsalesman_ilp; pub use graph::{ diff --git a/src/rules/qubo_ilp.rs b/src/rules/qubo_ilp.rs new file mode 100644 index 000000000..9f7c3100a --- /dev/null +++ b/src/rules/qubo_ilp.rs @@ -0,0 +1,117 @@ +//! Reduction from QUBO to ILP via McCormick linearization. +//! +//! QUBO minimizes x^T Q x where x ∈ {0,1}^n and Q is upper-triangular. +//! +//! ## Linearization +//! - Diagonal: Q_ii · x_i² = Q_ii · x_i (linear for binary x) +//! - Off-diagonal: For each non-zero Q_ij (i < j), introduce y_ij = x_i · x_j +//! with McCormick constraints: y_ij ≤ x_i, y_ij ≤ x_j, y_ij ≥ x_i + x_j - 1 +//! +//! ## Variables +//! - x_i ∈ {0,1} for i = 0..n-1 (original QUBO variables) +//! - y_k ∈ {0,1} for each non-zero off-diagonal Q_ij (auxiliary products) +//! +//! ## Objective +//! minimize Σ_i Q_ii · x_i + Σ_{i; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.num_original].to_vec() + } +} + +#[reduction( + overhead = { + ReductionOverhead::new(vec![ + ("num_vars", poly!(num_vars ^ 2)), + ("num_constraints", poly!(num_vars ^ 2)), + ]) + } +)] +impl ReduceTo for QUBO { + type Result = ReductionQUBOToILP; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vars(); + let matrix = self.matrix(); + + // Collect non-zero off-diagonal entries (i < j) + let mut off_diag: Vec<(usize, usize, f64)> = Vec::new(); + for (i, row) in matrix.iter().enumerate() { + for (j, &q_ij) in row.iter().enumerate().skip(i + 1) { + if q_ij != 0.0 { + off_diag.push((i, j, q_ij)); + } + } + } + + let m = off_diag.len(); + let total_vars = n + m; + + // All variables are binary + let bounds = vec![VarBounds::binary(); total_vars]; + + // Objective: minimize Σ Q_ii · x_i + Σ Q_ij · y_k + let mut objective: Vec<(usize, f64)> = Vec::new(); + for (i, row) in matrix.iter().enumerate() { + let q_ii = row[i]; + if q_ii != 0.0 { + objective.push((i, q_ii)); + } + } + for (k, &(_, _, q_ij)) in off_diag.iter().enumerate() { + objective.push((n + k, q_ij)); + } + + // McCormick constraints: 3 per auxiliary variable + let mut constraints = Vec::with_capacity(3 * m); + for (k, &(i, j, _)) in off_diag.iter().enumerate() { + let y_k = n + k; + // y_k ≤ x_i + constraints.push(LinearConstraint::le( + vec![(y_k, 1.0), (i, -1.0)], + 0.0, + )); + // y_k ≤ x_j + constraints.push(LinearConstraint::le( + vec![(y_k, 1.0), (j, -1.0)], + 0.0, + )); + // y_k ≥ x_i + x_j - 1 + constraints.push(LinearConstraint::ge( + vec![(y_k, 1.0), (i, -1.0), (j, -1.0)], + -1.0, + )); + } + + let target = ILP::new(total_vars, bounds, constraints, objective, ObjectiveSense::Minimize); + ReductionQUBOToILP { + target, + num_original: n, + } + } +} + +#[cfg(test)] +#[path = "../unit_tests/rules/qubo_ilp.rs"] +mod tests; diff --git a/src/unit_tests/rules/qubo_ilp.rs b/src/unit_tests/rules/qubo_ilp.rs new file mode 100644 index 000000000..cea0abe83 --- /dev/null +++ b/src/unit_tests/rules/qubo_ilp.rs @@ -0,0 +1,65 @@ +use super::*; +use crate::solvers::BruteForce; +use std::collections::HashSet; + +#[test] +fn test_qubo_to_ilp_closed_loop() { + // QUBO: minimize 2*x0 - 3*x1 + x0*x1 + // Q = [[2, 1], [0, -3]] + // x=0,0 -> 0, x=1,0 -> 2, x=0,1 -> -3, x=1,1 -> 0 + // Optimal: x = [0, 1] with obj = -3 + let qubo = QUBO::from_matrix(vec![vec![2.0, 1.0], vec![0.0, -3.0]]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_best(&qubo).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_qubo_to_ilp_diagonal_only() { + // No quadratic terms: minimize 3*x0 - 2*x1 + // Optimal: x = [0, 1] with obj = -2 + let qubo = QUBO::from_matrix(vec![vec![3.0, 0.0], vec![0.0, -2.0]]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + // No auxiliary variables when no off-diagonal terms + assert_eq!(ilp.num_variables(), 2); + assert!(ilp.constraints.is_empty()); + + let solver = BruteForce::new(); + let best = solver.find_all_best(ilp); + let extracted = reduction.extract_solution(&best[0]); + assert_eq!(extracted, vec![0, 1]); +} + +#[test] +fn test_qubo_to_ilp_3var() { + // QUBO: minimize -x0 - x1 - x2 + 4*x0*x1 + 4*x1*x2 + // Penalty on adjacent pairs → optimal is [1, 0, 1] + let qubo = QUBO::from_matrix(vec![ + vec![-1.0, 4.0, 0.0], + vec![0.0, -1.0, 4.0], + vec![0.0, 0.0, -1.0], + ]); + let reduction = ReduceTo::::reduce_to(&qubo); + let ilp = reduction.target_problem(); + + // 3 original + 2 auxiliary (for two off-diagonal terms) + assert_eq!(ilp.num_variables(), 5); + // 3 constraints per auxiliary = 6 + assert_eq!(ilp.constraints.len(), 6); + + let solver = BruteForce::new(); + let best = solver.find_all_best(ilp); + let extracted = reduction.extract_solution(&best[0]); + assert_eq!(extracted, vec![1, 0, 1]); +} From 01c9f6ce045ff3c9da4881d58374bbb6530b36b5 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Wed, 18 Feb 2026 22:33:25 +0800 Subject: [PATCH 3/4] =?UTF-8?q?feat:=20add=20CircuitSAT=20=E2=86=92=20ILP?= =?UTF-8?q?=20reduction=20via=20gate=20constraint=20encoding?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Direct 1-step path, more efficient than CircuitSAT→SpinGlass→QUBO→ILP (issue #83). Fix XOR test: CircuitSAT `c = x XOR y` constrains c == (x XOR y) for all variable assignments (4 solutions), not just c=true (2 solutions). --- src/rules/circuit_ilp.rs | 231 ++++++++++++++++++++++ src/rules/mod.rs | 2 + src/unit_tests/rules/circuit_ilp.rs | 125 ++++++++++++ src/unit_tests/rules/circuit_spinglass.rs | 12 +- 4 files changed, 364 insertions(+), 6 deletions(-) create mode 100644 src/rules/circuit_ilp.rs create mode 100644 src/unit_tests/rules/circuit_ilp.rs diff --git a/src/rules/circuit_ilp.rs b/src/rules/circuit_ilp.rs new file mode 100644 index 000000000..04e89f255 --- /dev/null +++ b/src/rules/circuit_ilp.rs @@ -0,0 +1,231 @@ +//! Reduction from CircuitSAT to ILP via gate constraint encoding. +//! +//! Each boolean gate is encoded as linear constraints over binary variables. +//! The expression tree is flattened by introducing an auxiliary variable per +//! internal node (Tseitin-style). +//! +//! ## Gate Encodings (all variables binary) +//! - NOT(a) = c: c + a = 1 +//! - AND(a₁,...,aₖ) = c: c ≤ aᵢ (∀i), c ≥ Σaᵢ - (k-1) +//! - OR(a₁,...,aₖ) = c: c ≥ aᵢ (∀i), c ≤ Σaᵢ +//! - XOR(a, b) = c: c ≤ a+b, c ≥ a-b, c ≥ b-a, c ≤ 2-a-b +//! - Const(v) = c: c = v +//! +//! ## Objective +//! Trivial (minimize 0): any feasible ILP solution is a satisfying assignment. + +use crate::models::optimization::{LinearConstraint, ObjectiveSense, VarBounds, ILP}; +use crate::models::specialized::{BooleanExpr, BooleanOp, CircuitSAT}; +use crate::poly; +use crate::reduction; +use crate::rules::registry::ReductionOverhead; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use std::collections::HashMap; + +/// Result of reducing CircuitSAT to ILP. +#[derive(Debug, Clone)] +pub struct ReductionCircuitToILP { + target: ILP, + source_variables: Vec, + variable_map: HashMap, +} + +impl ReductionResult for ReductionCircuitToILP { + type Source = CircuitSAT; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + self.source_variables + .iter() + .map(|name| target_solution[self.variable_map[name]]) + .collect() + } +} + +/// Builder that accumulates ILP variables and constraints. +struct ILPBuilder { + num_vars: usize, + constraints: Vec, + variable_map: HashMap, +} + +impl ILPBuilder { + fn new() -> Self { + Self { + num_vars: 0, + constraints: Vec::new(), + variable_map: HashMap::new(), + } + } + + /// Get or create a variable index for a named circuit variable. + fn get_or_create_var(&mut self, name: &str) -> usize { + if let Some(&idx) = self.variable_map.get(name) { + idx + } else { + let idx = self.num_vars; + self.variable_map.insert(name.to_string(), idx); + self.num_vars += 1; + idx + } + } + + /// Allocate an anonymous auxiliary variable. + fn alloc_aux(&mut self) -> usize { + let idx = self.num_vars; + self.num_vars += 1; + idx + } + + /// Recursively process a BooleanExpr, returning the ILP variable index + /// that holds the expression's value. + fn process_expr(&mut self, expr: &BooleanExpr) -> usize { + match &expr.op { + BooleanOp::Var(name) => self.get_or_create_var(name), + BooleanOp::Const(value) => { + let c = self.alloc_aux(); + let v = if *value { 1.0 } else { 0.0 }; + self.constraints + .push(LinearConstraint::eq(vec![(c, 1.0)], v)); + c + } + BooleanOp::Not(inner) => { + let a = self.process_expr(inner); + let c = self.alloc_aux(); + // c + a = 1 + self.constraints + .push(LinearConstraint::eq(vec![(c, 1.0), (a, 1.0)], 1.0)); + c + } + BooleanOp::And(args) => { + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + let c = self.alloc_aux(); + let k = inputs.len() as f64; + // c ≤ a_i for all i + for &a_i in &inputs { + self.constraints + .push(LinearConstraint::le(vec![(c, 1.0), (a_i, -1.0)], 0.0)); + } + // c ≥ Σa_i - (k - 1) + let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; + for &a_i in &inputs { + terms.push((a_i, -1.0)); + } + self.constraints + .push(LinearConstraint::ge(terms, -(k - 1.0))); + c + } + BooleanOp::Or(args) => { + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + let c = self.alloc_aux(); + // c ≥ a_i for all i + for &a_i in &inputs { + self.constraints + .push(LinearConstraint::ge(vec![(c, 1.0), (a_i, -1.0)], 0.0)); + } + // c ≤ Σa_i + let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; + for &a_i in &inputs { + terms.push((a_i, -1.0)); + } + self.constraints.push(LinearConstraint::le(terms, 0.0)); + c + } + BooleanOp::Xor(args) => { + // Chain pairwise: XOR(a1, a2, a3) = XOR(XOR(a1, a2), a3) + let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); + assert!(!inputs.is_empty()); + let mut result = inputs[0]; + for &next in &inputs[1..] { + let c = self.alloc_aux(); + let a = result; + let b = next; + // c ≤ a + b + self.constraints.push(LinearConstraint::le( + vec![(c, 1.0), (a, -1.0), (b, -1.0)], + 0.0, + )); + // c ≥ a - b + self.constraints.push(LinearConstraint::ge( + vec![(c, 1.0), (a, -1.0), (b, 1.0)], + 0.0, + )); + // c ≥ b - a + self.constraints.push(LinearConstraint::ge( + vec![(c, 1.0), (a, 1.0), (b, -1.0)], + 0.0, + )); + // c ≤ 2 - a - b + self.constraints.push(LinearConstraint::le( + vec![(c, 1.0), (a, 1.0), (b, 1.0)], + 2.0, + )); + result = c; + } + result + } + } + } +} + +#[reduction( + overhead = { + ReductionOverhead::new(vec![ + ("num_vars", poly!(num_variables) + poly!(num_assignments)), + ("num_constraints", poly!(num_variables) + poly!(num_assignments)), + ]) + } +)] +impl ReduceTo for CircuitSAT { + type Result = ReductionCircuitToILP; + + fn reduce_to(&self) -> Self::Result { + let mut builder = ILPBuilder::new(); + + // Pre-register all circuit variables to preserve ordering + for name in self.variable_names() { + builder.get_or_create_var(name); + } + + // Process each assignment + for assignment in &self.circuit().assignments { + let expr_var = builder.process_expr(&assignment.expr); + // Constrain each output to equal the expression result + for output_name in &assignment.outputs { + let out_var = builder.get_or_create_var(output_name); + if out_var != expr_var { + // out = expr_var + builder.constraints.push(LinearConstraint::eq( + vec![(out_var, 1.0), (expr_var, -1.0)], + 0.0, + )); + } + } + } + + let bounds = vec![VarBounds::binary(); builder.num_vars]; + // Trivial objective: minimize 0 (satisfaction problem) + let objective = vec![]; + let target = ILP::new( + builder.num_vars, + bounds, + builder.constraints, + objective, + ObjectiveSense::Minimize, + ); + + ReductionCircuitToILP { + target, + source_variables: self.variable_names().to_vec(), + variable_map: builder.variable_map, + } + } +} + +#[cfg(test)] +#[path = "../unit_tests/rules/circuit_ilp.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 9cff61490..aaa138269 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -35,6 +35,8 @@ mod traits; pub mod unitdiskmapping; +#[cfg(feature = "ilp-solver")] +mod circuit_ilp; #[cfg(feature = "ilp-solver")] mod coloring_ilp; #[cfg(feature = "ilp-solver")] diff --git a/src/unit_tests/rules/circuit_ilp.rs b/src/unit_tests/rules/circuit_ilp.rs new file mode 100644 index 000000000..3b2b54a3b --- /dev/null +++ b/src/unit_tests/rules/circuit_ilp.rs @@ -0,0 +1,125 @@ +use super::*; +use crate::models::specialized::{Assignment, BooleanExpr, Circuit, CircuitSAT}; +use crate::solvers::BruteForce; +use std::collections::HashSet; + +#[test] +fn test_circuitsat_to_ilp_and_gate() { + // c = x AND y, constrain c = true → only x=1, y=1 satisfies + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); + assert!(!extracted.is_empty()); +} + +#[test] +fn test_circuitsat_to_ilp_or_gate() { + // c = x OR y, constrain c = true → x=1,y=0 or x=0,y=1 or x=1,y=1 + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::or(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + let ilp = reduction.target_problem(); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(ilp); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_circuitsat_to_ilp_xor_gate() { + // c = x XOR y, constrains c == (x XOR y) for all variable assignments + let circuit = Circuit::new(vec![Assignment::new( + vec!["c".to_string()], + BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); + assert_eq!(extracted.len(), 4); // all 4 truth table rows satisfy c == (x XOR y) +} + +#[test] +fn test_circuitsat_to_ilp_nested() { + // d = (x AND y) OR z, constrain d = true + let circuit = Circuit::new(vec![Assignment::new( + vec!["d".to_string()], + BooleanExpr::or(vec![ + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + BooleanExpr::var("z"), + ]), + )]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} + +#[test] +fn test_circuitsat_to_ilp_closed_loop() { + // Multi-assignment circuit: a = x AND y, b = NOT a, constrain b = false + // Satisfying: x=1, y=1 → a=true → b=false ✓ + // x=0, y=0 → a=false → b=true ✗ (b must be false) + // etc. + let circuit = Circuit::new(vec![ + Assignment::new( + vec!["a".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), + ), + Assignment::new( + vec!["b".to_string()], + BooleanExpr::not(BooleanExpr::var("a")), + ), + ]); + let source = CircuitSAT::new(circuit); + let reduction = ReduceTo::::reduce_to(&source); + + let solver = BruteForce::new(); + let best_target = solver.find_all_best(reduction.target_problem()); + let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); + + let extracted: HashSet<_> = best_target + .iter() + .map(|t| reduction.extract_solution(t)) + .collect(); + assert!(extracted.is_subset(&best_source)); +} diff --git a/src/unit_tests/rules/circuit_spinglass.rs b/src/unit_tests/rules/circuit_spinglass.rs index eb84963d1..249ad38cd 100644 --- a/src/unit_tests/rules/circuit_spinglass.rs +++ b/src/unit_tests/rules/circuit_spinglass.rs @@ -147,7 +147,7 @@ fn test_constant_true() { BooleanExpr::constant(true), )]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); let sg = reduction.target_problem(); let solver = BruteForce::new(); @@ -174,7 +174,7 @@ fn test_constant_false() { BooleanExpr::constant(false), )]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); let sg = reduction.target_problem(); let solver = BruteForce::new(); @@ -205,7 +205,7 @@ fn test_multi_input_and() { ]), )]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); let sg = reduction.target_problem(); let solver = BruteForce::new(); @@ -238,7 +238,7 @@ fn test_reduction_result_methods() { BooleanExpr::var("x"), )]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); // Test target_problem and extract_solution work let sg = reduction.target_problem(); @@ -249,7 +249,7 @@ fn test_reduction_result_methods() { fn test_empty_circuit() { let circuit = Circuit::new(vec![]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); let sg = reduction.target_problem(); // Empty circuit should result in empty SpinGlass @@ -263,7 +263,7 @@ fn test_solution_extraction() { BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), )]); let problem = CircuitSAT::new(circuit); - let reduction = problem.reduce_to(); + let reduction = ReduceTo::>::reduce_to(&problem); // The source variables are c, x, y (sorted) assert_eq!(reduction.source_variables, vec!["c", "x", "y"]); From aec9e5683eb1650ea0b79c5851994ddd90ea79f9 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Thu, 19 Feb 2026 12:05:02 +0800 Subject: [PATCH 4/4] =?UTF-8?q?docs:=20add=20examples=20and=20paper=20entr?= =?UTF-8?q?ies=20for=20QUBO=E2=86=92ILP=20and=20CircuitSAT=E2=86=92ILP=20r?= =?UTF-8?q?eductions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Remove plan files (docs/plans/2026-02-18-ilp-*) - Add reduction examples: reduction_qubo_to_ilp.rs (4-var McCormick) and reduction_circuitsat_to_ilp.rs (full adder gate encoding) - Add reduction-rule entries in paper (reductions.typ) with proofs - Regenerate reduction_graph.json with new edges - Register both examples in tests/suites/examples.rs Co-Authored-By: Claude Opus 4.6 --- docs/paper/reductions.typ | 51 ++ .../2026-02-18-ilp-reduction-paths-design.md | 78 -- .../2026-02-18-ilp-reduction-paths-impl.md | 726 ------------------ docs/src/reductions/reduction_graph.json | 30 + examples/reduction_circuitsat_to_ilp.rs | 169 ++++ examples/reduction_qubo_to_ilp.rs | 121 +++ tests/suites/examples.rs | 4 + 7 files changed, 375 insertions(+), 804 deletions(-) delete mode 100644 docs/plans/2026-02-18-ilp-reduction-paths-design.md delete mode 100644 docs/plans/2026-02-18-ilp-reduction-paths-impl.md create mode 100644 examples/reduction_circuitsat_to_ilp.rs create mode 100644 examples/reduction_qubo_to_ilp.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 39fe20b78..0e76be6e7 100644 --- a/docs/paper/reductions.typ +++ b/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") diff --git a/docs/plans/2026-02-18-ilp-reduction-paths-design.md b/docs/plans/2026-02-18-ilp-reduction-paths-design.md deleted file mode 100644 index 8f6d504c6..000000000 --- a/docs/plans/2026-02-18-ilp-reduction-paths-design.md +++ /dev/null @@ -1,78 +0,0 @@ -# ILP Reduction Paths for QUBO and CircuitSAT - -**Issue:** #83 — Add ILP reduction paths for CircuitSAT, MaxCut, QUBO, SpinGlass -**Date:** 2026-02-18 - -## Problem - -Four problem types have no reduction path to ILP, causing `pred solve` to fail with the default ILP solver: QUBO, SpinGlass, MaxCut, CircuitSAT. - -## Solution - -Two new reductions: - -1. **QUBO → ILP** — Covers QUBO, SpinGlass (via SpinGlass→QUBO→ILP), and MaxCut (via MaxCut→SpinGlass→QUBO→ILP) -2. **CircuitSAT → ILP** — Direct 1-step path (more efficient than the 3-step CircuitSAT→SpinGlass→QUBO→ILP chain) - -## Reduction 1: QUBO → ILP (McCormick Linearization) - -QUBO minimizes `x^T Q x` where `x ∈ {0,1}^n` and Q is upper-triangular. - -**Linearization:** For each non-zero off-diagonal `Q_ij` (i < j), introduce binary auxiliary `y_ij = x_i · x_j`: -- `y_ij ≤ x_i` -- `y_ij ≤ x_j` -- `y_ij ≥ x_i + x_j - 1` - -Diagonal terms are already linear: `Q_ii · x_i² = Q_ii · x_i` for binary x. - -**ILP:** -- Variables: `n` original + `m` auxiliary (m = non-zero off-diagonal count) -- All binary bounds -- Objective: `minimize Σ_i Q_ii · x_i + Σ_{i **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. - -**Goal:** Add QUBO→ILP and CircuitSAT→ILP reductions so all problem types can reach ILP (fixes #83). - -**Architecture:** Two independent reductions following existing patterns: McCormick linearization for QUBO→ILP, Tseitin-style gate encoding for CircuitSAT→ILP. Both are feature-gated behind `ilp-solver`. - -**Tech Stack:** Rust, `#[reduction]` macro, `inventory` crate for registration, `ILP` model types from `src/models/optimization/ilp.rs`. - ---- - -## Task 1: QUBO → ILP Reduction - -**Files:** -- Create: `src/rules/qubo_ilp.rs` -- Modify: `src/rules/mod.rs` (add module declaration) -- Test: `src/unit_tests/rules/qubo_ilp.rs` - -**Reference:** `src/rules/maximumindependentset_ilp.rs` for ILP reduction pattern, `src/rules/factoring_ilp.rs` for McCormick pattern. - -### Step 1: Write the failing test - -Create `src/unit_tests/rules/qubo_ilp.rs`: - -```rust -use super::*; -use crate::solvers::BruteForce; -use crate::traits::Problem; -use std::collections::HashSet; - -#[test] -fn test_qubo_to_ilp_closed_loop() { - // QUBO: minimize 2*x0 - 3*x1 + x0*x1 - // Q = [[2, 1], [0, -3]] - // x=0,0 -> 0, x=1,0 -> 2, x=0,1 -> -3, x=1,1 -> 0 - // Optimal: x = [0, 1] with obj = -3 - let qubo = QUBO::from_matrix(vec![vec![2.0, 1.0], vec![0.0, -3.0]]); - let reduction = ReduceTo::::reduce_to(&qubo); - let ilp = reduction.target_problem(); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(ilp); - let best_source: HashSet<_> = solver.find_all_best(&qubo).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); -} - -#[test] -fn test_qubo_to_ilp_diagonal_only() { - // No quadratic terms: minimize 3*x0 - 2*x1 - // Optimal: x = [0, 1] with obj = -2 - let qubo = QUBO::from_matrix(vec![vec![3.0, 0.0], vec![0.0, -2.0]]); - let reduction = ReduceTo::::reduce_to(&qubo); - let ilp = reduction.target_problem(); - - // No auxiliary variables when no off-diagonal terms - assert_eq!(ilp.num_variables(), 2); - assert!(ilp.constraints.is_empty()); - - let solver = BruteForce::new(); - let best = solver.find_all_best(ilp); - let extracted = reduction.extract_solution(&best[0]); - assert_eq!(extracted, vec![0, 1]); -} - -#[test] -fn test_qubo_to_ilp_3var() { - // QUBO: minimize -x0 - x1 - x2 + 4*x0*x1 + 4*x1*x2 - // Penalty on adjacent pairs → optimal is [1, 0, 1] - let qubo = QUBO::from_matrix(vec![ - vec![-1.0, 4.0, 0.0], - vec![0.0, -1.0, 4.0], - vec![0.0, 0.0, -1.0], - ]); - let reduction = ReduceTo::::reduce_to(&qubo); - let ilp = reduction.target_problem(); - - // 3 original + 2 auxiliary (for two off-diagonal terms) - assert_eq!(ilp.num_variables(), 5); - // 3 constraints per auxiliary = 6 - assert_eq!(ilp.constraints.len(), 6); - - let solver = BruteForce::new(); - let best = solver.find_all_best(ilp); - let extracted = reduction.extract_solution(&best[0]); - assert_eq!(extracted, vec![1, 0, 1]); -} -``` - -### Step 2: Run test to verify it fails - -Run: `cargo test --features ilp-solver test_qubo_to_ilp -- --nocapture 2>&1 | head -30` -Expected: Compilation error (module doesn't exist yet) - -### Step 3: Write the reduction implementation - -Create `src/rules/qubo_ilp.rs`: - -```rust -//! Reduction from QUBO to ILP via McCormick linearization. -//! -//! QUBO minimizes x^T Q x where x ∈ {0,1}^n and Q is upper-triangular. -//! -//! ## Linearization -//! - Diagonal: Q_ii · x_i² = Q_ii · x_i (linear for binary x) -//! - Off-diagonal: For each non-zero Q_ij (i < j), introduce y_ij = x_i · x_j -//! with McCormick constraints: y_ij ≤ x_i, y_ij ≤ x_j, y_ij ≥ x_i + x_j - 1 -//! -//! ## Variables -//! - x_i ∈ {0,1} for i = 0..n-1 (original QUBO variables) -//! - y_k ∈ {0,1} for each non-zero off-diagonal Q_ij (auxiliary products) -//! -//! ## Objective -//! minimize Σ_i Q_ii · x_i + Σ_{i; - type Target = ILP; - - fn target_problem(&self) -> &ILP { - &self.target - } - - fn extract_solution(&self, target_solution: &[usize]) -> Vec { - target_solution[..self.num_original].to_vec() - } -} - -#[reduction( - overhead = { - ReductionOverhead::new(vec![ - ("num_vars", poly!(num_vars ^ 2)), - ("num_constraints", poly!(num_vars ^ 2)), - ]) - } -)] -impl ReduceTo for QUBO { - type Result = ReductionQUBOToILP; - - fn reduce_to(&self) -> Self::Result { - let n = self.num_vars(); - let matrix = self.matrix(); - - // Collect non-zero off-diagonal entries (i < j) - let mut off_diag: Vec<(usize, usize, f64)> = Vec::new(); - for i in 0..n { - for j in (i + 1)..n { - let q_ij = matrix[i][j]; - if q_ij != 0.0 { - off_diag.push((i, j, q_ij)); - } - } - } - - let m = off_diag.len(); - let total_vars = n + m; - - // All variables are binary - let bounds = vec![VarBounds::binary(); total_vars]; - - // Objective: minimize Σ Q_ii · x_i + Σ Q_ij · y_k - let mut objective: Vec<(usize, f64)> = Vec::new(); - for i in 0..n { - let q_ii = matrix[i][i]; - if q_ii != 0.0 { - objective.push((i, q_ii)); - } - } - for (k, &(_, _, q_ij)) in off_diag.iter().enumerate() { - objective.push((n + k, q_ij)); - } - - // McCormick constraints: 3 per auxiliary variable - let mut constraints = Vec::with_capacity(3 * m); - for (k, &(i, j, _)) in off_diag.iter().enumerate() { - let y_k = n + k; - // y_k ≤ x_i - constraints.push(LinearConstraint::le( - vec![(y_k, 1.0), (i, -1.0)], - 0.0, - )); - // y_k ≤ x_j - constraints.push(LinearConstraint::le( - vec![(y_k, 1.0), (j, -1.0)], - 0.0, - )); - // y_k ≥ x_i + x_j - 1 - constraints.push(LinearConstraint::ge( - vec![(y_k, 1.0), (i, -1.0), (j, -1.0)], - -1.0, - )); - } - - let target = ILP::new(total_vars, bounds, constraints, objective, ObjectiveSense::Minimize); - ReductionQUBOToILP { - target, - num_original: n, - } - } -} - -#[cfg(test)] -#[path = "../unit_tests/rules/qubo_ilp.rs"] -mod tests; -``` - -### Step 4: Register module in `src/rules/mod.rs` - -Add after the existing `ilp_qubo` line: - -```rust -#[cfg(feature = "ilp-solver")] -mod qubo_ilp; -``` - -### Step 5: Run tests to verify they pass - -Run: `cargo test --features ilp-solver test_qubo_to_ilp -- --nocapture` -Expected: All 3 tests pass - -### Step 6: Commit - -```bash -git add src/rules/qubo_ilp.rs src/rules/mod.rs src/unit_tests/rules/qubo_ilp.rs -git commit -m "feat: add QUBO → ILP reduction via McCormick linearization - -Closes the ILP path for QUBO, SpinGlass, and MaxCut (issue #83)." -``` - ---- - -## Task 2: CircuitSAT → ILP Reduction - -**Files:** -- Create: `src/rules/circuit_ilp.rs` -- Modify: `src/rules/mod.rs` (add module declaration) -- Test: `src/unit_tests/rules/circuit_ilp.rs` - -**Reference:** `src/rules/circuit_spinglass.rs` for expression tree walking, `src/rules/maximumindependentset_ilp.rs` for ILP reduction structure. - -### Step 1: Write the failing test - -Create `src/unit_tests/rules/circuit_ilp.rs`: - -```rust -use super::*; -use crate::models::specialized::{Assignment, BooleanExpr, Circuit, CircuitSAT}; -use crate::solvers::BruteForce; -use crate::traits::Problem; -use std::collections::HashSet; - -#[test] -fn test_circuitsat_to_ilp_and_gate() { - // c = x AND y, constrain c = true → only x=1, y=1 satisfies - let circuit = Circuit::new(vec![Assignment::new( - vec!["c".to_string()], - BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), - )]); - let source = CircuitSAT::new(circuit); - let reduction = ReduceTo::::reduce_to(&source); - let ilp = reduction.target_problem(); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(ilp); - let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); - assert!(!extracted.is_empty()); -} - -#[test] -fn test_circuitsat_to_ilp_or_gate() { - // c = x OR y, constrain c = true → x=1,y=0 or x=0,y=1 or x=1,y=1 - let circuit = Circuit::new(vec![Assignment::new( - vec!["c".to_string()], - BooleanExpr::or(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), - )]); - let source = CircuitSAT::new(circuit); - let reduction = ReduceTo::::reduce_to(&source); - let ilp = reduction.target_problem(); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(ilp); - let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); -} - -#[test] -fn test_circuitsat_to_ilp_xor_gate() { - // c = x XOR y, constrain c = true → x=1,y=0 or x=0,y=1 - let circuit = Circuit::new(vec![Assignment::new( - vec!["c".to_string()], - BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), - )]); - let source = CircuitSAT::new(circuit); - let reduction = ReduceTo::::reduce_to(&source); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(reduction.target_problem()); - let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); - assert_eq!(extracted.len(), 2); // exactly x=1,y=0 and x=0,y=1 -} - -#[test] -fn test_circuitsat_to_ilp_nested() { - // d = (x AND y) OR z, constrain d = true - let circuit = Circuit::new(vec![Assignment::new( - vec!["d".to_string()], - BooleanExpr::or(vec![ - BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), - BooleanExpr::var("z"), - ]), - )]); - let source = CircuitSAT::new(circuit); - let reduction = ReduceTo::::reduce_to(&source); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(reduction.target_problem()); - let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); -} - -#[test] -fn test_circuitsat_to_ilp_closed_loop() { - // Multi-assignment circuit: a = x AND y, b = NOT a, constrain b = false - // Satisfying: x=1, y=1 → a=true → b=false ✓ - // x=0, y=0 → a=false → b=true ✗ (b must be false) - // etc. - let circuit = Circuit::new(vec![ - Assignment::new( - vec!["a".to_string()], - BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]), - ), - Assignment::new( - vec!["b".to_string()], - BooleanExpr::not(BooleanExpr::var("a")), - ), - ]); - let source = CircuitSAT::new(circuit); - let reduction = ReduceTo::::reduce_to(&source); - - let solver = BruteForce::new(); - let best_target = solver.find_all_best(reduction.target_problem()); - let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect(); - - let extracted: HashSet<_> = best_target - .iter() - .map(|t| reduction.extract_solution(t)) - .collect(); - assert!(extracted.is_subset(&best_source)); -} -``` - -### Step 2: Run test to verify it fails - -Run: `cargo test --features ilp-solver test_circuitsat_to_ilp -- --nocapture 2>&1 | head -30` -Expected: Compilation error - -### Step 3: Write the reduction implementation - -Create `src/rules/circuit_ilp.rs`: - -```rust -//! Reduction from CircuitSAT to ILP via gate constraint encoding. -//! -//! Each boolean gate is encoded as linear constraints over binary variables. -//! The expression tree is flattened by introducing an auxiliary variable per -//! internal node (Tseitin-style). -//! -//! ## Gate Encodings (all variables binary) -//! - NOT(a) = c: c + a = 1 -//! - AND(a₁,...,aₖ) = c: c ≤ aᵢ (∀i), c ≥ Σaᵢ - (k-1) -//! - OR(a₁,...,aₖ) = c: c ≥ aᵢ (∀i), c ≤ Σaᵢ -//! - XOR(a, b) = c: c ≤ a+b, c ≥ a-b, c ≥ b-a, c ≤ 2-a-b -//! - Const(v) = c: c = v -//! -//! ## Objective -//! Trivial (minimize 0): any feasible ILP solution is a satisfying assignment. - -use crate::models::optimization::{LinearConstraint, ObjectiveSense, VarBounds, ILP}; -use crate::models::specialized::{BooleanExpr, BooleanOp, CircuitSAT}; -use crate::poly; -use crate::reduction; -use crate::rules::registry::ReductionOverhead; -use crate::rules::traits::{ReduceTo, ReductionResult}; -use std::collections::HashMap; - -/// Result of reducing CircuitSAT to ILP. -#[derive(Debug, Clone)] -pub struct ReductionCircuitToILP { - target: ILP, - source_variables: Vec, - variable_map: HashMap, -} - -impl ReductionResult for ReductionCircuitToILP { - type Source = CircuitSAT; - type Target = ILP; - - fn target_problem(&self) -> &ILP { - &self.target - } - - fn extract_solution(&self, target_solution: &[usize]) -> Vec { - self.source_variables - .iter() - .map(|name| target_solution[self.variable_map[name]]) - .collect() - } -} - -/// Builder that accumulates ILP variables and constraints. -struct ILPBuilder { - num_vars: usize, - constraints: Vec, - variable_map: HashMap, -} - -impl ILPBuilder { - fn new() -> Self { - Self { - num_vars: 0, - constraints: Vec::new(), - variable_map: HashMap::new(), - } - } - - /// Get or create a variable index for a named circuit variable. - fn get_or_create_var(&mut self, name: &str) -> usize { - if let Some(&idx) = self.variable_map.get(name) { - idx - } else { - let idx = self.num_vars; - self.variable_map.insert(name.to_string(), idx); - self.num_vars += 1; - idx - } - } - - /// Allocate an anonymous auxiliary variable. - fn alloc_aux(&mut self) -> usize { - let idx = self.num_vars; - self.num_vars += 1; - idx - } - - /// Recursively process a BooleanExpr, returning the ILP variable index - /// that holds the expression's value. - fn process_expr(&mut self, expr: &BooleanExpr) -> usize { - match &expr.op { - BooleanOp::Var(name) => self.get_or_create_var(name), - BooleanOp::Const(value) => { - let c = self.alloc_aux(); - let v = if *value { 1.0 } else { 0.0 }; - self.constraints.push(LinearConstraint::eq(vec![(c, 1.0)], v)); - c - } - BooleanOp::Not(inner) => { - let a = self.process_expr(inner); - let c = self.alloc_aux(); - // c + a = 1 - self.constraints - .push(LinearConstraint::eq(vec![(c, 1.0), (a, 1.0)], 1.0)); - c - } - BooleanOp::And(args) => { - let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); - let c = self.alloc_aux(); - let k = inputs.len() as f64; - // c ≤ a_i for all i - for &a_i in &inputs { - self.constraints - .push(LinearConstraint::le(vec![(c, 1.0), (a_i, -1.0)], 0.0)); - } - // c ≥ Σa_i - (k - 1) - let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; - for &a_i in &inputs { - terms.push((a_i, -1.0)); - } - self.constraints - .push(LinearConstraint::ge(terms, -(k - 1.0))); - c - } - BooleanOp::Or(args) => { - let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); - let c = self.alloc_aux(); - // c ≥ a_i for all i - for &a_i in &inputs { - self.constraints - .push(LinearConstraint::ge(vec![(c, 1.0), (a_i, -1.0)], 0.0)); - } - // c ≤ Σa_i - let mut terms: Vec<(usize, f64)> = vec![(c, 1.0)]; - for &a_i in &inputs { - terms.push((a_i, -1.0)); - } - self.constraints.push(LinearConstraint::le(terms, 0.0)); - c - } - BooleanOp::Xor(args) => { - // Chain pairwise: XOR(a1, a2, a3) = XOR(XOR(a1, a2), a3) - let inputs: Vec = args.iter().map(|a| self.process_expr(a)).collect(); - assert!(!inputs.is_empty()); - let mut result = inputs[0]; - for &next in &inputs[1..] { - let c = self.alloc_aux(); - let a = result; - let b = next; - // c ≤ a + b - self.constraints.push(LinearConstraint::le( - vec![(c, 1.0), (a, -1.0), (b, -1.0)], - 0.0, - )); - // c ≥ a - b - self.constraints.push(LinearConstraint::ge( - vec![(c, 1.0), (a, -1.0), (b, 1.0)], - 0.0, - )); - // c ≥ b - a - self.constraints.push(LinearConstraint::ge( - vec![(c, 1.0), (a, 1.0), (b, -1.0)], - 0.0, - )); - // c ≤ 2 - a - b - self.constraints.push(LinearConstraint::le( - vec![(c, 1.0), (a, 1.0), (b, 1.0)], - 2.0, - )); - result = c; - } - result - } - } - } -} - -#[reduction( - overhead = { - ReductionOverhead::new(vec![ - ("num_vars", poly!(num_variables + num_assignments)), - ("num_constraints", poly!(num_variables + num_assignments)), - ]) - } -)] -impl ReduceTo for CircuitSAT { - type Result = ReductionCircuitToILP; - - fn reduce_to(&self) -> Self::Result { - let mut builder = ILPBuilder::new(); - - // Pre-register all circuit variables to preserve ordering - for name in self.variable_names() { - builder.get_or_create_var(name); - } - - // Process each assignment - for assignment in &self.circuit().assignments { - let expr_var = builder.process_expr(&assignment.expr); - // Constrain each output to equal the expression result - for output_name in &assignment.outputs { - let out_var = builder.get_or_create_var(output_name); - if out_var != expr_var { - // out = expr_var - builder.constraints.push(LinearConstraint::eq( - vec![(out_var, 1.0), (expr_var, -1.0)], - 0.0, - )); - } - } - } - - let bounds = vec![VarBounds::binary(); builder.num_vars]; - // Trivial objective: minimize 0 (satisfaction problem) - let objective = vec![]; - let target = ILP::new( - builder.num_vars, - bounds, - builder.constraints, - objective, - ObjectiveSense::Minimize, - ); - - ReductionCircuitToILP { - target, - source_variables: self.variable_names().to_vec(), - variable_map: builder.variable_map, - } - } -} - -#[cfg(test)] -#[path = "../unit_tests/rules/circuit_ilp.rs"] -mod tests; -``` - -### Step 4: Register module in `src/rules/mod.rs` - -Add after the `coloring_ilp` line in the `#[cfg(feature = "ilp-solver")]` block: - -```rust -#[cfg(feature = "ilp-solver")] -mod circuit_ilp; -``` - -### Step 5: Run tests to verify they pass - -Run: `cargo test --features ilp-solver test_circuitsat_to_ilp -- --nocapture` -Expected: All 5 tests pass - -### Step 6: Commit - -```bash -git add src/rules/circuit_ilp.rs src/rules/mod.rs src/unit_tests/rules/circuit_ilp.rs -git commit -m "feat: add CircuitSAT → ILP reduction via gate constraint encoding - -Direct 1-step path, more efficient than CircuitSAT→SpinGlass→QUBO→ILP (issue #83)." -``` - ---- - -## Task 3: Integration Verification - -### Step 1: Run full test suite - -Run: `make test clippy` -Expected: All tests pass, no clippy warnings - -### Step 2: Verify reduction graph has new paths - -Run: `cargo test --features ilp-solver test_reduction_graph -- --nocapture 2>&1 | grep -i "qubo\|circuit"` or check the graph test file at `src/unit_tests/rules/graph.rs` for existing assertions and add new ones if needed. - -### Step 3: Test CLI integration (if on the cli-tool-design branch) - -Run: -```bash -echo '{"problem":"QUBO","instance":{"matrix":[[2.0,1.0],[0.0,-3.0]]}}' > /tmp/qubo_test.json -cargo run --features ilp-solver -- solve /tmp/qubo_test.json -``` -Expected: Solution found (not "No reduction path" error) - -### Step 4: Commit any fixes - ---- - -## Task 4: Examples and Documentation (Optional — can be a follow-up PR) - -**Files:** -- Create: `examples/reduction_qubo_to_ilp.rs` -- Create: `examples/reduction_circuitsat_to_ilp.rs` -- Modify: `tests/suites/examples.rs` (register new examples) -- Modify: `docs/paper/reductions.typ` (add reduction-rule entries) - -### Step 1: Create QUBO → ILP example - -Follow pattern from `examples/reduction_ilp_to_qubo.rs`: -- Create a small QUBO instance (e.g., 3-variable) -- Reduce to ILP, print transformation details -- Solve with BruteForce, extract and verify -- Export JSON to `docs/paper/examples/` - -### Step 2: Create CircuitSAT → ILP example - -Follow pattern from `examples/reduction_circuitsat_to_spinglass.rs`: -- Create a small circuit (e.g., AND + NOT) -- Reduce to ILP, print transformation details -- Solve, extract and verify -- Export JSON - -### Step 3: Register examples in test suite - -Add to `tests/suites/examples.rs`: -```rust -example_test!(reduction_qubo_to_ilp); -example_test!(reduction_circuitsat_to_ilp); -example_fn!(test_qubo_to_ilp, reduction_qubo_to_ilp); -example_fn!(test_circuitsat_to_ilp, reduction_circuitsat_to_ilp); -``` - -### Step 4: Add paper entries - -In `docs/paper/reductions.typ`, add `reduction-rule` entries for both new reductions. - -### Step 5: Commit - -```bash -git add examples/ tests/suites/examples.rs docs/ -git commit -m "docs: add examples and paper entries for QUBO→ILP and CircuitSAT→ILP" -``` diff --git a/docs/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json index 7f6e9f683..acf4bd9eb 100644 --- a/docs/src/reductions/reduction_graph.json +++ b/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, diff --git a/examples/reduction_circuitsat_to_ilp.rs b/examples/reduction_circuitsat_to_ilp.rs new file mode 100644 index 000000000..a5415087a --- /dev/null +++ b/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::::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 = 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() +} diff --git a/examples/reduction_qubo_to_ilp.rs b/examples/reduction_qubo_to_ilp.rs new file mode 100644 index 000000000..2dcaaa868 --- /dev/null +++ b/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::::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::::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::::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() +} diff --git a/tests/suites/examples.rs b/tests/suites/examples.rs index 6658d0566..721c1ed8c 100644 --- a/tests/suites/examples.rs +++ b/tests/suites/examples.rs @@ -12,6 +12,7 @@ macro_rules! example_test { example_test!(chained_reduction_factoring_to_spinglass); example_test!(chained_reduction_ksat_to_mis); +example_test!(reduction_circuitsat_to_ilp); example_test!(reduction_circuitsat_to_spinglass); example_test!(reduction_factoring_to_circuitsat); example_test!(reduction_factoring_to_ilp); @@ -35,6 +36,7 @@ example_test!(reduction_minimumvertexcover_to_ilp); example_test!(reduction_minimumvertexcover_to_maximumindependentset); example_test!(reduction_minimumvertexcover_to_minimumsetcovering); example_test!(reduction_minimumvertexcover_to_qubo); +example_test!(reduction_qubo_to_ilp); example_test!(reduction_qubo_to_spinglass); example_test!(reduction_satisfiability_to_kcoloring); example_test!(reduction_satisfiability_to_ksatisfiability); @@ -61,6 +63,7 @@ example_fn!( test_chained_reduction_ksat_to_mis, chained_reduction_ksat_to_mis ); +example_fn!(test_circuitsat_to_ilp, reduction_circuitsat_to_ilp); example_fn!( test_circuitsat_to_spinglass, reduction_circuitsat_to_spinglass @@ -135,6 +138,7 @@ example_fn!( test_minimumvertexcover_to_qubo, reduction_minimumvertexcover_to_qubo ); +example_fn!(test_qubo_to_ilp, reduction_qubo_to_ilp); example_fn!(test_qubo_to_spinglass, reduction_qubo_to_spinglass); example_fn!( test_satisfiability_to_kcoloring,