Merge pull request #51 from timbeurskens/feature/choice-filtering

implement choice retention

Cargo.toml

@@ -9,7 +9,7 @@ authors = ["Tim Beurskens <timbeurskens.97@gmail.com>"]
 [package]
 name = "rsbdd"
 description = "A BDD-based SAT solver"
-version = "0.10.6"
+version = "0.12.0"
 edition.workspace = true
 authors.workspace = true
 
@@ -33,16 +33,16 @@ pretty_assertions.workspace = true
 
 [workspace.dependencies]
 dot = "0.1"
-itertools = "0.10"
+itertools = "0.11"
 lazy_static = "1.4"
 rand = "0.8"
 rustc-hash = "1.1"
-clap = { version = "4.3", features = ["derive", "env", "wrap_help", "usage"] }
-csv = "1.2"
-regex = "1.7"
+clap = { version = "4.4", features = ["derive", "env", "wrap_help", "usage"] }
+csv = "1.3"
+regex = "1.9"
 glob = "0.3"
-pretty_assertions = "1.3"
+pretty_assertions = "1.4"
 anyhow = "1.0"
-rayon = "1.7"
+rayon = "1.8"
 argfile = "0.1"
-wild = "2.1"
+wild = "2.2"

queentest.txt

@@ -0,0 +1,54 @@
+"Generated by n-queens-gen version 0.10.4 queens=7 "
+
+"every diagonal must contain at most one queen (direction 1)"
+[v_0,v_8,v_16,v_24,v_32,v_40,v_48,] <= 1 &
+[v_1,v_9,v_17,v_25,v_33,v_41,] <= 1 &
+[v_2,v_10,v_18,v_26,v_34,] <= 1 &
+[v_3,v_11,v_19,v_27,] <= 1 &
+[v_4,v_12,v_20,] <= 1 &
+[v_5,v_13,] <= 1 &
+[v_6,] <= 1 &
+
+[v_7,v_15,v_23,v_31,v_39,v_47,] <= 1 &
+[v_14,v_22,v_30,v_38,v_46,] <= 1 &
+[v_21,v_29,v_37,v_45,] <= 1 &
+[v_28,v_36,v_44,] <= 1 &
+[v_35,v_43,] <= 1 &
+[v_42,] <= 1 &
+
+"every diagonal must contain at most one queen (direction 2)"
+[v_0,] <= 1 &
+[v_1,v_7,] <= 1 &
+[v_2,v_8,v_14,] <= 1 &
+[v_3,v_9,v_15,v_21,] <= 1 &
+[v_4,v_10,v_16,v_22,v_28,] <= 1 &
+[v_5,v_11,v_17,v_23,v_29,v_35,] <= 1 &
+[v_6,v_12,v_18,v_24,v_30,v_36,v_42,] <= 1 &
+
+[v_48,] <= 1 &
+[v_47,v_41,] <= 1 &
+[v_46,v_40,v_34,] <= 1 &
+[v_45,v_39,v_33,v_27,] <= 1 &
+[v_44,v_38,v_32,v_26,v_20,] <= 1 &
+[v_43,v_37,v_31,v_25,v_19,v_13,] <= 1 &
+
+"every row must contain exactly one queen"
+[v_0,v_1,v_2,v_3,v_4,v_5,v_6,] = 1 &
+[v_7,v_8,v_9,v_10,v_11,v_12,v_13,] = 1 &
+[v_14,v_15,v_16,v_17,v_18,v_19,v_20,] = 1 &
+[v_21,v_22,v_23,v_24,v_25,v_26,v_27,] = 1 &
+[v_28,v_29,v_30,v_31,v_32,v_33,v_34,] = 1 &
+[v_35,v_36,v_37,v_38,v_39,v_40,v_41,] = 1 &
+[v_42,v_43,v_44,v_45,v_46,v_47,v_48,] = 1 &
+
+"every column must contain exactly one queen"
+[v_0,v_7,v_14,v_21,v_28,v_35,v_42,] = 1 &
+[v_1,v_8,v_15,v_22,v_29,v_36,v_43,] = 1 &
+[v_2,v_9,v_16,v_23,v_30,v_37,v_44,] = 1 &
+[v_3,v_10,v_17,v_24,v_31,v_38,v_45,] = 1 &
+[v_4,v_11,v_18,v_25,v_32,v_39,v_46,] = 1 &
+[v_5,v_12,v_19,v_26,v_33,v_40,v_47,] = 1 &
+[v_6,v_13,v_20,v_27,v_34,v_41,v_48,] = 1 &
+
+"end"
+true

