boolean_circuit/
cnf.rs

1use std::{collections::HashMap, iter, rc::Rc};
2
3use crate::{Gate, Literal, Operation};
4
5/// Turns the circuit represented by the ouput gate `gate` into a conjunctive normal form (CNF) formula.
6///
7/// The function uses the Tseitin transformation, so it needs a way to generate new unique variables,
8/// which is done by the function `new_var`.
9///
10/// Parameters
11/// * `gate`: The output gate of the circuit.
12/// * `new_var`: A function that can be used to generate new unique variable names. Each call has to return
13///   a new variable name not returned before and not used in the circuit.
14///
15/// Returns an iterator over the clauses of the CNF formula. Each clause is a vector of literals.
16pub fn generate_cnf<'a>(
17    gate: &'a Gate,
18    new_var: &mut impl FnMut() -> String,
19) -> impl Iterator<Item = Vec<Literal>> + 'a {
20    // We start by generating a variable / literal for each gate.
21    let lit_for_gate_id: HashMap<_, _> = gate
22        .iter()
23        .map(|n| {
24            let var = match n.operation() {
25                Operation::Variable(name) => Literal::Pos(name.clone()),
26                _ => Literal::Pos(Rc::new(new_var())),
27            };
28            (n.id(), var)
29        })
30        .collect();
31    let lit_for_gate = move |gate: &Gate| lit_for_gate_id[&gate.id()].clone();
32    let output_var = lit_for_gate(gate);
33    // Now we iterate over the gates and generate the required clauses for each gate.
34    gate.into_iter()
35        .flat_map(move |n| {
36            let var = lit_for_gate(n);
37            match n.operation() {
38                Operation::Variable(_) => vec![],
39                Operation::Constant(true) => vec![vec![var]],
40                Operation::Constant(false) => vec![vec![!&var]],
41                Operation::Conjunction(left, right) => {
42                    let left_var = lit_for_gate(left);
43                    let right_var = lit_for_gate(right);
44                    vec![
45                        vec![!&left_var, !&right_var, var.clone()],
46                        vec![left_var.clone(), !&var],
47                        vec![right_var.clone(), !&var],
48                    ]
49                }
50                Operation::Disjunction(left, right) => {
51                    let left_var = lit_for_gate(left);
52                    let right_var = lit_for_gate(right);
53                    vec![
54                        vec![left_var.clone(), right_var.clone(), !&var],
55                        vec![!&left_var, var.clone()],
56                        vec![!&right_var, var.clone()],
57                    ]
58                }
59                Operation::Xor(left, right) => {
60                    let left_var = lit_for_gate(left);
61                    let right_var = lit_for_gate(right);
62                    vec![
63                        vec![left_var.clone(), right_var.clone(), !&var],
64                        vec![left_var.clone(), !&right_var, var.clone()],
65                        vec![!&left_var, right_var.clone(), var.clone()],
66                        vec![!&left_var, !&right_var, !&var],
67                    ]
68                }
69                Operation::Negation(inner) => {
70                    let inner_var = lit_for_gate(inner);
71                    vec![
72                        vec![inner_var.clone(), var.clone()],
73                        vec![!&inner_var, !&var],
74                    ]
75                }
76            }
77        })
78        // Finally, we add the output variable as its own clause.
79        .chain(iter::once(vec![output_var]))
80}
81
82#[cfg(test)]
83mod test {
84    use itertools::Itertools;
85
86    use super::*;
87
88    #[derive(Default)]
89    struct VarGen {
90        counter: u32,
91    }
92
93    impl VarGen {
94        fn next(&mut self) -> String {
95            let name = format!("x{}", self.counter);
96            self.counter += 1;
97            name
98        }
99    }
100
101    fn to_cnf_string(gate: &Gate, new_var: &mut impl FnMut() -> String) -> String {
102        generate_cnf(gate, new_var)
103            .map(|clause| format!("({})", clause.iter().format(" \\/ ")))
104            .format(" /\\ ")
105            .to_string()
106    }
107
108    #[test]
109    fn test_to_cnf() {
110        let mut var_gen = VarGen::default();
111        let mut new_var = || var_gen.next();
112        let gate = Gate::from("a");
113        assert_eq!(to_cnf_string(&gate, &mut new_var), "(a)".to_string());
114    }
115
116    #[test]
117    fn test_to_cnf_conjunction() {
118        let mut var_gen = VarGen::default();
119        let mut new_var = || var_gen.next();
120        let gate = Gate::from("a") & Gate::from("b");
121        assert_eq!(
122            to_cnf_string(&gate, &mut new_var),
123            "(-a \\/ -b \\/ x0) /\\ (a \\/ -x0) /\\ (b \\/ -x0) /\\ (x0)".to_string()
124        );
125    }
126
127    #[test]
128    fn test_to_cnf_disjunction() {
129        let mut var_gen = VarGen::default();
130        let mut new_var = || var_gen.next();
131        let gate = Gate::from("a") | Gate::from("b");
132        assert_eq!(
133            to_cnf_string(&gate, &mut new_var),
134            "(a \\/ b \\/ -x0) /\\ (-a \\/ x0) /\\ (-b \\/ x0) /\\ (x0)".to_string()
135        );
136    }
137
138    #[test]
139    fn test_clause_reuse() {
140        let mut var_gen = VarGen::default();
141        let mut new_var = || var_gen.next();
142        let v = Gate::from("a");
143        let x = v.clone() | v;
144        let y = x.clone() & (!x);
145        assert_eq!(
146            to_cnf_string(&y, &mut new_var),
147            "(-x1 \\/ -x2 \\/ x0) /\\ (x1 \\/ -x0) /\\ (x2 \\/ -x0) /\\ (a \\/ a \\/ -x1) /\\ (-a \\/ x1) /\\ (-a \\/ x1) /\\ (x1 \\/ x2) /\\ (-x1 \\/ -x2) /\\ (x0)".to_string()
148        );
149    }
150}
boolean_circuit/cnf.rs

boolean_circuit/
cnf.rs
