Ruddy

Ruddy is a minimalistic, high-performance Rust library for (reduced and ordered) binary decision diagrams (BDDs), which are a compact representation of Boolean functions.

The name Ruddy is a blend of BuDDy (one of the first widely used BDD libraries) and Rust. However, Ruddy is not affiliated with the developers of BuDDy in any formal way. The name is meant merely as a tribute.

Features

Most popular BDD implementations use a shared representation, where all BDD nodes are stored in a single pool managed by a manager. This allows graphs shared between BDDs to be stored only once in memory. An alternative is the split representation, where each BDD owns its nodes (e.g., as an array).

When BDDs do not meaningfully share nodes, split representations can be faster and more memory-efficient. Ruddy implements both representations, letting users choose what works best for their use case.

Currently, Ruddy supports the following features:

• Binary logical operators (conjunction, xor, ...) and negation.
• Existential and universal quantification, also combined with a binary operator (also called relational product).
• Satisfying valuations and paths iterators along with methods to count them.
• Export to DOT.
• Conversion between split and shared BDDs.
• Binary and text (de)serialization of split BDDs.

Usage

An example of using the Ruddy split implementation:

use ruddy::split::Bdd;
use ruddy::VariableId;

fn example_split() {
    // Create two variables v0 and v1.
    let v0 = VariableId::new(0);
    let v1 = VariableId::new(1);

    // Make the BDDs representing `v0=true` and `v1=true`.
    let a = Bdd::new_literal(v0, true);
    let b = Bdd::new_literal(v1, true);

    // Calculate BDD `a => b`.
    let imp = a.implies(&b);

    // Calculate BDD `!a ∨ b`.
    let equiv_imp = a.not().or(&b);

    // Check that they are equivalent.
    assert!(imp.iff(&equiv_imp).is_true());
}

The same example, using the shared implementation:

use ruddy::shared::BddManager;
use ruddy::VariableId;

fn example_shared() {
    // Create the manager.
    let mut manager = BddManager::new();

    // Create two variables v0 and v1.
    let v0 = VariableId::new(0);
    let v1 = VariableId::new(1);

    // Make the BDDs representing `v0=true` and `v1=true`.
    let a = manager.new_bdd_literal(v0, true);
    let b = manager.new_bdd_literal(v1, true);

    // Calculate BDD `a => b`.
    let imp = manager.implies(&a, &b);

    // Calculate BDD `!a ∨ b`.
    let not_a = manager.not(&a);
    let equiv_imp = manager.or(&not_a, &b);

    // Check that they are equivalent.
    assert!(imp == equiv_imp);
}

More complex examples can be found in the examples folder.