Crate sddrs

Crate sddrs 

Source
Expand description

§Bottom-up compiler for Sentential Decision Diagrams.

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

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.

See examples for more examples.

The following snippet compiles the function (A ∧ B) ∨ C to 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;
use std::fs::File;
use std::io::BufWriter;

let options = options::SddOptions::builder()
    // Create right-linear vtree.
    .vtree_strategy(options::VTreeStrategy::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, &a_and_b_or_c)
    .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}'");

Main methods to compile SDDs are:

Main methods to query SDDs are:

SDDs can be also minimized after compilation by appropriately manipulating the vtree:

These transformations do not guarantee that the SDD will decrease in size. In fact, it may grow. For this purpose, dynamic minimization via crate::vtree::fragment::Fragment tries to find the vtree that actually minimizes the SDD the most crate::manager::SddManager::minimize.

There are also additional helper functions:

Additional resources:

Modules§

literal
Variables, polarities, and literals.
manager
Manager responsible for manipulating and querying SDDs as well as maintaining the state of the compilation.
sdd
Sentential Decision Diagrams.
vtree
Vtrees and fragments.

Macros§

btreeset