#bdd #symbolic #boolean-expression

biodivine-lib-bdd

A simple thread-safe implementation of basic binary decision diagrams

3 unstable releases

new 0.2.1 Jan 12, 2021
0.2.0 Dec 15, 2020
0.1.0 Feb 7, 2020

#70 in Math

MIT license

135KB
2.5K SLoC

Crates.io Api Docs Travis (.org) Codecov GitHub issues Dev Docs GitHub last commit Crates.io GitHub top language

Biodivine/LibBDD

This crate provides a basic implementation of binary decision diagrams (BDDs) — a symbolic data structure for representing boolean functions or other equivalent objects (such as bit-vector sets).

Compared to other popular implementations, every BDD owns its memory. It is thus trivial to serialise, but also to share between threads. This makes it useful for applications that process high number of BDDs concurrently.

We currently provide support for explicit operations as well as evaluation of basic boolean expressions and a custom bdd macro for hybrid usage:

use biodivine_lib_bdd::*;

fn demo() {
    let vars = BddVariableSet::new(vec!["a", "b", "c"]);
    let a = vars.mk_var_by_name("a");
    let b = vars.mk_var_by_name("b");
    let c = vars.mk_var_by_name("c");
    
    let f1 = a.iff(&b.not()).or(&c.xor(&a));
    let f2 = vars.eval_expression_string("(a <=> !b) | c ^ a");
    let f3 = bdd!((a <=> (!b)) | (c ^ a));
    
    assert!(!f1.is_false());
    assert_eq!(f1.cardinality(), 6.0);
    assert_eq!(f1, f2);
    assert_eq!(f2, f3);
    assert!(f1.iff(&f2).is_true());
    assert!(f1.iff(&f3).is_true());
}

Additionally, we provide serialisation into a custom string and binary formats as well as .dot. For a more detailed description, see the tutorial module documentation. There is also an experimental support for converting BDDs back into boolean expressions.

Performance

Critical part of every BDD implementation is performance. Currently, the repository contains a benchmark branch with several benchmark problems evaluable using this crate as well as other state-of-the-art BDD libraries (bex, cudd and buddy). In our experience, biodivine-lib-bdd performs comparably to these libraries for large problem instances:

Performance stats

The benchmarks typically consist of incrementally constructing one large BDD of exponential size. For some applications where node reuse is more important (very similar formulas appear repeatedly), lib-bdd would probably be slower. Also note that even though buddy is winning, the setting of initial cache size was critical when achieving this level of performance (each benchmark has a specifically tuned cache size to avoid garbage collection and overallocation). If the size of the problem is not known beforehand, buddy may perform significantly worse.

Dependencies

~125KB