problemreductions/models/formula/
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::registry::{FieldInfo, ProblemSchemaEntry};
7use crate::traits::{Problem, SatisfactionProblem};
8use serde::{Deserialize, Serialize};
9use std::collections::HashMap;
10
11inventory::submit! {
12    ProblemSchemaEntry {
13        name: "CircuitSAT",
14        module_path: module_path!(),
15        description: "Find satisfying input to a boolean circuit",
16        fields: &[
17            FieldInfo { name: "circuit", type_name: "Circuit", description: "The boolean circuit" },
18        ],
19    }
20}
21
22/// Boolean expression node types.
23#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
24pub enum BooleanOp {
25    /// Variable reference
26    Var(String),
27    /// Boolean constant
28    Const(bool),
29    /// NOT operation
30    Not(Box<BooleanExpr>),
31    /// AND operation
32    And(Vec<BooleanExpr>),
33    /// OR operation
34    Or(Vec<BooleanExpr>),
35    /// XOR operation
36    Xor(Vec<BooleanExpr>),
37}
38
39/// A boolean expression tree.
40#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
41pub struct BooleanExpr {
42    pub op: BooleanOp,
43}
44
45impl BooleanExpr {
46    /// Create a variable reference.
47    pub fn var(name: &str) -> Self {
48        BooleanExpr {
49            op: BooleanOp::Var(name.to_string()),
50        }
51    }
52
53    /// Create a boolean constant.
54    pub fn constant(value: bool) -> Self {
55        BooleanExpr {
56            op: BooleanOp::Const(value),
57        }
58    }
59
60    /// Create a NOT expression.
61    #[allow(clippy::should_implement_trait)]
62    pub fn not(expr: BooleanExpr) -> Self {
63        BooleanExpr {
64            op: BooleanOp::Not(Box::new(expr)),
65        }
66    }
67
68    /// Create an AND expression.
69    pub fn and(args: Vec<BooleanExpr>) -> Self {
70        BooleanExpr {
71            op: BooleanOp::And(args),
72        }
73    }
74
75    /// Create an OR expression.
76    pub fn or(args: Vec<BooleanExpr>) -> Self {
77        BooleanExpr {
78            op: BooleanOp::Or(args),
79        }
80    }
81
82    /// Create an XOR expression.
83    pub fn xor(args: Vec<BooleanExpr>) -> Self {
84        BooleanExpr {
85            op: BooleanOp::Xor(args),
86        }
87    }
88
89    /// Extract all variable names from this expression.
90    pub fn variables(&self) -> Vec<String> {
91        let mut vars = Vec::new();
92        self.extract_variables(&mut vars);
93        vars.sort();
94        vars.dedup();
95        vars
96    }
97
98    fn extract_variables(&self, vars: &mut Vec<String>) {
99        match &self.op {
100            BooleanOp::Var(name) => vars.push(name.clone()),
101            BooleanOp::Const(_) => {}
102            BooleanOp::Not(inner) => inner.extract_variables(vars),
103            BooleanOp::And(args) | BooleanOp::Or(args) | BooleanOp::Xor(args) => {
104                for arg in args {
105                    arg.extract_variables(vars);
106                }
107            }
108        }
109    }
110
111    /// Evaluate the expression given variable assignments.
112    pub fn evaluate(&self, assignments: &HashMap<String, bool>) -> bool {
113        match &self.op {
114            BooleanOp::Var(name) => *assignments.get(name).unwrap_or(&false),
115            BooleanOp::Const(value) => *value,
116            BooleanOp::Not(inner) => !inner.evaluate(assignments),
117            BooleanOp::And(args) => args.iter().all(|a| a.evaluate(assignments)),
118            BooleanOp::Or(args) => args.iter().any(|a| a.evaluate(assignments)),
119            BooleanOp::Xor(args) => args
120                .iter()
121                .fold(false, |acc, a| acc ^ a.evaluate(assignments)),
122        }
123    }
124}
125
126/// An assignment in a circuit: outputs = expr.
127#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
128pub struct Assignment {
129    /// Output variable names.
130    pub outputs: Vec<String>,
131    /// The expression to evaluate.
132    pub expr: BooleanExpr,
133}
134
135impl Assignment {
136    /// Create a new assignment.
137    pub fn new(outputs: Vec<String>, expr: BooleanExpr) -> Self {
138        Self { outputs, expr }
139    }
140
141    /// Get all variables referenced (both outputs and inputs).
142    pub fn variables(&self) -> Vec<String> {
143        let mut vars = self.outputs.clone();
144        vars.extend(self.expr.variables());
145        vars.sort();
146        vars.dedup();
147        vars
148    }
149
150    /// Check if the assignment is satisfied given variable assignments.
151    pub fn is_satisfied(&self, assignments: &HashMap<String, bool>) -> bool {
152        let result = self.expr.evaluate(assignments);
153        self.outputs
154            .iter()
155            .all(|o| assignments.get(o).copied().unwrap_or(false) == result)
156    }
157}
158
159/// A boolean circuit as a sequence of assignments.
160#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
161pub struct Circuit {
162    /// The assignments in the circuit.
163    pub assignments: Vec<Assignment>,
164}
165
166impl Circuit {
167    /// Create a new circuit from assignments.
168    pub fn new(assignments: Vec<Assignment>) -> Self {
169        Self { assignments }
170    }
171
172    /// Get all variables in the circuit.
173    pub fn variables(&self) -> Vec<String> {
174        let mut vars = Vec::new();
175        for assign in &self.assignments {
176            vars.extend(assign.variables());
177        }
178        vars.sort();
179        vars.dedup();
180        vars
181    }
182
183    /// Get the number of assignments.
184    pub fn num_assignments(&self) -> usize {
185        self.assignments.len()
186    }
187}
188
189/// The Circuit SAT problem.
190///
191/// Given a boolean circuit, find variable assignments that satisfy
192/// all circuit constraints.
193///
194/// # Example
195///
196/// ```
197/// use problemreductions::models::formula::{CircuitSAT, BooleanExpr, Assignment, Circuit};
198/// use problemreductions::{Problem, Solver, BruteForce};
199///
200/// // Create a simple circuit: c = x AND y
201/// let circuit = Circuit::new(vec![
202///     Assignment::new(
203///         vec!["c".to_string()],
204///         BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")])
205///     ),
206/// ]);
207///
208/// let problem = CircuitSAT::new(circuit);
209/// let solver = BruteForce::new();
210/// let solutions = solver.find_all_satisfying(&problem);
211///
212/// // Multiple satisfying assignments exist
213/// assert!(!solutions.is_empty());
214/// ```
215#[derive(Debug, Clone, Serialize, Deserialize)]
216pub struct CircuitSAT {
217    /// The circuit.
218    circuit: Circuit,
219    /// Variables in order.
220    variables: Vec<String>,
221}
222
223impl CircuitSAT {
224    /// Create a new CircuitSAT problem.
225    pub fn new(circuit: Circuit) -> Self {
226        let variables = circuit.variables();
227        Self { circuit, variables }
228    }
229
230    /// Get the circuit.
231    pub fn circuit(&self) -> &Circuit {
232        &self.circuit
233    }
234
235    /// Get the variable names.
236    pub fn variable_names(&self) -> &[String] {
237        &self.variables
238    }
239
240    /// Get the number of variables in the circuit.
241    pub fn num_variables(&self) -> usize {
242        self.variables.len()
243    }
244
245    /// Get the number of assignments (constraints) in the circuit.
246    pub fn num_assignments(&self) -> usize {
247        self.circuit.num_assignments()
248    }
249
250    /// Check if a configuration is a valid satisfying assignment.
251    pub fn is_valid_solution(&self, config: &[usize]) -> bool {
252        self.count_satisfied(config) == self.circuit.num_assignments()
253    }
254
255    /// Convert a configuration to variable assignments.
256    fn config_to_assignments(&self, config: &[usize]) -> HashMap<String, bool> {
257        self.variables
258            .iter()
259            .enumerate()
260            .map(|(i, name)| (name.clone(), config.get(i).copied().unwrap_or(0) == 1))
261            .collect()
262    }
263
264    /// Count how many assignments are satisfied.
265    fn count_satisfied(&self, config: &[usize]) -> usize {
266        let assignments = self.config_to_assignments(config);
267        self.circuit
268            .assignments
269            .iter()
270            .filter(|a| a.is_satisfied(&assignments))
271            .count()
272    }
273}
274
275/// Check if a circuit assignment is satisfying.
276#[cfg(test)]
277pub(crate) fn is_circuit_satisfying(
278    circuit: &Circuit,
279    assignments: &HashMap<String, bool>,
280) -> bool {
281    circuit
282        .assignments
283        .iter()
284        .all(|a| a.is_satisfied(assignments))
285}
286
287impl Problem for CircuitSAT {
288    const NAME: &'static str = "CircuitSAT";
289    type Metric = bool;
290
291    fn dims(&self) -> Vec<usize> {
292        vec![2; self.variables.len()]
293    }
294
295    fn evaluate(&self, config: &[usize]) -> bool {
296        self.count_satisfied(config) == self.circuit.num_assignments()
297    }
298
299    fn variant() -> Vec<(&'static str, &'static str)> {
300        crate::variant_params![]
301    }
302}
303
304impl SatisfactionProblem for CircuitSAT {}
305
306crate::declare_variants! {
307    CircuitSAT => "2^num_variables",
308}
309
310#[cfg(test)]
311#[path = "../../unit_tests/models/formula/circuit.rs"]
312mod tests;
problemreductions/models/formula/circuit.rs

problemreductions/models/formula/
circuit.rs
