diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 39fe20b7..0e76be6e 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/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json index 7f6e9f68..acf4bd9e 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 00000000..a5415087 --- /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 00000000..2dcaaa86 --- /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/src/rules/circuit_ilp.rs b/src/rules/circuit_ilp.rs new file mode 100644 index 00000000..04e89f25 --- /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 678cd0a4..aaa13826 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")] @@ -56,6 +58,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 00000000..9f7c3100 --- /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/circuit_ilp.rs b/src/unit_tests/rules/circuit_ilp.rs new file mode 100644 index 00000000..3b2b54a3 --- /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 eb84963d..249ad38c 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"]); diff --git a/src/unit_tests/rules/qubo_ilp.rs b/src/unit_tests/rules/qubo_ilp.rs new file mode 100644 index 00000000..cea0abe8 --- /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]); +} diff --git a/tests/suites/examples.rs b/tests/suites/examples.rs index 6658d056..721c1ed8 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,