Add an "optimized DNF" translation (slower, but gives smaller DNFs).

src/_impl_bdd/_impl_dnf.rs

@@ -134,4 +134,80 @@ impl Bdd {
 
         results
     }
+
+    /// Similar to [Bdd::to_dnf], but uses a quadratic optimization algorithm to greedily
+    /// minimize the number of clauses in the final normal form.
+    ///
+    /// For very large BDDs, this can require a lot of computation time. However, in such cases,
+    /// [Bdd::to_dnf] is likely not going to yield good results either.
+    ///
+    /// Currently, there is no "iterator" variant of this algorithm that would generate the DNF
+    /// on-the-fly. But it should be relatively straightforward, so if you need it, please get
+    /// in touch.
+    pub fn to_optimized_dnf(&self) -> Vec<BddPartialValuation> {
+        self._to_optimized_dnf(&|| Ok::<(), ()>(())).unwrap()
+    }
+
+    /// A cancellable variant of [Bdd::to_optimized_dnf].
+    pub fn _to_optimized_dnf<E, I: Fn() -> Result<(), E>>(
+        &self,
+        interrupt: &I,
+    ) -> Result<Vec<BddPartialValuation>, E> {
+        if self.is_false() {
+            return Ok(Vec::new());
+        }
+        if self.is_true() {
+            return Ok(vec![BddPartialValuation::empty()]);
+        }
+
+        fn _rec<E, I: Fn() -> Result<(), E>>(
+            bdd: &Bdd,
+            clause: &mut BddPartialValuation,
+            results: &mut Vec<BddPartialValuation>,
+            interrupt: &I,
+        ) -> Result<(), E> {
+            if bdd.is_false() {
+                return Ok(());
+            }
+
+            if bdd.is_true() {
+                results.push(clause.clone());
+                return Ok(());
+            }
+
+            let mut support = Vec::from_iter(bdd.support_set());
+            support.sort();
+
+            assert!(!support.is_empty());
+
+            let mut best = (support[0], usize::MAX);
+
+            for var in support {
+                interrupt()?;
+
+                let bdd_t = bdd.var_restrict(var, true);
+                let bdd_f = bdd.var_restrict(var, false);
+                let size = bdd_t.size() + bdd_f.size();
+                if size < best.1 {
+                    best = (var, size);
+                }
+            }
+
+            let (var, _) = best;
+
+            clause[var] = Some(true);
+            _rec(&bdd.var_restrict(var, true), clause, results, interrupt)?;
+            clause[var] = Some(false);
+            _rec(&bdd.var_restrict(var, false), clause, results, interrupt)?;
+            clause[var] = None;
+
+            Ok(())
+        }
+
+        let mut buffer = BddPartialValuation::empty();
+        let mut results = Vec::new();
+        _rec(self, &mut buffer, &mut results, interrupt)?;
+
+        Ok(results)
+    }
 }

src/_test_bdd/_test_bdd_logic_fuzzing.rs

@@ -149,11 +149,15 @@ const FUZZ_SEEDS: [u64; 10] = [
     1, 12, 123, 1234, 12345, 123456, 1234567, 12345678, 123456789, 1234567890,
 ];
 
-fn fuzz_test(num_vars: u16, tree_height: u8, seed: u64) {
+fn fuzz_test(num_vars: u16, tree_height: u8, seed: u64) -> bool {
     let universe = BddVariableSet::new_anonymous(num_vars);
     let op_tree = BddOpTree::new_random(tree_height, num_vars, seed);
     let eval = op_tree.eval_in(&universe);
 
+    if eval.is_true() || eval.is_false() {
+        return false;
+    }
+
     for valuation in ValuationsOfClauseIterator::new_unconstrained(num_vars) {
         assert_eq!(
             op_tree.eval_in_valuation(&valuation),
@@ -162,40 +166,92 @@ fn fuzz_test(num_vars: u16, tree_height: u8, seed: u64) {
             valuation
         );
     }
+
+    let dnf = eval.to_dnf();
+    let cnf = eval.to_cnf();
+    let dnf_o = eval.to_optimized_dnf();
+
+    assert!(dnf_o.len() <= dnf.len());
+
+    assert!(universe.mk_dnf(&dnf).iff(&eval).is_true());
+    assert!(universe.mk_dnf(&dnf_o).iff(&eval).is_true());
+    assert!(universe.mk_cnf(&cnf).iff(&eval).is_true());
+
+    true
 }
 
 #[test]
 fn fuzz_var_2() {
+    let mut non_trivial = 0;
+
     for height in 1..10 {
         for seed in FUZZ_SEEDS.iter() {
-            fuzz_test(2, height, *seed);
+            if fuzz_test(2, height, *seed) {
+                non_trivial += 1;
+            }
         }
     }
+
+    println!(
+        "Check {}/{} non-trivial BDDs.",
+        non_trivial,
+        9 * FUZZ_SEEDS.len()
+    );
 }
 
 #[test]
 fn fuzz_var_4() {
+    let mut non_trivial = 0;
+
     for height in 1..10 {
         for seed in FUZZ_SEEDS.iter() {
-            fuzz_test(4, height, *seed);
+            if fuzz_test(4, height, *seed) {
+                non_trivial += 1;
+            }
         }
     }
+
+    println!(
+        "Check {}/{} non-trivial BDDs.",
+        non_trivial,
+        9 * FUZZ_SEEDS.len()
+    );
 }
 
 #[test]
 fn fuzz_var_8() {
+    let mut non_trivial = 0;
+
     for height in 1..10 {
         for seed in FUZZ_SEEDS.iter() {
-            fuzz_test(8, height, *seed);
+            if fuzz_test(8, height, *seed) {
+                non_trivial += 1;
+            }
         }
     }
+
+    println!(
+        "Check {}/{} non-trivial BDDs.",
+        non_trivial,
+        9 * FUZZ_SEEDS.len()
+    );
 }
 
 #[test]
 fn fuzz_var_12() {
+    let mut non_trivial = 0;
+
     for height in 1..10 {
         for seed in FUZZ_SEEDS.iter() {
-            fuzz_test(12, height, *seed);
+            if fuzz_test(12, height, *seed) {
+                non_trivial += 1;
+            }
         }
     }
+
+    println!(
+        "Check {}/{} non-trivial BDDs.",
+        non_trivial,
+        9 * FUZZ_SEEDS.len()
+    );
 }