ruddy 0.0.2

Minimalistic library for working with binary decision diagrams.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

# Ruddy

Ruddy is a minimalistic, high-performance Rust library
for [(reduced and ordered) binary decision diagrams](https://en.wikipedia.org/wiki/Binary_decision_diagram) (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:

```rust
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:

```rust
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.