src/bdd.rs

@@ -6,7 +6,7 @@ use std::fmt::Debug;
 use std::hash::{Hash, Hasher};
 use std::rc::Rc;
 
-use crate::{BDDSymbol, NamedSymbol};
+use crate::{BDDSymbol, NamedSymbol, TruthTableEntry};
 
 #[macro_export]
 macro_rules! bdd {
@@ -19,7 +19,7 @@ macro_rules! bdd {
     }};
 }
 
-#[derive(Debug, Clone, Eq, PartialEq, Hash, Default)]
+#[derive(Debug, Clone, Default, Eq, PartialEq, Hash)]
 pub enum BDD<Symbol: BDDSymbol> {
     #[default]
     False,
@@ -28,6 +28,44 @@ pub enum BDD<Symbol: BDDSymbol> {
     Choice(Rc<BDD<Symbol>>, Symbol, Rc<BDD<Symbol>>),
 }
 
+impl<Symbol> BDD<Symbol>
+where
+    Symbol: BDDSymbol,
+{
+    pub fn is_choice(&self) -> bool {
+        matches!(self, BDD::Choice(_, _, _))
+    }
+
+    pub fn is_const(&self) -> bool {
+        !self.is_choice()
+    }
+
+    pub fn is_true(&self) -> bool {
+        self == &BDD::True
+    }
+
+    pub fn is_false(&self) -> bool {
+        self == &BDD::False
+    }
+
+    pub fn node_list(self: &Rc<Self>) -> Vec<Rc<Self>> {
+        match self.as_ref() {
+            BDD::Choice(l, _, r) => {
+                let l_nodes = l.node_list();
+                let r_nodes = r.node_list();
+
+                l_nodes
+                    .iter()
+                    .chain(&vec![Rc::clone(self)])
+                    .chain(r_nodes.iter())
+                    .cloned()
+                    .collect()
+            }
+            BDD::True | BDD::False => vec![Rc::clone(self)],
+        }
+    }
+}
+
 impl From<BDD<NamedSymbol>> for BDD<usize> {
     fn from(bdd: BDD<NamedSymbol>) -> BDD<usize> {
         match bdd {
@@ -82,7 +120,7 @@ impl<S: BDDSymbol> BDDEnv<S> {
     }
 
     pub fn duplicates(&self, root: Rc<BDD<S>>) -> usize {
-        let all_nodes: Vec<Rc<BDD<S>>> = Self::node_list(root);
+        let all_nodes: Vec<Rc<BDD<S>>> = root.node_list();
 
         // todo: conclusion: hashes are stricter than pointers
         // try to rephrase the equivalence check, such hash a == hash b <=> a == b
@@ -101,23 +139,6 @@ impl<S: BDDSymbol> BDDEnv<S> {
         unique_pointers - unique_hashes
     }
 
-    pub fn node_list(root: Rc<BDD<S>>) -> Vec<Rc<BDD<S>>> {
-        match root.as_ref() {
-            BDD::Choice(l, _, r) => {
-                let l_nodes = Self::node_list(Rc::clone(l));
-                let r_nodes = Self::node_list(Rc::clone(r));
-
-                l_nodes
-                    .iter()
-                    .chain(&vec![Rc::clone(&root)])
-                    .chain(r_nodes.iter())
-                    .cloned()
-                    .collect()
-            }
-            BDD::True | BDD::False => vec![Rc::clone(&root)],
-        }
-    }
-
     /// Make a new choice based on the given symbol and the left and right subtree.
     /// The new choice is then simplified and a reference is added to the lookup table.
     ///
@@ -444,4 +465,43 @@ impl<S: BDDSymbol> BDDEnv<S> {
             _ => Rc::clone(a),
         }
     }
+
+    pub fn retain_choice_bottom_up(&self, src: Rc<BDD<S>>, filter: TruthTableEntry) -> Rc<BDD<S>> {
+        match filter {
+            // if we don't filter, we can just return the source
+            TruthTableEntry::Any => src,
+            // otherwise, remove nodes depending on truth value of the filter
+            _ => {
+                match src.as_ref() {
+                    BDD::Choice(left, symbol, right) => {
+                        // recursively run the retain function
+                        let left = self.retain_choice_bottom_up(Rc::clone(left), filter);
+                        let right = self.retain_choice_bottom_up(Rc::clone(right), filter);
+
+                        if left.is_const() && right.is_choice() {
+                            if left.is_true() != filter.is_true() {
+                                // omit choice
+                                eprintln!("omitted choice {symbol}");
+                                right
+                            } else {
+                                self.mk_choice(left, symbol.clone(), right)
+                            }
+                        } else if right.is_const() && left.is_choice() {
+                            if right.is_true() != filter.is_true() {
+                                // omit choice
+                                eprintln!("omitted choice {symbol}");
+                                left
+                            } else {
+                                self.mk_choice(left, symbol.clone(), right)
+                            }
+                        } else {
+                            self.mk_choice(left, symbol.clone(), right)
+                        }
+                    }
+                    // if the node is a constant, we can just return it
+                    _ => src,
+                }
+            }
+        }
+    }
 }

src/main.rs → src/bin/rsbdd.rs

@@ -37,36 +37,40 @@ struct Args {
     /// Write the bdd to a dot graphviz file.
     dot: Option<PathBuf>,
 
-    /// Compute a single satisfying model as output.
     #[clap(short, long)]
+    /// Compute a single satisfying model as output.
     model: bool,
 
-    /// Print all satisfying variables leading to a truth value.
     #[clap(short, long)]
+    /// Print all satisfying variables leading to a truth value.
     vars: bool,
 
-    /// Only show true or false entries in the output.
     #[clap(short, long, value_parser, default_value_t = TruthTableEntry::Any)]
+    /// Only show true or false entries in the output.
     filter: TruthTableEntry,
 
-    /// Repeat the solving process n times for more accurate performance reports.
+    #[clap(short = 'c', long, value_parser, default_value_t = TruthTableEntry::Any)]
+    /// Only retain choice variables when filtering.
+    retain_choices: TruthTableEntry,
+
     #[clap(short, long, value_parser, value_name = "N")]
+    /// Repeat the solving process n times for more accurate performance reports.
     benchmark: Option<usize>,
 
-    /// Use GNUPlot to plot the runtime distribution.
     #[clap(short = 'g', long)]
+    /// Use GNUPlot to plot the runtime distribution.
     plot: bool,
 
-    /// Parse the formula as string.
     #[clap(short, long, value_parser)]
+    /// Parse the formula as string.
     evaluate: Option<String>,
 
-    /// Read a custom variable ordering from file.
     #[clap(short, long, value_parser)]
+    /// Read a custom variable ordering from file.
     ordering: Option<PathBuf>,
 
-    /// Export the automatically derived ordering to stdout.
     #[clap(short = 'r', long)]
+    /// Export the automatically derived ordering to stdout.
     export_ordering: bool,
 }
 
@@ -126,6 +130,14 @@ fn main() {
         eprintln!("finished {}/{} runs", i + 1, repeat);
     }
 
+    // Simplify the output when retain_choices is on
+    if !args.retain_choices.is_any() {
+        result = input_parsed
+            .env
+            .borrow()
+            .retain_choice_bottom_up(result, args.retain_choices);
+    }
+
     // only print performance results when the benchmark flag is available, and more than 1 run has completed
     if args.benchmark.is_some() && repeat > 0 {
         print_performance_results(&exec_times);

src/parser_io.rs

@@ -43,7 +43,7 @@ impl SymbolicParseTree {
                 let mut new_nodes: Vec<SymbolicBDD> = this_node;
 
                 for subtree in f {
-                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree).into_iter());
+                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree));
                 }
 
                 new_nodes
@@ -52,11 +52,11 @@ impl SymbolicParseTree {
                 let mut new_nodes: Vec<SymbolicBDD> = this_node;
 
                 for subtree in a {
-                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree).into_iter());
+                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree));
                 }
 
                 for subtree in b {
-                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree).into_iter());
+                    new_nodes.extend(SymbolicParseTree::nodes_recursive(subtree));
                 }
 
                 new_nodes

src/truth_table.rs

@@ -36,6 +36,18 @@ impl TruthTableEntry {
             TruthTableEntry::Any => matches!(s, "any" | "Any" | "a" | "A" | "*"),
         }
     }
+
+    pub fn is_true(self) -> bool {
+        self == TruthTableEntry::True
+    }
+
+    pub fn is_false(self) -> bool {
+        self == TruthTableEntry::False
+    }
+
+    pub fn is_any(self) -> bool {
+        self == TruthTableEntry::Any
+    }
 }
 
 impl Display for TruthTableEntry {

tests/hash.rs

@@ -99,7 +99,7 @@ fn test_duplicates() {
 
     let mut max_size: usize = 0;
 
-    for ref node in BDDEnv::node_list(Rc::clone(&expr_comb_clean)) {
+    for ref node in expr_comb_clean.node_list() {
         let h = node.get_hash();
 
         if let Some(l) = hm.get_mut(&h) {