problemreductions/models/specialized/
circuit.rs

1//! Circuit SAT problem implementation.
2//!
3//! CircuitSAT represents a boolean circuit satisfiability problem.
4//! The goal is to find variable assignments that satisfy the circuit constraints.
5
6use crate::graph_types::SimpleGraph;
7use crate::traits::Problem;
8use crate::types::{EnergyMode, ProblemSize, SolutionSize};
9use serde::{Deserialize, Serialize};
10use std::collections::HashMap;
11
12/// Boolean expression node types.
13#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
14pub enum BooleanOp {
15    /// Variable reference
16    Var(String),
17    /// Boolean constant
18    Const(bool),
19    /// NOT operation
20    Not(Box<BooleanExpr>),
21    /// AND operation
22    And(Vec<BooleanExpr>),
23    /// OR operation
24    Or(Vec<BooleanExpr>),
25    /// XOR operation
26    Xor(Vec<BooleanExpr>),
27}
28
29/// A boolean expression tree.
30#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
31pub struct BooleanExpr {
32    pub op: BooleanOp,
33}
34
35impl BooleanExpr {
36    /// Create a variable reference.
37    pub fn var(name: &str) -> Self {
38        BooleanExpr {
39            op: BooleanOp::Var(name.to_string()),
40        }
41    }
42
43    /// Create a boolean constant.
44    pub fn constant(value: bool) -> Self {
45        BooleanExpr {
46            op: BooleanOp::Const(value),
47        }
48    }
49
50    /// Create a NOT expression.
51    #[allow(clippy::should_implement_trait)]
52    pub fn not(expr: BooleanExpr) -> Self {
53        BooleanExpr {
54            op: BooleanOp::Not(Box::new(expr)),
55        }
56    }
57
58    /// Create an AND expression.
59    pub fn and(args: Vec<BooleanExpr>) -> Self {
60        BooleanExpr {
61            op: BooleanOp::And(args),
62        }
63    }
64
65    /// Create an OR expression.
66    pub fn or(args: Vec<BooleanExpr>) -> Self {
67        BooleanExpr {
68            op: BooleanOp::Or(args),
69        }
70    }
71
72    /// Create an XOR expression.
73    pub fn xor(args: Vec<BooleanExpr>) -> Self {
74        BooleanExpr {
75            op: BooleanOp::Xor(args),
76        }
77    }
78
79    /// Extract all variable names from this expression.
80    pub fn variables(&self) -> Vec<String> {
81        let mut vars = Vec::new();
82        self.extract_variables(&mut vars);
83        vars.sort();
84        vars.dedup();
85        vars
86    }
87
88    fn extract_variables(&self, vars: &mut Vec<String>) {
89        match &self.op {
90            BooleanOp::Var(name) => vars.push(name.clone()),
91            BooleanOp::Const(_) => {}
92            BooleanOp::Not(inner) => inner.extract_variables(vars),
93            BooleanOp::And(args) | BooleanOp::Or(args) | BooleanOp::Xor(args) => {
94                for arg in args {
95                    arg.extract_variables(vars);
96                }
97            }
98        }
99    }
100
101    /// Evaluate the expression given variable assignments.
102    pub fn evaluate(&self, assignments: &HashMap<String, bool>) -> bool {
103        match &self.op {
104            BooleanOp::Var(name) => *assignments.get(name).unwrap_or(&false),
105            BooleanOp::Const(value) => *value,
106            BooleanOp::Not(inner) => !inner.evaluate(assignments),
107            BooleanOp::And(args) => args.iter().all(|a| a.evaluate(assignments)),
108            BooleanOp::Or(args) => args.iter().any(|a| a.evaluate(assignments)),
109            BooleanOp::Xor(args) => args
110                .iter()
111                .fold(false, |acc, a| acc ^ a.evaluate(assignments)),
112        }
113    }
114}
115
116/// An assignment in a circuit: outputs = expr.
117#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
118pub struct Assignment {
119    /// Output variable names.
120    pub outputs: Vec<String>,
121    /// The expression to evaluate.
122    pub expr: BooleanExpr,
123}
124
125impl Assignment {
126    /// Create a new assignment.
127    pub fn new(outputs: Vec<String>, expr: BooleanExpr) -> Self {
128        Self { outputs, expr }
129    }
130
131    /// Get all variables referenced (both outputs and inputs).
132    pub fn variables(&self) -> Vec<String> {
133        let mut vars = self.outputs.clone();
134        vars.extend(self.expr.variables());
135        vars.sort();
136        vars.dedup();
137        vars
138    }
139
140    /// Check if the assignment is satisfied given variable assignments.
141    pub fn is_satisfied(&self, assignments: &HashMap<String, bool>) -> bool {
142        let result = self.expr.evaluate(assignments);
143        self.outputs
144            .iter()
145            .all(|o| assignments.get(o).copied().unwrap_or(false) == result)
146    }
147}
148
149/// A boolean circuit as a sequence of assignments.
150#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
151pub struct Circuit {
152    /// The assignments in the circuit.
153    pub assignments: Vec<Assignment>,
154}
155
156impl Circuit {
157    /// Create a new circuit from assignments.
158    pub fn new(assignments: Vec<Assignment>) -> Self {
159        Self { assignments }
160    }
161
162    /// Get all variables in the circuit.
163    pub fn variables(&self) -> Vec<String> {
164        let mut vars = Vec::new();
165        for assign in &self.assignments {
166            vars.extend(assign.variables());
167        }
168        vars.sort();
169        vars.dedup();
170        vars
171    }
172
173    /// Get the number of assignments.
174    pub fn num_assignments(&self) -> usize {
175        self.assignments.len()
176    }
177}
178
179/// The Circuit SAT problem.
180///
181/// Given a boolean circuit, find variable assignments that satisfy
182/// as many assignments as possible (or all of them).
183///
184/// # Example
185///
186/// ```
187/// use problemreductions::models::specialized::{CircuitSAT, BooleanExpr, Assignment, Circuit};
188/// use problemreductions::{Problem, Solver, BruteForce};
189///
190/// // Create a simple circuit: c = x AND y
191/// let circuit = Circuit::new(vec![
192///     Assignment::new(
193///         vec!["c".to_string()],
194///         BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")])
195///     ),
196/// ]);
197///
198/// let problem = CircuitSAT::<i32>::new(circuit);
199/// let solver = BruteForce::new();
200/// let solutions = solver.find_best(&problem);
201///
202/// // Multiple satisfying assignments exist
203/// assert!(!solutions.is_empty());
204/// ```
205#[derive(Debug, Clone, Serialize, Deserialize)]
206pub struct CircuitSAT<W = i32> {
207    /// The circuit.
208    circuit: Circuit,
209    /// Variables in order.
210    variables: Vec<String>,
211    /// Weights for each assignment.
212    weights: Vec<W>,
213}
214
215impl<W: Clone + Default + From<i32>> CircuitSAT<W> {
216    /// Create a new CircuitSAT problem with unit weights.
217    pub fn new(circuit: Circuit) -> Self {
218        let variables = circuit.variables();
219        let weights = vec![W::from(1); circuit.num_assignments()];
220        Self {
221            circuit,
222            variables,
223            weights,
224        }
225    }
226}
227
228impl<W> CircuitSAT<W> {
229    /// Create a CircuitSAT problem with custom weights.
230    pub fn with_weights(circuit: Circuit, weights: Vec<W>) -> Self {
231        assert_eq!(weights.len(), circuit.num_assignments());
232        let variables = circuit.variables();
233        Self {
234            circuit,
235            variables,
236            weights,
237        }
238    }
239
240    /// Get the circuit.
241    pub fn circuit(&self) -> &Circuit {
242        &self.circuit
243    }
244
245    /// Get the variable names.
246    pub fn variable_names(&self) -> &[String] {
247        &self.variables
248    }
249
250    /// Convert a configuration to variable assignments.
251    fn config_to_assignments(&self, config: &[usize]) -> HashMap<String, bool> {
252        self.variables
253            .iter()
254            .enumerate()
255            .map(|(i, name)| (name.clone(), config.get(i).copied().unwrap_or(0) == 1))
256            .collect()
257    }
258
259    /// Count how many assignments are satisfied.
260    fn count_satisfied(&self, config: &[usize]) -> usize {
261        let assignments = self.config_to_assignments(config);
262        self.circuit
263            .assignments
264            .iter()
265            .filter(|a| a.is_satisfied(&assignments))
266            .count()
267    }
268}
269
270impl<W> Problem for CircuitSAT<W>
271where
272    W: Clone + Default + PartialOrd + num_traits::Num + num_traits::Zero + std::ops::AddAssign + 'static,
273{
274    const NAME: &'static str = "CircuitSAT";
275    type GraphType = SimpleGraph;
276    type Weight = W;
277    type Size = W;
278
279    fn num_variables(&self) -> usize {
280        self.variables.len()
281    }
282
283    fn num_flavors(&self) -> usize {
284        2 // Binary
285    }
286
287    fn problem_size(&self) -> ProblemSize {
288        ProblemSize::new(vec![
289            ("num_variables", self.variables.len()),
290            ("num_assignments", self.circuit.num_assignments()),
291        ])
292    }
293
294    fn energy_mode(&self) -> EnergyMode {
295        EnergyMode::LargerSizeIsBetter // Maximize satisfied assignments
296    }
297
298    fn solution_size(&self, config: &[usize]) -> SolutionSize<Self::Size> {
299        let assignments = self.config_to_assignments(config);
300        let mut total = W::zero();
301
302        for (i, assign) in self.circuit.assignments.iter().enumerate() {
303            if assign.is_satisfied(&assignments) {
304                total += self.weights[i].clone();
305            }
306        }
307
308        // Valid if all assignments are satisfied
309        let is_valid = self.count_satisfied(config) == self.circuit.num_assignments();
310        SolutionSize::new(total, is_valid)
311    }
312}
313
314/// Check if a circuit assignment is satisfying.
315pub fn is_circuit_satisfying(circuit: &Circuit, assignments: &HashMap<String, bool>) -> bool {
316    circuit
317        .assignments
318        .iter()
319        .all(|a| a.is_satisfied(assignments))
320}
321
322#[cfg(test)]
323mod tests {
324    use super::*;
325    use crate::solvers::{BruteForce, Solver};
326
327    #[test]
328    fn test_boolean_expr_var() {
329        let expr = BooleanExpr::var("x");
330        let mut assignments = HashMap::new();
331        assignments.insert("x".to_string(), true);
332        assert!(expr.evaluate(&assignments));
333
334        assignments.insert("x".to_string(), false);
335        assert!(!expr.evaluate(&assignments));
336    }
337
338    #[test]
339    fn test_boolean_expr_const() {
340        let t = BooleanExpr::constant(true);
341        let f = BooleanExpr::constant(false);
342        let assignments = HashMap::new();
343        assert!(t.evaluate(&assignments));
344        assert!(!f.evaluate(&assignments));
345    }
346
347    #[test]
348    fn test_boolean_expr_not() {
349        let expr = BooleanExpr::not(BooleanExpr::var("x"));
350        let mut assignments = HashMap::new();
351        assignments.insert("x".to_string(), true);
352        assert!(!expr.evaluate(&assignments));
353
354        assignments.insert("x".to_string(), false);
355        assert!(expr.evaluate(&assignments));
356    }
357
358    #[test]
359    fn test_boolean_expr_and() {
360        let expr = BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]);
361        let mut assignments = HashMap::new();
362
363        assignments.insert("x".to_string(), true);
364        assignments.insert("y".to_string(), true);
365        assert!(expr.evaluate(&assignments));
366
367        assignments.insert("y".to_string(), false);
368        assert!(!expr.evaluate(&assignments));
369    }
370
371    #[test]
372    fn test_boolean_expr_or() {
373        let expr = BooleanExpr::or(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]);
374        let mut assignments = HashMap::new();
375
376        assignments.insert("x".to_string(), false);
377        assignments.insert("y".to_string(), false);
378        assert!(!expr.evaluate(&assignments));
379
380        assignments.insert("y".to_string(), true);
381        assert!(expr.evaluate(&assignments));
382    }
383
384    #[test]
385    fn test_boolean_expr_xor() {
386        let expr = BooleanExpr::xor(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]);
387        let mut assignments = HashMap::new();
388
389        assignments.insert("x".to_string(), true);
390        assignments.insert("y".to_string(), true);
391        assert!(!expr.evaluate(&assignments)); // XOR(T, T) = F
392
393        assignments.insert("y".to_string(), false);
394        assert!(expr.evaluate(&assignments)); // XOR(T, F) = T
395    }
396
397    #[test]
398    fn test_boolean_expr_variables() {
399        let expr = BooleanExpr::and(vec![
400            BooleanExpr::var("x"),
401            BooleanExpr::or(vec![BooleanExpr::var("y"), BooleanExpr::var("z")]),
402        ]);
403        let vars = expr.variables();
404        assert_eq!(vars, vec!["x", "y", "z"]);
405    }
406
407    #[test]
408    fn test_assignment_satisfied() {
409        let assign = Assignment::new(
410            vec!["c".to_string()],
411            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
412        );
413
414        let mut assignments = HashMap::new();
415        assignments.insert("x".to_string(), true);
416        assignments.insert("y".to_string(), true);
417        assignments.insert("c".to_string(), true);
418        assert!(assign.is_satisfied(&assignments));
419
420        assignments.insert("c".to_string(), false);
421        assert!(!assign.is_satisfied(&assignments));
422    }
423
424    #[test]
425    fn test_circuit_variables() {
426        let circuit = Circuit::new(vec![
427            Assignment::new(
428                vec!["c".to_string()],
429                BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
430            ),
431            Assignment::new(
432                vec!["d".to_string()],
433                BooleanExpr::or(vec![BooleanExpr::var("c"), BooleanExpr::var("z")]),
434            ),
435        ]);
436        let vars = circuit.variables();
437        assert_eq!(vars, vec!["c", "d", "x", "y", "z"]);
438    }
439
440    #[test]
441    fn test_circuit_sat_creation() {
442        let circuit = Circuit::new(vec![Assignment::new(
443            vec!["c".to_string()],
444            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
445        )]);
446        let problem = CircuitSAT::<i32>::new(circuit);
447        assert_eq!(problem.num_variables(), 3); // c, x, y
448        assert_eq!(problem.num_flavors(), 2);
449    }
450
451    #[test]
452    fn test_circuit_sat_solution_size() {
453        // c = x AND y
454        let circuit = Circuit::new(vec![Assignment::new(
455            vec!["c".to_string()],
456            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
457        )]);
458        let problem = CircuitSAT::<i32>::new(circuit);
459
460        // Variables sorted: c, x, y
461        // c=1, x=1, y=1 -> c = 1 AND 1 = 1, valid
462        let sol = problem.solution_size(&[1, 1, 1]);
463        assert!(sol.is_valid);
464        assert_eq!(sol.size, 1);
465
466        // c=0, x=0, y=0 -> c = 0 AND 0 = 0, valid
467        let sol = problem.solution_size(&[0, 0, 0]);
468        assert!(sol.is_valid);
469        assert_eq!(sol.size, 1);
470
471        // c=1, x=0, y=0 -> c should be 0, but c=1, invalid
472        let sol = problem.solution_size(&[1, 0, 0]);
473        assert!(!sol.is_valid);
474        assert_eq!(sol.size, 0);
475    }
476
477    #[test]
478    fn test_circuit_sat_brute_force() {
479        // c = x AND y
480        let circuit = Circuit::new(vec![Assignment::new(
481            vec!["c".to_string()],
482            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
483        )]);
484        let problem = CircuitSAT::<i32>::new(circuit);
485        let solver = BruteForce::new();
486
487        let solutions = solver.find_best(&problem);
488        // All satisfying: c matches x AND y
489        // 4 valid configs: (0,0,0), (0,0,1), (0,1,0), (1,1,1)
490        assert_eq!(solutions.len(), 4);
491        for sol in &solutions {
492            assert!(problem.solution_size(sol).is_valid);
493        }
494    }
495
496    #[test]
497    fn test_circuit_sat_complex() {
498        // c = x AND y
499        // d = c OR z
500        let circuit = Circuit::new(vec![
501            Assignment::new(
502                vec!["c".to_string()],
503                BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
504            ),
505            Assignment::new(
506                vec!["d".to_string()],
507                BooleanExpr::or(vec![BooleanExpr::var("c"), BooleanExpr::var("z")]),
508            ),
509        ]);
510        let problem = CircuitSAT::<i32>::new(circuit);
511        let solver = BruteForce::new();
512
513        let solutions = solver.find_best(&problem);
514        // All valid solutions satisfy both assignments
515        for sol in &solutions {
516            let sol_size = problem.solution_size(sol);
517            assert!(sol_size.is_valid);
518            assert_eq!(sol_size.size, 2);
519        }
520    }
521
522    #[test]
523    fn test_is_circuit_satisfying() {
524        let circuit = Circuit::new(vec![Assignment::new(
525            vec!["c".to_string()],
526            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
527        )]);
528
529        let mut assignments = HashMap::new();
530        assignments.insert("x".to_string(), true);
531        assignments.insert("y".to_string(), true);
532        assignments.insert("c".to_string(), true);
533        assert!(is_circuit_satisfying(&circuit, &assignments));
534
535        assignments.insert("c".to_string(), false);
536        assert!(!is_circuit_satisfying(&circuit, &assignments));
537    }
538
539    #[test]
540    fn test_problem_size() {
541        let circuit = Circuit::new(vec![
542            Assignment::new(vec!["c".to_string()], BooleanExpr::var("x")),
543            Assignment::new(vec!["d".to_string()], BooleanExpr::var("y")),
544        ]);
545        let problem = CircuitSAT::<i32>::new(circuit);
546        let size = problem.problem_size();
547        assert_eq!(size.get("num_variables"), Some(4));
548        assert_eq!(size.get("num_assignments"), Some(2));
549    }
550
551    #[test]
552    fn test_energy_mode() {
553        let circuit = Circuit::new(vec![]);
554        let problem = CircuitSAT::<i32>::new(circuit);
555        assert!(problem.energy_mode().is_maximization());
556    }
557
558    #[test]
559    fn test_empty_circuit() {
560        let circuit = Circuit::new(vec![]);
561        let problem = CircuitSAT::<i32>::new(circuit);
562        let sol = problem.solution_size(&[]);
563        assert!(sol.is_valid);
564        assert_eq!(sol.size, 0);
565    }
566
567    #[test]
568    fn test_weighted_circuit_sat() {
569        let circuit = Circuit::new(vec![
570            Assignment::new(vec!["c".to_string()], BooleanExpr::var("x")),
571            Assignment::new(vec!["d".to_string()], BooleanExpr::var("y")),
572        ]);
573        let problem = CircuitSAT::with_weights(circuit, vec![10, 1]);
574
575        // Variables sorted: c, d, x, y
576        // Config [1, 0, 1, 0]: c=1, d=0, x=1, y=0
577        // c=x (1=1) satisfied (weight 10), d=y (0=0) satisfied (weight 1)
578        let sol = problem.solution_size(&[1, 0, 1, 0]);
579        assert_eq!(sol.size, 11); // Both satisfied: 10 + 1
580        assert!(sol.is_valid);
581
582        // Config [1, 0, 0, 0]: c=1, d=0, x=0, y=0
583        // c=x (1!=0) not satisfied, d=y (0=0) satisfied (weight 1)
584        let sol = problem.solution_size(&[1, 0, 0, 0]);
585        assert_eq!(sol.size, 1); // Only d=y satisfied
586        assert!(!sol.is_valid);
587
588        // Config [0, 1, 0, 0]: c=0, d=1, x=0, y=0
589        // c=x (0=0) satisfied (weight 10), d=y (1!=0) not satisfied
590        let sol = problem.solution_size(&[0, 1, 0, 0]);
591        assert_eq!(sol.size, 10); // Only c=x satisfied
592        assert!(!sol.is_valid);
593    }
594}
problemreductions/models/specialized/circuit.rs

problemreductions/models/specialized/
circuit.rs
