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

problemreductions/models/formula/
circuit.rs
