📚 sddrs: Bottom-Up Sentential Decision Diagram Compiler

Incrementally build, manipualate, and optimize Sentential Decision Diagrams (SDD): a succinct representation of Boolean functions.

Crate's API documentation can be found here.

🎉 Features

The compiler currently supports:

• incremental compilation of Boolean functions (knowledge bases) to compressed and trimmed SDDs,
• efficient querying of model count, model enumeration, and equivalence of SDDs,
• dynamic minimization of SDDs via vtree fragments,
• garbage collection of dead nodes,
• SDD compilation from CNF in DIMACS format.

Usage

📦 Library

To use the compiler within a project, add the following line to your Cargo.toml:

[dependencies]
sddrs = { version = "0.1" }

Then import the crate, initialize an SddManager and compile Boolean functions! The following snippet compiles the function $(A \land B) \lor C$ to an SDD, computes number of its models, enumerates and prints them to the stdout, and renders the compiled SDD and its vtree to the DOT format.

use sddrs::manager::{options, GCStatistics, SddManager};
use sddrs::literal::literal::Polarity;
use bon::arr;

fn main() {
    let options = options::SddOptions::builder()
        // Create right-linear vtree.
        .vtree_strategy(options::VTreeStragey::RightLinear)
        // Initialize the manager with variables A, B, and C.
        .variables(["A".to_string(), "B".to_string(), "C"])
        .build();
    let manager = SddManager::new(options);

    // Retrieve SDDs for literals A, B, and C.
    let a = manager.literal("A", Polarity::Positive).unwrap();
    let b = manager.literal("B", Polarity::Positive).unwrap();
    let c = manager.literal("C", Polarity::Positive).unwrap();

    // Compute "A ∧ B"
    let a_and_b = manager.conjoin(&a, &b);
    // Compute "(A ∧ B) ∨ C"
    let a_and_b_or_c = manager.disjoin(&a_and_b, &c);

    let model_count = manager.model_count(&a_and_b_or_c);
    let models = manager.model_enumeration(&a_and_b_or_c);

    println!("'(A ∧ B) ∨ C' has {model_count} models.");
    println!("They are:\n{models}");

    let sdd_path = "my_formula.dot"
    let f = File::create(sdd_path).unwrap();
    let mut b = BufWriter::new(f);
    manager
        .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd)
        .unwrap();

    let vtree_path = "my_vtree.dot"
    let f = File::create(vtree_path).unwrap();
    let mut b = BufWriter::new(f);
    manager
        .draw_vtree(&mut b as &mut dyn std::io::Write)
        .unwrap();

    println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'");
}

See examples for more examples.

Binary

The compiler can be also compiled and invoked as a command-line utility.

cargo build --release
./target/release/sddrsc \
    --count-models \
    --enumerate-models \
    --vtree right-linear \
    --minimize-after-k-clauses 2 \
    --print-statistics \
    --collect-garbage  \
    --sdd.dot \
    --dimacs-path ./static/datasets/easy.cnf

To render the SDD, install Graphviz and run

dot sdd.dot -Tpng -o sdd.png

📃 Related Links

• SDD: A New Canonical Representation of Propositional Knowledge Bases - Adnad Darwiche: paper introducing SDDs
• Dynamic Minimization of Sentential Decision Diagrams - Arthur Choi and Adnan Darwiche: paper describing dynamic minimization of SDDs
• SDD: A New Canonical Representation of Propositional Knowledge Bases – Adnan Darwiche (YouTube tutorial)
• Bottom-Up Knowledge Compilers – Adnan Darwiche (YouTube tutorial)
• The SDD Package homepage: homepage of the original C SDD compiler
• RSDD: alternative implementation of SDD in Rust