Semantic BDD Pointers!

Cargo.toml

@@ -36,6 +36,7 @@ wasm-bindgen = { version = "0.2.84" }
 [dev-dependencies]
 serde_json = { version = "1.0.81" }
 clap = { version = "4.2.1", features = ["derive"] }
+rayon = "1.7.0"
 
 [lib]
 name = "rsdd"
@@ -81,3 +82,7 @@ path = "examples/semantic_top_down_experiment.rs"
 [[example]]
 name = "marginal_map_experiment"
 path = "examples/marginal_map_experiment.rs"
+
+[[example]]
+name = "parallel_semantic"
+path = "examples/parallel_semantic.rs"

examples/parallel_semantic.rs

@@ -0,0 +1,207 @@
+use std::{
+    fs,
+    time::{Duration, Instant},
+};
+
+use clap::Parser;
+use rayon::prelude::*;
+use rsdd::{
+    builder::{parallel::SemanticBddBuilder, BottomUpBuilder},
+    constants::primes,
+    repr::{create_semantic_hash_map, Cnf, DDNNFPtr},
+};
+
+#[derive(Parser, Debug)]
+#[clap(author, version, about, long_about = None)]
+struct Args {
+    /// input CNF in DIMACS form
+    #[clap(short, long, value_parser)]
+    file: String,
+
+    /// number of splits to perform on the data
+    #[clap(short, long, value_parser, default_value_t = 4)]
+    num_splits: usize,
+
+    /// use multithreading!
+    #[clap(short, long, value_parser)]
+    thread: bool,
+}
+
+fn split_cnf(cnf: &Cnf, num_splits: usize) -> Vec<Cnf> {
+    let chunk_size = cnf.clauses().len() / num_splits
+        + (if cnf.clauses().len() % num_splits == 0 {
+            0
+        } else {
+            1
+        });
+
+    cnf.clauses().chunks(chunk_size).map(Cnf::new).collect()
+}
+
+fn single_threaded(cnf: &Cnf, num_splits: usize) {
+    let num_splits = std::cmp::min(num_splits, cnf.clauses().len());
+
+    let num_vars = cnf.num_vars();
+    let map = create_semantic_hash_map(num_vars);
+    let order = cnf.min_fill_order();
+
+    let builders: Vec<_> = (0..num_splits)
+        .map(|_| {
+            SemanticBddBuilder::<{ primes::U64_LARGEST }>::new_with_map(order.clone(), map.clone())
+        })
+        .collect();
+
+    let mut ptrs = Vec::new();
+
+    let mut timings = Vec::new();
+
+    for (i, subcnf) in split_cnf(cnf, num_splits).iter().enumerate() {
+        let start = Instant::now();
+        ptrs.push(builders[i].compile_cnf(subcnf));
+        let end = start.elapsed();
+        timings.push(end);
+    }
+
+    let compile_duration: Duration = timings.iter().sum();
+    let compile_max = timings.iter().max().unwrap();
+
+    println!("DONE COMPILING: {:.2}s", compile_duration.as_secs_f64());
+    println!("MAX COMPILATION: {:.2}s", compile_max.as_secs_f64());
+
+    let start = Instant::now();
+
+    let builder = &builders[0];
+    let mut ptr = ptrs[0];
+
+    for i in 1..ptrs.len() {
+        let new_ptr = builder.merge_from(&builders[i], &[ptrs[i]])[0];
+        ptr = builder.and(ptr, new_ptr);
+    }
+
+    let merge_duration = start.elapsed();
+
+    let st_builder =
+        SemanticBddBuilder::<{ primes::U64_LARGEST }>::new_with_map(order.clone(), map.clone());
+
+    let start = Instant::now();
+    let st_ptr = st_builder.compile_cnf(cnf);
+    let single_duration = start.elapsed();
+
+    let wmc = ptr.wmc(&order, &map);
+    let st_wmc = st_ptr.wmc(&order, &map);
+
+    println!("=== TIMING ===");
+    println!(
+        "Compile: {:.2}s (Total {:.2}s), Merge: {:.2}s",
+        compile_max.as_secs_f64(),
+        compile_duration.as_secs_f64(),
+        merge_duration.as_secs_f64()
+    );
+    println!("Single-threaded: {:.2}s", single_duration.as_secs_f64());
+    println!(
+        "Speedup ratio: {:.2}x",
+        single_duration.as_secs_f64() / (compile_max.as_secs_f64() + merge_duration.as_secs_f64())
+    );
+    if wmc != st_wmc {
+        println!(
+            "BROKEN. Not equal WMC; single: {}, merge: {}",
+            st_wmc.value(),
+            wmc.value()
+        );
+    }
+}
+
+fn multi_threaded(cnf: &Cnf, num_splits: usize) {
+    let num_splits = std::cmp::min(num_splits, cnf.clauses().len());
+
+    let num_vars = cnf.num_vars();
+    let map = create_semantic_hash_map(num_vars);
+    let order = cnf.min_fill_order();
+
+    let builders: Vec<_> = split_cnf(cnf, num_splits)
+        .into_par_iter()
+        .map(|subcnf| {
+            (
+                SemanticBddBuilder::<{ primes::U64_LARGEST }>::new_with_map(
+                    order.clone(),
+                    map.clone(),
+                ),
+                subcnf,
+            )
+        })
+        .collect();
+
+    let start = Instant::now();
+
+    let ptrs: Vec<_> = builders
+        .par_iter()
+        .map(|(builder, cnf)| builder.compile_cnf(cnf))
+        .collect();
+
+    let compile_duration: Duration = start.elapsed();
+
+    println!("DONE COMPILING: {:.2}s", compile_duration.as_secs_f64());
+
+    let mut merge_ds = 0.0;
+    let mut merge_and = 0.0;
+
+    let builder = &builders[0].0;
+    let mut ptr = ptrs[0];
+
+    for i in 1..ptrs.len() {
+        let start = Instant::now();
+        let new_ptr = builder.merge_from(&builders[i].0, &[ptrs[i]])[0];
+        merge_ds += start.elapsed().as_secs_f64();
+
+        let start = Instant::now();
+        ptr = builder.and(ptr, new_ptr);
+        merge_and += start.elapsed().as_secs_f64();
+        println!("completed one AND; total time spent: {:.2}s", merge_and);
+    }
+
+    let merge_duration = merge_ds + merge_and;
+
+    let st_builder =
+        SemanticBddBuilder::<{ primes::U64_LARGEST }>::new_with_map(order.clone(), map.clone());
+
+    let start = Instant::now();
+    let st_ptr = st_builder.compile_cnf(cnf);
+    let single_duration = start.elapsed();
+
+    let wmc = ptr.wmc(&order, &map);
+    let st_wmc = st_ptr.wmc(&order, &map);
+
+    println!("=== TIMING ===");
+    println!(
+        "Compile: {:.2}s, Merge: {:.2}s (ds: {:.2}s, ands: {:.2}s)",
+        compile_duration.as_secs_f64(),
+        merge_duration,
+        merge_ds,
+        merge_and
+    );
+    println!("Single-threaded: {:.2}s", single_duration.as_secs_f64());
+    println!(
+        "Speedup ratio: {:.2}x",
+        single_duration.as_secs_f64() / (compile_duration.as_secs_f64() + merge_duration)
+    );
+    if wmc != st_wmc {
+        println!(
+            "BROKEN. Not equal WMC; single: {}, merge: {}",
+            st_wmc.value(),
+            wmc.value()
+        );
+    }
+}
+
+fn main() {
+    let args = Args::parse();
+
+    let cnf_input = fs::read_to_string(args.file).expect("Should have been able to read the file");
+
+    let cnf = Cnf::from_dimacs(&cnf_input);
+
+    match args.thread {
+        false => single_threaded(&cnf, args.num_splits),
+        true => multi_threaded(&cnf, args.num_splits),
+    }
+}

