Binary Decision Diagrams for Rust

High-performance Binary Decision Diagrams (BDDs) library for Rust. BDDs represent Boolean functions canonically, enabling efficient formal verification, static analysis, model checking, and optimization.

Features

• Manager-Centric: All operations through central Bdd manager with hash consing

• Safe & Efficient: Lightweight Ref handles with minimal overhead

• Operation Caching: Computed table avoids redundant operations

• 1-Based Variables: Simplifies integration with DIMACS and similar formats

• Boolean Operations: AND, OR, XOR, NOT, ITE, implication, equivalence

• Quantification: Existential (∃) and universal (∀) over variables

• Complement Edges: Efficient negation via edge attributes

• SAT & Model Counting: Satisfiability checking, model extraction, solution counting

• Visualization: Graphviz DOT export

Companion Guide

A comprehensive tutorial on BDDs is available: guide/

Installation

Add bdd-rs to your Cargo.toml:

[dependencies]
bdd-rs = "0.1"

Quick Start

use bdd_rs::bdd::Bdd;

// Initialize the BDD manager
let bdd = Bdd::default();

// Create variables (1-indexed)
let x1 = bdd.mk_var(1);
let x2 = bdd.mk_var(2);

// Build formula: f = x1 ∧ ¬x2
let not_x2 = bdd.apply_not(x2);
let f = bdd.apply_and(x1, not_x2);

// Check properties
assert!(!bdd.is_zero(f));  // Satisfiable
assert!(!bdd.is_one(f));   // Not a tautology

// Evaluate with assignment: x1=true, x2=false
let result = bdd.cofactor_cube(f, &[1, -2]);
assert!(bdd.is_one(result));

Core API

BDD Manager Operations

• Bdd::default() — Create BDD manager with default parameters

• mk_var(var_id) — Create BDD for variable (1-indexed)

• collect_garbage(roots) — Reclaim unused nodes

Boolean Operations

• apply_and(f, g) — Conjunction: f ∧ g

• apply_or(f, g) — Disjunction: f ∨ g

• apply_xor(f, g) — Exclusive OR: f ⊕ g

• apply_not(f) — Negation: ¬f

• apply_imply(f, g) — Implication: f ⇒ g

• apply_eq(f, g) — Equivalence: f ⇔ g

• apply_ite(i, t, e) — If-then-else: (i ∧ t) ∨ (¬i ∧ e)

Quantification

• exists(var, f) — Existential quantification: ∃var. f

• forall(var, f) — Universal quantification: ∀var. f

Satisfiability & Properties

• is_zero(f) — Check if f is false (unsatisfiable)

• is_one(f) — Check if f is true (tautology)

• is_implies(f, g) — Check if f implies g

• count_sat(f) — Count satisfying assignments

• any_sat(f) — Extract one satisfying assignment

• cofactor(f, var, value) — Restrict variable to value

• cofactor_cube(f, literals) — Restrict multiple variables

Utilities

• size(f) — Count nodes in BDD

• var(f) — Get decision variable of node

• low(f) / high(f) — Get low/high children

• print_stats() — Display manager statistics

Case Studies & Examples

Comprehensive examples demonstrating BDD applications:

Abstract Interpretation

See examples/abstract-interpretation/

Static program analysis framework combining abstract interpretation with BDDs.

Companion Guide: guide/

Examples:

• Numeric Analysis: Sign domain, constant propagation, interval analysis, congruence domain

• Fixpoint Computation: Loop analysis with widening/narrowing

• Control-Sensitive Analysis: Traffic light FSM, mode controllers, protocol verification

• Pointer Analysis: BDD-based points-to analysis with must/may aliasing

• String Analysis: Length tracking, prefix/suffix analysis, regex matching, automata

• Type Analysis: Dynamic type tracking and type error detection

• Security Analysis: Taint tracking, input validation, SQL injection prevention

• Realistic Programs: Array bounds checking, combined multi-domain analysis

Tests: Comprehensive unit and integration tests for all domains

cd examples/abstract-interpretation
cargo run --example sign_analysis
cargo run --example realistic_programs
cargo test  # Run 80+ tests

Symbolic Model Checking

See examples/model-checking/

Symbolic model checking implementing algorithms from Burch et al. (1990).

Companion Guide: guide/

Features:

• Kripke structures with image/preimage computation

• Full CTL support: EX, AX, EF, AF, EG, AG, EU, AU

• Fixpoint algorithms for millions to billions of states

cd examples/model-checking
cargo test
cargo run --bin modelcheck -- example toggle

Symbolic Execution

See examples/symbolic-execution/

Symbolic execution for boolean programs with BDD constraint solving.

Features:

• Path-sensitive state tracking

• Counterexample generation from assertion failures

• Bounded loop unrolling

• Exception handling (try/catch/finally)

Examples: Branching, XOR properties, mutex verification, loops

cd examples/symbolic-execution
cargo run --bin symexec -- example simple
cargo run --bin symexec -- example mutex
cargo run --bin symexec -- example buggy  # See counterexamples!

Additional Examples

• EDA (examples/eda/): Electronic design automation applications

• Feature Models (examples/feature-model/): Software product line analysis

Documentation

• API: cargo doc --open

• Guide: 150-page tutorial

• Examples: Abstract Interpretation, Model Checking, Symbolic Execution

Performance

• Release Mode: Always use --release for production (exponentially faster)

• Variable Ordering: Critical for BDD size; poor ordering causes exponential blowup

• Garbage Collection: Call collect_garbage() periodically

• Caching: Operation cache improves repeated operations

Architecture

Core Modules

• bdd.rs — BDD manager with core algorithms

• node.rs — BDD node representation

• reference.rs — Lightweight node references (Ref)

• storage.rs — Hash-consing table for nodes

• cache.rs — Operation result caching

• table.rs — Unique table for node deduplication

• sat.rs — Satisfiability and model counting

• eval.rs — Variable assignment and evaluation

• paths.rs — Path enumeration

• dot.rs — Graphviz visualization

• utils.rs — Utility functions

Design Decisions

• Manager-Centric: All operations through Bdd manager

• Complement Edges: Only low edges negated, high edges never complemented

• 1-Based Variables: Start at 1 (0 reserved internally)

• Canonical Form: Unique representation per Boolean function

• Hash Consing: Automatic deduplication

Testing

# Run all tests
cargo test

# Test specific module
cargo test --lib bdd

# Run example-specific tests
cd examples/abstract-interpretation
cargo test  # 80+ tests

Contributing

Contributions are welcome! Areas for improvement:

• Variable reordering algorithms (sifting, window permutation)

• Additional symbolic operations (restrict, compose)

• Performance optimizations (parallel operations, cache tuning)

• More examples and case studies

• Documentation improvements

References

Foundational Papers

• Bryant (1986): "Graph-Based Algorithms for Boolean Function Manipulation" — Introduces ROBDDs

• Burch et al. (1990): "Symbolic Model Checking: 10^20 States and Beyond" — Symbolic model checking

• Cousot & Cousot (1977): "Abstract Interpretation: A Unified Lattice Model" — Abstract interpretation foundations

License

This crate is licensed under the MIT License.