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;
8use serde::{Deserialize, Serialize};
9use std::collections::HashMap;
10
11inventory::submit! {
12    ProblemSchemaEntry {
13        name: "CircuitSAT",
14        display_name: "Circuit SAT",
15        aliases: &[],
16        dimensions: &[],
17        category: crate::registry::ProblemCategory::Formula,
18        module_path: module_path!(),
19        description: "Find satisfying input to a boolean circuit",
20        fields: &[
21            FieldInfo { name: "circuit", type_name: "Circuit", description: "The boolean circuit" },
22        ],
23    }
24}
25
26/// Boolean expression node types.
27#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
28pub enum BooleanOp {
29    /// Variable reference
30    Var(String),
31    /// Boolean constant
32    Const(bool),
33    /// NOT operation
34    Not(Box<BooleanExpr>),
35    /// AND operation
36    And(Vec<BooleanExpr>),
37    /// OR operation
38    Or(Vec<BooleanExpr>),
39    /// XOR operation
40    Xor(Vec<BooleanExpr>),
41}
42
43/// A boolean expression tree.
44#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
45pub struct BooleanExpr {
46    pub op: BooleanOp,
47}
48
49impl BooleanExpr {
50    /// Create a variable reference.
51    pub fn var(name: &str) -> Self {
52        BooleanExpr {
53            op: BooleanOp::Var(name.to_string()),
54        }
55    }
56
57    /// Create a boolean constant.
58    pub fn constant(value: bool) -> Self {
59        BooleanExpr {
60            op: BooleanOp::Const(value),
61        }
62    }
63
64    /// Create a NOT expression.
65    #[allow(clippy::should_implement_trait)]
66    pub fn not(expr: BooleanExpr) -> Self {
67        BooleanExpr {
68            op: BooleanOp::Not(Box::new(expr)),
69        }
70    }
71
72    /// Create an AND expression.
73    pub fn and(args: Vec<BooleanExpr>) -> Self {
74        BooleanExpr {
75            op: BooleanOp::And(args),
76        }
77    }
78
79    /// Create an OR expression.
80    pub fn or(args: Vec<BooleanExpr>) -> Self {
81        BooleanExpr {
82            op: BooleanOp::Or(args),
83        }
84    }
85
86    /// Create an XOR expression.
87    pub fn xor(args: Vec<BooleanExpr>) -> Self {
88        BooleanExpr {
89            op: BooleanOp::Xor(args),
90        }
91    }
92
93    /// Extract all variable names from this expression.
94    pub fn variables(&self) -> Vec<String> {
95        let mut vars = Vec::new();
96        self.extract_variables(&mut vars);
97        vars.sort();
98        vars.dedup();
99        vars
100    }
101
102    fn extract_variables(&self, vars: &mut Vec<String>) {
103        match &self.op {
104            BooleanOp::Var(name) => vars.push(name.clone()),
105            BooleanOp::Const(_) => {}
106            BooleanOp::Not(inner) => inner.extract_variables(vars),
107            BooleanOp::And(args) | BooleanOp::Or(args) | BooleanOp::Xor(args) => {
108                for arg in args {
109                    arg.extract_variables(vars);
110                }
111            }
112        }
113    }
114
115    /// Return the number of nodes in this expression tree.
116    pub fn num_nodes(&self) -> usize {
117        match &self.op {
118            BooleanOp::Var(_) | BooleanOp::Const(_) => 1,
119            BooleanOp::Not(inner) => 1 + inner.num_nodes(),
120            BooleanOp::And(args) | BooleanOp::Or(args) | BooleanOp::Xor(args) => {
121                1 + args.iter().map(BooleanExpr::num_nodes).sum::<usize>()
122            }
123        }
124    }
125
126    /// Evaluate the expression given variable assignments.
127    pub fn evaluate(&self, assignments: &HashMap<String, bool>) -> bool {
128        match &self.op {
129            BooleanOp::Var(name) => *assignments.get(name).unwrap_or(&false),
130            BooleanOp::Const(value) => *value,
131            BooleanOp::Not(inner) => !inner.evaluate(assignments),
132            BooleanOp::And(args) => args.iter().all(|a| a.evaluate(assignments)),
133            BooleanOp::Or(args) => args.iter().any(|a| a.evaluate(assignments)),
134            BooleanOp::Xor(args) => args
135                .iter()
136                .fold(false, |acc, a| acc ^ a.evaluate(assignments)),
137        }
138    }
139}
140
141/// An assignment in a circuit: outputs = expr.
142#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
143pub struct Assignment {
144    /// Output variable names.
145    pub outputs: Vec<String>,
146    /// The expression to evaluate.
147    pub expr: BooleanExpr,
148}
149
150impl Assignment {
151    /// Create a new assignment.
152    pub fn new(outputs: Vec<String>, expr: BooleanExpr) -> Self {
153        Self { outputs, expr }
154    }
155
156    /// Get all variables referenced (both outputs and inputs).
157    pub fn variables(&self) -> Vec<String> {
158        let mut vars = self.outputs.clone();
159        vars.extend(self.expr.variables());
160        vars.sort();
161        vars.dedup();
162        vars
163    }
164
165    /// Check if the assignment is satisfied given variable assignments.
166    pub fn is_satisfied(&self, assignments: &HashMap<String, bool>) -> bool {
167        let result = self.expr.evaluate(assignments);
168        self.outputs
169            .iter()
170            .all(|o| assignments.get(o).copied().unwrap_or(false) == result)
171    }
172}
173
174/// A boolean circuit as a sequence of assignments.
175#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
176pub struct Circuit {
177    /// The assignments in the circuit.
178    pub assignments: Vec<Assignment>,
179}
180
181impl Circuit {
182    /// Create a new circuit from assignments.
183    pub fn new(assignments: Vec<Assignment>) -> Self {
184        Self { assignments }
185    }
186
187    /// Get all variables in the circuit.
188    pub fn variables(&self) -> Vec<String> {
189        let mut vars = Vec::new();
190        for assign in &self.assignments {
191            vars.extend(assign.variables());
192        }
193        vars.sort();
194        vars.dedup();
195        vars
196    }
197
198    /// Get the number of assignments.
199    pub fn num_assignments(&self) -> usize {
200        self.assignments.len()
201    }
202
203    /// Return the total number of Boolean expression nodes.
204    pub fn num_expression_nodes(&self) -> usize {
205        self.assignments
206            .iter()
207            .map(|assignment| assignment.expr.num_nodes())
208            .sum()
209    }
210
211    /// Return the total number of assignment outputs.
212    pub fn num_assignment_outputs(&self) -> usize {
213        self.assignments
214            .iter()
215            .map(|assignment| assignment.outputs.len())
216            .sum()
217    }
218}
219
220/// The Circuit SAT problem.
221///
222/// Given a boolean circuit, find variable assignments that satisfy
223/// all circuit constraints.
224///
225/// # Example
226///
227/// ```
228/// use problemreductions::models::formula::{CircuitSAT, BooleanExpr, Assignment, Circuit};
229/// use problemreductions::{Problem, BruteForce};
230///
231/// // Create a simple circuit: c = x AND y
232/// let circuit = Circuit::new(vec![
233///     Assignment::new(
234///         vec!["c".to_string()],
235///         BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")])
236///     ),
237/// ]);
238///
239/// let problem = CircuitSAT::new(circuit);
240/// let solver = BruteForce::new();
241/// let solutions = solver.find_all_witnesses(&problem).unwrap();
242///
243/// // Multiple satisfying assignments exist
244/// assert!(!solutions.is_empty());
245/// ```
246#[derive(Debug, Clone, Serialize, Deserialize)]
247pub struct CircuitSAT {
248    /// The circuit.
249    circuit: Circuit,
250    /// Variables in order.
251    variables: Vec<String>,
252}
253
254impl CircuitSAT {
255    /// Create a new CircuitSAT problem.
256    pub fn new(circuit: Circuit) -> Self {
257        let variables = circuit.variables();
258        Self { circuit, variables }
259    }
260
261    /// Get the circuit.
262    pub fn circuit(&self) -> &Circuit {
263        &self.circuit
264    }
265
266    /// Get the variable names.
267    pub fn variable_names(&self) -> &[String] {
268        &self.variables
269    }
270
271    /// Get the number of variables in the circuit.
272    pub fn num_variables(&self) -> usize {
273        self.variables.len()
274    }
275
276    /// Get the number of assignments (constraints) in the circuit.
277    pub fn num_assignments(&self) -> usize {
278        self.circuit.num_assignments()
279    }
280
281    /// Return the total number of Boolean expression nodes.
282    pub fn num_expression_nodes(&self) -> usize {
283        self.circuit.num_expression_nodes()
284    }
285
286    /// Return the total number of assignment outputs.
287    pub fn num_assignment_outputs(&self) -> usize {
288        self.circuit.num_assignment_outputs()
289    }
290
291    /// Check if a configuration is a valid satisfying assignment.
292    pub fn is_valid_solution(
293        &self,
294        config: &[bool],
295    ) -> Result<bool, crate::traits::EvaluationError> {
296        if config.len() != self.variables.len() {
297            return Err(crate::traits::EvaluationError::InvalidConfiguration(
298                "assignment length does not match the circuit variables".into(),
299            ));
300        }
301        Ok(self.count_satisfied(config) == self.circuit.num_assignments())
302    }
303
304    /// Convert a configuration to variable assignments.
305    fn config_to_assignments(&self, config: &[bool]) -> HashMap<String, bool> {
306        self.variables
307            .iter()
308            .enumerate()
309            .map(|(i, name)| (name.clone(), config[i]))
310            .collect()
311    }
312
313    /// Count how many assignments are satisfied.
314    fn count_satisfied(&self, config: &[bool]) -> usize {
315        let assignments = self.config_to_assignments(config);
316        self.circuit
317            .assignments
318            .iter()
319            .filter(|a| a.is_satisfied(&assignments))
320            .count()
321    }
322}
323
324/// Check if a circuit assignment is satisfying.
325#[cfg(test)]
326pub(crate) fn is_circuit_satisfying(
327    circuit: &Circuit,
328    assignments: &HashMap<String, bool>,
329) -> bool {
330    circuit
331        .assignments
332        .iter()
333        .all(|a| a.is_satisfied(assignments))
334}
335
336impl Problem for CircuitSAT {
337    const NAME: &'static str = "CircuitSAT";
338    type Solution = Vec<bool>;
339    type Value = crate::types::Or;
340
341    crate::problem_parameters![
342        ("num_assignment_outputs", num_assignment_outputs),
343        ("num_assignments", num_assignments),
344        ("num_expression_nodes", num_expression_nodes),
345        ("num_variables", num_variables),
346    ];
347
348    fn evaluate(
349        &self,
350        config: &Self::Solution,
351    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
352        Ok(crate::types::Or(self.is_valid_solution(config)?))
353    }
354
355    fn variant() -> Vec<(&'static str, &'static str)> {
356        crate::variant_params![]
357    }
358}
359
360impl crate::solvers::BruteForceProblem for CircuitSAT {
361    fn dimensions(&self) -> Vec<usize> {
362        vec![2; self.variables.len()]
363    }
364}
365
366crate::declare_variants! {
367    default CircuitSAT => "2^num_variables",
368}
369
370crate::register_brute_force! {
371    CircuitSAT decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
372}
373
374#[cfg(feature = "example-db")]
375pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
376    vec![crate::example_db::specs::ModelExampleSpec {
377        id: "circuit_sat",
378        instance: Box::new(CircuitSAT::new(Circuit::new(vec![
379            Assignment::new(
380                vec!["a".to_string()],
381                BooleanExpr::and(vec![BooleanExpr::var("x1"), BooleanExpr::var("x2")]),
382            ),
383            Assignment::new(
384                vec!["b".to_string()],
385                BooleanExpr::or(vec![BooleanExpr::var("x1"), BooleanExpr::var("x2")]),
386            ),
387            Assignment::new(
388                vec!["c".to_string()],
389                BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
390            ),
391        ]))),
392        optimal_config: serde_json::json!(vec![false, false, false, false, false]),
393        optimal_value: serde_json::json!(true),
394    }]
395}
396
397#[cfg(test)]
398#[path = "../../unit_tests/models/formula/circuit.rs"]
399mod tests;
problemreductions/models/formula/circuit.rs

problemreductions/models/formula/
circuit.rs