src/backing_store/bump_table.rs

@@ -84,6 +84,7 @@ fn propagate<'a, T: Clone>(
 
 /// Implements a mutable vector-backed robin-hood linear probing hash table,
 /// whose keys are given by BDD pointers.
+#[derive(Debug)]
 pub struct BackedRobinhoodTable<'a, T>
 where
     T: Hash + PartialEq + Clone,

src/builder/bdd/stats.rs

@@ -1,5 +1,6 @@
 /// An auxiliary data structure for tracking statistics about BDD manager
 /// performance (for fine-tuning)
+#[derive(Debug)]
 pub struct BddBuilderStats {
     /// For now, always track the number of recursive calls. In the future,
     /// this should probably be gated behind a debug build (since I suspect

src/builder/cache/all_app.rs

@@ -8,6 +8,7 @@ use rustc_hash::FxHashMap;
 
 /// An Ite structure, assumed to be in standard form.
 /// The top-level data structure that caches applications
+#[derive(Debug)]
 pub struct AllIteTable<T> {
     /// a vector of applications, indexed by the top label of the first pointer.
     table: FxHashMap<(T, T, T), T>,
@@ -54,6 +55,14 @@ impl<'a, T: DDNNFPtr<'a>> AllIteTable<T> {
             table: FxHashMap::default(),
         }
     }
+
+    pub fn iter(&self) -> impl Iterator<Item = (&(T, T, T), &T)> + '_ {
+        self.table.iter()
+    }
+
+    pub fn insert_directly(&mut self, k: (T, T, T), v: T) {
+        self.table.insert(k, v);
+    }
 }
 
 impl<'a, T: DDNNFPtr<'a>> Default for AllIteTable<T> {

src/builder/mod.rs

@@ -5,6 +5,7 @@ pub mod cache;
 
 pub mod bdd;
 pub mod decision_nnf;
+pub mod parallel;
 pub mod sdd;
 
 use crate::{
@@ -31,6 +32,7 @@ pub trait BottomUpBuilder<'a, Ptr> {
     fn or(&'a self, a: Ptr, b: Ptr) -> Ptr {
         self.negate(self.and(self.negate(a), self.negate(b)))
     }
+
     fn negate(&'a self, f: Ptr) -> Ptr;
 
     /// if f then g else h

src/builder/parallel/mod.rs

@@ -0,0 +1,3 @@
+mod semantic_bdd;
+
+pub use self::semantic_bdd::*;