CUDD (Binary Decision Diagrams)

BDD-based symbolic manipulation and decision procedures for Boolean problems.

Overview

The CUDD backend provides a high-performance implementation of Binary Decision Diagrams (BDDs) that can be used to encode and manipulate Boolean functions and symbolic sets.

Location: lib/Solvers/CUDD/

Main capabilities:

  • Canonical representation of Boolean functions.

  • Efficient Boolean operations (AND, OR, NOT, implication, equivalence, etc.).

  • Symbolic sets and relations represented as BDDs.

  • Support for fixed-point style computations over BDDs.

Typical Use Cases

  • Symbolic state-space exploration and model checking.

  • Boolean abstraction layers in larger analyses.

  • Compact representation of large sets or relations.

Basic Usage (C++)

#include <Solvers/CUDD/CUDDManager.h>

CUDDManager Manager;
auto X = Manager.createVariable("x");
auto Y = Manager.createVariable("y");

// Boolean formula: x ∧ ¬y
auto Phi = X & !Y;

Features

  • BDD operations – Canonical representation and manipulation of Boolean functions.

  • Symbolic sets – Encoding of sets as BDDs with efficient union, intersection, and projection.

  • Fixed-point computation – Iterative algorithms over BDDs for reachability and invariance problems.

Integration Notes

The CUDD backend is typically not used directly by end users. Instead, it is used by higher-level applications and analyses that require symbolic Boolean reasoning. See solvers for an overview of where CUDD fits in the solver stack.