problemreductions/rules/
circuit_sat.rs

1//! Reduction from CircuitSAT to Satisfiability via Tseitin encoding.
2
3use crate::models::formula::{
4    Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability,
5};
6use crate::reduction;
7use crate::rules::traits::{ReduceTo, ReductionResult};
8use std::collections::HashMap;
9
10#[derive(Debug, Clone, PartialEq, Eq)]
11enum NormalizedExpr {
12    Var(String),
13    Const(bool),
14    Not(Box<NormalizedExpr>),
15    And(Box<NormalizedExpr>, Box<NormalizedExpr>),
16    Or(Box<NormalizedExpr>, Box<NormalizedExpr>),
17    Xor(Box<NormalizedExpr>, Box<NormalizedExpr>),
18}
19
20#[derive(Debug, Clone, Copy, PartialEq, Eq)]
21enum EncodedTerm {
22    Const(bool),
23    Var(i32),
24}
25
26#[derive(Debug, Clone)]
27struct TseitinEncoding {
28    num_vars: usize,
29    clauses: Vec<CNFClause>,
30}
31
32#[derive(Debug)]
33struct TseitinEncoder {
34    source_var_ids: HashMap<String, i32>,
35    clauses: Vec<CNFClause>,
36    next_var: i32,
37}
38
39impl TseitinEncoder {
40    fn new(source: &CircuitSAT) -> Self {
41        let source_var_ids = source
42            .variable_names()
43            .iter()
44            .enumerate()
45            .map(|(index, name)| (name.clone(), index as i32 + 1))
46            .collect();
47        Self {
48            source_var_ids,
49            clauses: Vec::new(),
50            next_var: source.num_variables() as i32 + 1,
51        }
52    }
53
54    fn encode_problem(mut self, source: &CircuitSAT) -> TseitinEncoding {
55        for assignment in &source.circuit().assignments {
56            self.encode_assignment(assignment);
57        }
58
59        TseitinEncoding {
60            num_vars: (self.next_var - 1) as usize,
61            clauses: self.clauses,
62        }
63    }
64
65    fn encode_assignment(&mut self, assignment: &Assignment) {
66        if assignment.outputs.is_empty() {
67            return;
68        }
69
70        let root = self.encode_expr(&normalize_expr(&assignment.expr));
71        match root {
72            EncodedTerm::Const(value) => {
73                let literal_sign = if value { 1 } else { -1 };
74                for output in &assignment.outputs {
75                    let output_var = self.source_var(output);
76                    self.push_clause(vec![literal_sign * output_var]);
77                }
78            }
79            EncodedTerm::Var(root_var) => {
80                for output in &assignment.outputs {
81                    let output_var = self.source_var(output);
82                    self.push_equivalence(output_var, root_var);
83                }
84            }
85        }
86    }
87
88    fn encode_expr(&mut self, expr: &NormalizedExpr) -> EncodedTerm {
89        match expr {
90            NormalizedExpr::Var(name) => EncodedTerm::Var(self.source_var(name)),
91            NormalizedExpr::Const(value) => EncodedTerm::Const(*value),
92            NormalizedExpr::Not(inner) => match self.encode_expr(inner) {
93                EncodedTerm::Const(value) => EncodedTerm::Const(!value),
94                EncodedTerm::Var(child_var) => {
95                    let gate_var = self.allocate_auxiliary_var();
96                    self.push_clause(vec![-gate_var, -child_var]);
97                    self.push_clause(vec![gate_var, child_var]);
98                    EncodedTerm::Var(gate_var)
99                }
100            },
101            NormalizedExpr::And(left, right) => {
102                let left_term = self.encode_expr(left);
103                let right_term = self.encode_expr(right);
104                let left_var = self.expect_var(left_term, "AND left input");
105                let right_var = self.expect_var(right_term, "AND right input");
106                let gate_var = self.allocate_auxiliary_var();
107                self.push_clause(vec![-gate_var, left_var]);
108                self.push_clause(vec![-gate_var, right_var]);
109                self.push_clause(vec![gate_var, -left_var, -right_var]);
110                EncodedTerm::Var(gate_var)
111            }
112            NormalizedExpr::Or(left, right) => {
113                let left_term = self.encode_expr(left);
114                let right_term = self.encode_expr(right);
115                let left_var = self.expect_var(left_term, "OR left input");
116                let right_var = self.expect_var(right_term, "OR right input");
117                let gate_var = self.allocate_auxiliary_var();
118                self.push_clause(vec![gate_var, -left_var]);
119                self.push_clause(vec![gate_var, -right_var]);
120                self.push_clause(vec![-gate_var, left_var, right_var]);
121                EncodedTerm::Var(gate_var)
122            }
123            NormalizedExpr::Xor(left, right) => {
124                let left_term = self.encode_expr(left);
125                let right_term = self.encode_expr(right);
126                let left_var = self.expect_var(left_term, "XOR left input");
127                let right_var = self.expect_var(right_term, "XOR right input");
128                let gate_var = self.allocate_auxiliary_var();
129                self.push_clause(vec![-left_var, -right_var, -gate_var]);
130                self.push_clause(vec![left_var, right_var, -gate_var]);
131                self.push_clause(vec![left_var, -right_var, gate_var]);
132                self.push_clause(vec![-left_var, right_var, gate_var]);
133                EncodedTerm::Var(gate_var)
134            }
135        }
136    }
137
138    fn expect_var(&self, term: EncodedTerm, context: &str) -> i32 {
139        match term {
140            EncodedTerm::Var(var) => var,
141            EncodedTerm::Const(_) => {
142                panic!("normalized Tseitin encoding produced a constant for {context}")
143            }
144        }
145    }
146
147    fn source_var(&self, name: &str) -> i32 {
148        *self
149            .source_var_ids
150            .get(name)
151            .unwrap_or_else(|| panic!("CircuitSAT variable {name:?} missing from source ordering"))
152    }
153
154    fn allocate_auxiliary_var(&mut self) -> i32 {
155        let var = self.next_var;
156        self.next_var += 1;
157        var
158    }
159
160    fn push_equivalence(&mut self, left: i32, right: i32) {
161        self.push_clause(vec![-left, right]);
162        self.push_clause(vec![left, -right]);
163    }
164
165    fn push_clause(&mut self, literals: Vec<i32>) {
166        self.clauses.push(CNFClause::new(literals));
167    }
168}
169
170fn make_and(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
171    NormalizedExpr::And(Box::new(left), Box::new(right))
172}
173
174fn make_or(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
175    NormalizedExpr::Or(Box::new(left), Box::new(right))
176}
177
178fn make_xor(left: NormalizedExpr, right: NormalizedExpr) -> NormalizedExpr {
179    NormalizedExpr::Xor(Box::new(left), Box::new(right))
180}
181
182fn build_balanced_expr(
183    mut items: Vec<NormalizedExpr>,
184    combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr,
185) -> NormalizedExpr {
186    if items.len() == 1 {
187        return items.pop().expect("single item exists");
188    }
189
190    let right = items.split_off(items.len() / 2);
191    combine(
192        build_balanced_expr(items, combine),
193        build_balanced_expr(right, combine),
194    )
195}
196
197fn normalize_expr(expr: &BooleanExpr) -> NormalizedExpr {
198    match &expr.op {
199        BooleanOp::Var(name) => NormalizedExpr::Var(name.clone()),
200        BooleanOp::Const(value) => NormalizedExpr::Const(*value),
201        BooleanOp::Not(inner) => match normalize_expr(inner) {
202            NormalizedExpr::Const(value) => NormalizedExpr::Const(!value),
203            NormalizedExpr::Not(grandchild) => *grandchild,
204            normalized => NormalizedExpr::Not(Box::new(normalized)),
205        },
206        BooleanOp::And(args) => normalize_nary_gate(args, false, true, make_and),
207        BooleanOp::Or(args) => normalize_nary_gate(args, true, false, make_or),
208        BooleanOp::Xor(args) => {
209            let mut parity = false;
210            let mut normalized_args = Vec::new();
211
212            for arg in args {
213                match normalize_expr(arg) {
214                    NormalizedExpr::Const(value) => parity ^= value,
215                    normalized => normalized_args.push(normalized),
216                }
217            }
218
219            match normalized_args.len() {
220                0 => NormalizedExpr::Const(parity),
221                1 => {
222                    let base = normalized_args.pop().expect("single item exists");
223                    if parity {
224                        NormalizedExpr::Not(Box::new(base))
225                    } else {
226                        base
227                    }
228                }
229                _ => {
230                    let base = build_balanced_expr(normalized_args, make_xor);
231                    if parity {
232                        NormalizedExpr::Not(Box::new(base))
233                    } else {
234                        base
235                    }
236                }
237            }
238        }
239    }
240}
241
242fn normalize_nary_gate(
243    args: &[BooleanExpr],
244    absorbing_value: bool,
245    identity_value: bool,
246    combine: fn(NormalizedExpr, NormalizedExpr) -> NormalizedExpr,
247) -> NormalizedExpr {
248    let mut normalized_args = Vec::new();
249
250    for arg in args {
251        match normalize_expr(arg) {
252            NormalizedExpr::Const(value) if value == absorbing_value => {
253                return NormalizedExpr::Const(absorbing_value)
254            }
255            NormalizedExpr::Const(value) if value == identity_value => {}
256            normalized => normalized_args.push(normalized),
257        }
258    }
259
260    match normalized_args.len() {
261        0 => NormalizedExpr::Const(identity_value),
262        1 => normalized_args.pop().expect("single item exists"),
263        _ => build_balanced_expr(normalized_args, combine),
264    }
265}
266
267fn build_tseitin_encoding(source: &CircuitSAT) -> TseitinEncoding {
268    TseitinEncoder::new(source).encode_problem(source)
269}
270
271impl CircuitSAT {
272    pub fn tseitin_num_vars(&self) -> usize {
273        build_tseitin_encoding(self).num_vars
274    }
275
276    pub fn tseitin_num_clauses(&self) -> usize {
277        build_tseitin_encoding(self).clauses.len()
278    }
279}
280
281/// Result of reducing CircuitSAT to SAT.
282#[derive(Debug, Clone)]
283pub struct ReductionCircuitSATToSAT {
284    target: Satisfiability,
285    source_var_count: usize,
286}
287
288impl ReductionResult for ReductionCircuitSATToSAT {
289    type Source = CircuitSAT;
290    type Target = Satisfiability;
291
292    fn target_problem(&self) -> &Self::Target {
293        &self.target
294    }
295
296    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
297        target_solution
298            .iter()
299            .take(self.source_var_count)
300            .copied()
301            .collect()
302    }
303}
304
305#[reduction(
306    overhead = {
307        num_vars = "tseitin_num_vars",
308        num_clauses = "tseitin_num_clauses",
309    }
310)]
311impl ReduceTo<Satisfiability> for CircuitSAT {
312    type Result = ReductionCircuitSATToSAT;
313
314    fn reduce_to(&self) -> Self::Result {
315        let encoding = build_tseitin_encoding(self);
316        ReductionCircuitSATToSAT {
317            target: Satisfiability::new(encoding.num_vars, encoding.clauses),
318            source_var_count: self.num_variables(),
319        }
320    }
321}
322
323#[cfg(any(test, feature = "example-db"))]
324fn issue_example_source() -> CircuitSAT {
325    use crate::models::formula::Circuit;
326
327    CircuitSAT::new(Circuit::new(vec![Assignment::new(
328        vec!["r".to_string()],
329        BooleanExpr::or(vec![
330            BooleanExpr::and(vec![BooleanExpr::var("x1"), BooleanExpr::var("x2")]),
331            BooleanExpr::and(vec![
332                BooleanExpr::not(BooleanExpr::var("x3")),
333                BooleanExpr::var("x4"),
334            ]),
335        ]),
336    )]))
337}
338
339#[cfg(feature = "example-db")]
340pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
341    use crate::export::SolutionPair;
342    use crate::solvers::BruteForce;
343
344    vec![crate::example_db::specs::RuleExampleSpec {
345        id: "circuitsat_to_satisfiability",
346        build: || {
347            let source = issue_example_source();
348            let source_config = vec![1, 1, 1, 0, 1];
349            let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
350            let target_config = BruteForce::new()
351                .find_all_witnesses(reduction.target_problem())
352                .into_iter()
353                .find(|candidate| reduction.extract_solution(candidate) == source_config)
354                .expect("canonical CircuitSAT -> Satisfiability example must be satisfiable");
355
356            crate::example_db::specs::assemble_rule_example(
357                &source,
358                reduction.target_problem(),
359                vec![SolutionPair {
360                    source_config,
361                    target_config,
362                }],
363            )
364        },
365    }]
366}
367
368#[cfg(test)]
369#[path = "../unit_tests/rules/circuit_sat.rs"]
370mod tests;
problemreductions/rules/circuit_sat.rs

problemreductions/rules/
circuit_sat.rs
