problemreductions/rules/
circuit_ilp.rs

1//! Reduction from CircuitSAT to ILP via gate constraint encoding.
2//!
3//! Each boolean gate is encoded as linear constraints over binary variables.
4//! The expression tree is flattened by introducing an auxiliary variable per
5//! internal node (Tseitin-style).
6//!
7//! ## Gate Encodings (all variables binary)
8//! - NOT(a) = c:           c + a = 1
9//! - AND(a₁,...,aₖ) = c:  c ≤ aᵢ (∀i), c ≥ Σaᵢ - (k-1)
10//! - OR(a₁,...,aₖ) = c:   c ≥ aᵢ (∀i), c ≤ Σaᵢ
11//! - XOR(a, b) = c:        c ≤ a+b, c ≥ a-b, c ≥ b-a, c ≤ 2-a-b
12//! - Const(v) = c:          c = v
13//!
14//! ## Objective
15//! Trivial (minimize 0): any feasible ILP solution is a satisfying assignment.
16
17use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
18use crate::models::formula::{BooleanExpr, BooleanOp, CircuitSAT};
19use crate::reduction;
20use crate::rules::traits::{ReduceTo, ReductionResult};
21use std::collections::HashMap;
22
23/// Result of reducing CircuitSAT to ILP.
24#[derive(Debug, Clone)]
25pub struct ReductionCircuitToILP {
26    target: ILP<bool>,
27    source_variables: Vec<String>,
28    variable_map: HashMap<String, usize>,
29}
30
31impl ReductionResult for ReductionCircuitToILP {
32    type Source = CircuitSAT;
33    type Target = ILP<bool>;
34
35    fn target_problem(&self) -> &ILP<bool> {
36        &self.target
37    }
38
39    fn extract_solution(
40        &self,
41        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
42    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
43        if crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?
44            .value
45            .is_none()
46        {
47            return Err(crate::rules::ExtractionError::invalid(
48                "target ILP assignment is infeasible",
49            ));
50        }
51
52        Ok({
53            self.source_variables
54                .iter()
55                .map(|name| target_solution[self.variable_map[name]] == 1)
56                .collect()
57        })
58    }
59}
60
61/// Builder that accumulates ILP variables and constraints.
62struct ILPBuilder {
63    num_vars: usize,
64    constraints: Vec<LinearConstraint>,
65    variable_map: HashMap<String, usize>,
66}
67
68impl ILPBuilder {
69    fn new() -> Self {
70        Self {
71            num_vars: 0,
72            constraints: Vec::new(),
73            variable_map: HashMap::new(),
74        }
75    }
76
77    /// Get or create a variable index for a named circuit variable.
78    fn get_or_create_var(&mut self, name: &str) -> Result<usize, crate::rules::ReductionError> {
79        if let Some(&idx) = self.variable_map.get(name) {
80            Ok(idx)
81        } else {
82            let idx = self.alloc_aux()?;
83            self.variable_map.insert(name.to_string(), idx);
84            Ok(idx)
85        }
86    }
87
88    /// Allocate an anonymous auxiliary variable.
89    fn alloc_aux(&mut self) -> Result<usize, crate::rules::ReductionError> {
90        let idx = self.num_vars;
91        self.num_vars = self.num_vars.checked_add(1).ok_or_else(|| {
92            crate::rules::ReductionError::integer_overflow::<CircuitSAT, ILP<bool>>(
93                "allocating a circuit ILP variable",
94            )
95        })?;
96        Ok(idx)
97    }
98
99    /// Recursively process a BooleanExpr, returning the ILP variable index
100    /// that holds the expression's value.
101    fn process_expr(&mut self, expr: &BooleanExpr) -> Result<usize, crate::rules::ReductionError> {
102        Ok(match &expr.op {
103            BooleanOp::Var(name) => self.get_or_create_var(name)?,
104            BooleanOp::Const(value) => {
105                let c = self.alloc_aux()?;
106                let v = if *value { 1 } else { 0 };
107                self.constraints.push(LinearConstraint::eq(vec![(c, 1)], v));
108                c
109            }
110            BooleanOp::Not(inner) => {
111                let a = self.process_expr(inner)?;
112                let c = self.alloc_aux()?;
113                // c + a = 1
114                self.constraints
115                    .push(LinearConstraint::eq(vec![(c, 1), (a, 1)], 1));
116                c
117            }
118            BooleanOp::And(args) => {
119                let inputs: Vec<usize> = args
120                    .iter()
121                    .map(|arg| self.process_expr(arg))
122                    .collect::<Result<_, _>>()?;
123                let c = self.alloc_aux()?;
124                let k = <CircuitSAT as ReduceTo<ILP<bool>>>::exact_i64(
125                    inputs.len(),
126                    "encoding a circuit gate arity",
127                )?;
128                // c ≤ a_i for all i
129                for &a_i in &inputs {
130                    self.constraints
131                        .push(LinearConstraint::le(vec![(c, 1), (a_i, -1)], 0));
132                }
133                // c ≥ Σa_i - (k - 1)
134                let mut terms: Vec<(usize, i64)> = vec![(c, 1)];
135                for &a_i in &inputs {
136                    terms.push((a_i, -1));
137                }
138                self.constraints.push(LinearConstraint::ge(terms, 1 - k));
139                c
140            }
141            BooleanOp::Or(args) => {
142                let inputs: Vec<usize> = args
143                    .iter()
144                    .map(|arg| self.process_expr(arg))
145                    .collect::<Result<_, _>>()?;
146                let c = self.alloc_aux()?;
147                // c ≥ a_i for all i
148                for &a_i in &inputs {
149                    self.constraints
150                        .push(LinearConstraint::ge(vec![(c, 1), (a_i, -1)], 0));
151                }
152                // c ≤ Σa_i
153                let mut terms: Vec<(usize, i64)> = vec![(c, 1)];
154                for &a_i in &inputs {
155                    terms.push((a_i, -1));
156                }
157                self.constraints.push(LinearConstraint::le(terms, 0));
158                c
159            }
160            BooleanOp::Xor(args) => {
161                // Chain pairwise: XOR(a1, a2, a3) = XOR(XOR(a1, a2), a3)
162                let inputs: Vec<usize> = args
163                    .iter()
164                    .map(|arg| self.process_expr(arg))
165                    .collect::<Result<_, _>>()?;
166                let mut inputs = inputs.into_iter();
167                let mut result = match inputs.next() {
168                    Some(first) => first,
169                    // False is the identity of the Boolean XOR fold.
170                    None => self.process_expr(&BooleanExpr::constant(false))?,
171                };
172                for next in inputs {
173                    let c = self.alloc_aux()?;
174                    let a = result;
175                    let b = next;
176                    // c ≤ a + b
177                    self.constraints
178                        .push(LinearConstraint::le(vec![(c, 1), (a, -1), (b, -1)], 0));
179                    // c ≥ a - b
180                    self.constraints
181                        .push(LinearConstraint::ge(vec![(c, 1), (a, -1), (b, 1)], 0));
182                    // c ≥ b - a
183                    self.constraints
184                        .push(LinearConstraint::ge(vec![(c, 1), (a, 1), (b, -1)], 0));
185                    // c ≤ 2 - a - b
186                    self.constraints
187                        .push(LinearConstraint::le(vec![(c, 1), (a, 1), (b, 1)], 2));
188                    result = c;
189                }
190                result
191            }
192        })
193    }
194}
195
196#[reduction(
197    transform = upper_bound {
198        num_vars = "num_variables + 2 * num_expression_nodes",
199        num_constraints = "5 * num_expression_nodes + num_assignment_outputs",
200    },
201    unavailable = {
202        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
203    }
204)]
205impl ReduceTo<ILP<bool>> for CircuitSAT {
206    type Result = ReductionCircuitToILP;
207
208    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
209        let mut builder = ILPBuilder::new();
210
211        // Pre-register all circuit variables to preserve ordering
212        for name in self.variable_names() {
213            builder.get_or_create_var(name)?;
214        }
215
216        // Process each assignment
217        for assignment in &self.circuit().assignments {
218            let expr_var = builder.process_expr(&assignment.expr)?;
219            // Constrain each output to equal the expression result
220            for output_name in &assignment.outputs {
221                let out_var = builder.get_or_create_var(output_name)?;
222                if out_var != expr_var {
223                    // out = expr_var
224                    builder
225                        .constraints
226                        .push(LinearConstraint::eq(vec![(out_var, 1), (expr_var, -1)], 0));
227                }
228            }
229        }
230
231        // Trivial objective: minimize 0 (satisfaction problem)
232        let objective = vec![];
233        let target = ILP::new(
234            builder.num_vars,
235            builder.constraints,
236            objective,
237            ObjectiveSense::Minimize,
238        )
239        .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
240
241        Ok(ReductionCircuitToILP {
242            target,
243            source_variables: self.variable_names().to_vec(),
244            variable_map: builder.variable_map,
245        })
246    }
247}
248
249#[cfg(feature = "example-db")]
250pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
251    use crate::export::SolutionPair;
252    use crate::models::formula::{Assignment, BooleanExpr, Circuit};
253
254    fn full_adder_circuit_sat() -> CircuitSAT {
255        let circuit = Circuit::new(vec![
256            Assignment::new(
257                vec!["t".to_string()],
258                BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
259            ),
260            Assignment::new(
261                vec!["sum".to_string()],
262                BooleanExpr::xor(vec![BooleanExpr::var("t"), BooleanExpr::var("cin")]),
263            ),
264            Assignment::new(
265                vec!["ab".to_string()],
266                BooleanExpr::and(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
267            ),
268            Assignment::new(
269                vec!["cin_t".to_string()],
270                BooleanExpr::and(vec![BooleanExpr::var("cin"), BooleanExpr::var("t")]),
271            ),
272            Assignment::new(
273                vec!["cout".to_string()],
274                BooleanExpr::or(vec![BooleanExpr::var("ab"), BooleanExpr::var("cin_t")]),
275            ),
276        ]);
277        CircuitSAT::new(circuit)
278    }
279
280    vec![crate::example_db::specs::RuleExampleSpec {
281        id: "circuitsat_to_ilp",
282        build: || {
283            crate::example_db::specs::rule_example_with_witness::<
284                _,
285                crate::models::algebraic::ILP<bool>,
286            >(
287                full_adder_circuit_sat(),
288                SolutionPair {
289                    source_config: serde_json::json!(vec![
290                        false, false, false, false, false, false, false, false
291                    ]),
292                    target_config: serde_json::json!(vec![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]),
293                },
294            )
295        },
296    }]
297}
298
299#[cfg(test)]
300#[path = "../unit_tests/rules/circuit_ilp.rs"]
301mod tests;
problemreductions/rules/circuit_ilp.rs

problemreductions/rules/
circuit_ilp.rs
