logicng/operations/transformations/dnf/
factorization.rs

1use crate::formulas::operation_cache::OperationCache;
2use crate::formulas::{EncodedFormula, Formula, FormulaFactory, NaryIterator};
3use crate::handlers::{FactorizationError, FactorizationHandler, NopFactorizationHandler};
4
5/// Constructs the _DNF_ of the given formula by using factorization.
6pub fn factorization_dnf(formula: EncodedFormula, f: &FormulaFactory) -> EncodedFormula {
7    factorization_dnf_with_handler(formula, f, &mut NopFactorizationHandler {}).expect("Nop Handler never aborts.")
8}
9
10/// Constructs the _DNF_ of the given formula by using factorization with a
11/// custom handler.
12pub fn factorization_dnf_with_handler(
13    formula: EncodedFormula,
14    f: &FormulaFactory,
15    handler: &mut impl FactorizationHandler,
16) -> Result<EncodedFormula, FactorizationError> {
17    handler.started();
18    if f.config.caches.dnf {
19        apply_rec(formula, f, handler, &mut None)
20    } else {
21        apply_rec(formula, f, handler, &mut Some(OperationCache::new()))
22    }
23}
24
25fn apply_rec(
26    formula: EncodedFormula,
27    f: &FormulaFactory,
28    handler: &mut impl FactorizationHandler,
29    local_cache: &mut Option<OperationCache<EncodedFormula>>,
30) -> Result<EncodedFormula, FactorizationError> {
31    let cached =
32        local_cache.as_ref().map_or_else(|| f.caches.dnf.get(formula), |c| c.get(formula).map_or_else(|| f.caches.dnf.get(formula), Some));
33
34    cached.map_or_else(
35        || {
36            use Formula::{And, Cc, Equiv, False, Impl, Lit, Not, Or, Pbc, True};
37            let result = match formula.unpack(f) {
38                Lit(_) | True | False => Ok(formula),
39                Pbc(_) | Cc(_) | Equiv(_) | Impl(_) | Not(_) => apply_rec(f.nnf_of(formula), f, handler, local_cache),
40                Or(ops) => handle_or(ops, f, handler, local_cache),
41                And(ops) => handle_and(ops, f, handler, local_cache),
42            };
43            if let Ok(res) = result {
44                if let Some(c) = local_cache.as_mut() {
45                    c.insert(formula, res);
46                }
47                if f.config.caches.dnf {
48                    f.caches.dnf.insert(formula, res);
49                }
50                if f.config.caches.is_dnf {
51                    f.caches.is_dnf.insert(res, true);
52                }
53            }
54            result
55        },
56        Ok,
57    )
58}
59
60fn handle_or(
61    operands: NaryIterator,
62    f: &FormulaFactory,
63    handler: &mut impl FactorizationHandler,
64    cache: &mut Option<OperationCache<EncodedFormula>>,
65) -> Result<EncodedFormula, FactorizationError> {
66    compute_nops(operands, f, handler, cache).map(|nops| f.or(&nops))
67}
68
69fn handle_and(
70    operands: NaryIterator,
71    f: &FormulaFactory,
72    handler: &mut impl FactorizationHandler,
73    cache: &mut Option<OperationCache<EncodedFormula>>,
74) -> Result<EncodedFormula, FactorizationError> {
75    compute_nops(operands, f, handler, cache).and_then(|nops| {
76        let mut result = *nops.get(0).unwrap();
77        for &op in nops.iter().skip(1) {
78            result = distribute(result, op, f, handler)?;
79        }
80        Ok(result)
81    })
82}
83
84fn compute_nops(
85    operands: NaryIterator,
86    f: &FormulaFactory,
87    handler: &mut impl FactorizationHandler,
88    cache: &mut Option<OperationCache<EncodedFormula>>,
89) -> Result<Vec<EncodedFormula>, FactorizationError> {
90    let mut nops = Vec::with_capacity(operands.len());
91    for op in operands {
92        nops.push(apply_rec(op, f, handler, cache)?);
93    }
94    Ok(nops)
95}
96
97fn distribute(
98    f1: EncodedFormula,
99    f2: EncodedFormula,
100    f: &FormulaFactory,
101    handler: &mut impl FactorizationHandler,
102) -> Result<EncodedFormula, FactorizationError> {
103    handler.performed_distribution()?;
104    if f1.is_or() || f2.is_or() {
105        let mut nops = Vec::new();
106        let or = if f1.is_or() { f1 } else { f2 };
107        let nor = if f1.is_or() { f2 } else { f1 };
108        for &op in &*or.operands(f) {
109            nops.push(distribute(op, nor, f, handler)?);
110        }
111        Ok(f.or(&nops))
112    } else {
113        let result = f.and(&[f1, f2]);
114        handler.created_clause(result).map(|_| result)
115    }
116}
117
118#[cfg(test)]
119mod tests {
120    use crate::handlers::ClauseLimitFactorizationHandler;
121
122    use super::*;
123
124    #[test]
125    fn test_constants() {
126        test_dnf("$true", "$true");
127        test_dnf("$false", "$false");
128    }
129
130    #[test]
131    fn test_literals() {
132        test_dnf("a", "a");
133        test_dnf("~a", "~a");
134    }
135
136    #[test]
137    fn test_binary_operators() {
138        let f = &FormulaFactory::new();
139        test_dnf("a => b", "~a | b");
140        test_dnf("~a => ~b", "a | ~b");
141        test_dnf("a & b => x | y", "~a | ~b | x | y");
142        test_dnf("a <=> b", "(a & b) | (~a & ~b)");
143        test_dnf("~a <=> ~b", "(a & b) | (~a & ~b)");
144        assert!(factorization_dnf(f.parse("a => b").unwrap(), f).is_dnf(f));
145        assert!(factorization_dnf(f.parse("~a => ~b").unwrap(), f).is_dnf(f));
146        assert!(factorization_dnf(f.parse("a & b => x | y").unwrap(), f).is_dnf(f));
147        assert!(factorization_dnf(f.parse("a <=> b").unwrap(), f).is_dnf(f));
148        assert!(factorization_dnf(f.parse("~a <=> b").unwrap(), f).is_dnf(f));
149    }
150
151    #[test]
152    fn test_nary_operators() {
153        let f = &FormulaFactory::new();
154        test_dnf("a & b", "a & b");
155        test_dnf("x | y", "x | y");
156        test_dnf(
157            "~(a | b) & c & ~(x & ~y) & (w => z)",
158            "~w & ~x & ~a & ~b & c | z & ~x & ~a & ~b & c | ~w & y & ~a & ~b & c | z & y & ~a & ~b & c",
159        );
160        test_dnf("~(a & b) | c | ~(x | ~y)", "~a | ~b | c | ~x & y ");
161        test_dnf("a & b & (~x | ~y)", "~x & a & b | ~y & a & b ");
162        assert!(factorization_dnf(f.parse("a & b").unwrap(), f).is_dnf(f));
163        assert!(factorization_dnf(f.parse("x | y").unwrap(), f).is_dnf(f));
164        assert!(factorization_dnf(f.parse("~(a | b) & c & ~(x & ~y) & (w => z)").unwrap(), f,).is_dnf(f));
165        assert!(factorization_dnf(f.parse("~(a | b) & c & ~(x & ~y) & (w => z)").unwrap(), f,).is_dnf(f));
166        assert!(factorization_dnf(f.parse("~(a & b) | c | ~(x | ~y)").unwrap(), f).is_dnf(f));
167        assert!(factorization_dnf(f.parse("~(a & b) | c | ~(x | ~y)").unwrap(), f).is_dnf(f));
168        assert!(factorization_dnf(f.parse("a | b | (~x & ~y)").unwrap(), f).is_dnf(f));
169        assert!(factorization_dnf(f.parse("a | b | (~x & ~y)").unwrap(), f).is_dnf(f));
170    }
171
172    #[test]
173    fn test_not() {
174        test_dnf("~a2", "~a2");
175        test_dnf("~~a2", "a2");
176        test_dnf("~(a2 => b2)", "a2 & ~b2");
177        test_dnf("~(~(a2 | b2) => ~(x2 | y2))", "x2 & ~a2 & ~b2 | y2 & ~a2 & ~b2");
178        test_dnf("~(a2 <=> b2)", "(a2 & ~b2) | (~a2 & b2)");
179        test_dnf("~(~(a2 | b2) <=> ~(x2 | y2))", "~x2 & ~y2 & a2 | ~x2 & ~y2 & b2 | ~a2 & ~b2 & x2 | ~a2 & ~b2 & y2");
180        test_dnf("~(a2 & b2 & ~x2 & ~y2)", "~a2 | ~b2 | x2 | y2");
181        test_dnf("~(a2 | b2 | ~x2 | ~y2)", "~a2 & ~b2 & x2 & y2");
182        test_dnf("~(a2 | b2 | ~x2 | ~y2)", "~a2 & ~b2 & x2 & y2");
183    }
184
185    #[test]
186    fn test_with_handler() {
187        let f = &FormulaFactory::new();
188
189        let formula = f.parse("(~(~(a | b) => ~(x | y))) & ((a | x) => ~(b | y))").unwrap();
190        let mut handler = ClauseLimitFactorizationHandler::new(100, 2);
191        let result = factorization_dnf_with_handler(formula, f, &mut handler);
192        assert!(result.is_err());
193        assert!(handler.aborted);
194
195        let formula = f.parse("~(a | b)").unwrap();
196        let result = factorization_dnf_with_handler(formula, f, &mut handler);
197        assert!(result.is_ok());
198        assert!(!handler.aborted);
199
200        let mut handler = ClauseLimitFactorizationHandler::new(100, 100);
201        let formula = f.parse("~(~(a2 | b2) <=> ~(x2 | y2))").unwrap();
202        let result = factorization_dnf_with_handler(formula, f, &mut handler);
203        assert!(result.is_ok());
204        assert!(!handler.aborted);
205        assert_eq!(handler.dists, 15);
206        assert_eq!(handler.clauses, 10);
207    }
208
209    fn test_dnf(original: &str, expected: &str) {
210        let f = &FormulaFactory::new();
211        assert_eq!(factorization_dnf(f.parse(original).unwrap(), f), f.parse(expected).unwrap());
212    }
213}
logicng/operations/transformations/dnf/factorization.rs

logicng/operations/transformations/dnf/
factorization.rs
