sddrs: Bottom-Up Sentential Decision Diagram Compiler

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

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

See examples for more examples.

The following snippet compiles the function (A & B) | 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;

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".to_string()])
        .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}'");
}

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