Tree Decision Diagrams for Rust, Python and C.
tididi represents Boolean functions as circuits called Tree Decision Diagrams (TDDs), so you can work with their satisfying assignments without listing them. Build a circuit once, then combine it with other circuits or query it as your inputs change. One Rust implementation serves all three languages.
Like binary decision diagrams, minimized TDDs are canonical and combine efficiently under Boolean operations; in practice they can be much smaller.
- Rust:
cargo add tididi. See the Rust guide and the crate on crates.io. - Python:
pip install tididi. See the Python guide and the package on PyPI. - C and C++: prebuilt packages or a CMake build. See the C guide and the C README.
This example builds (x ∧ y) ∨ z and counts its satisfying assignments:
use std::sync::Arc;
use tididi::{literal, Vtree};
let vtree = Arc::new(Vtree::balanced(3));
let x = literal(&vtree, 1)?;
let y = literal(&vtree, 2)?;
let z = literal(&vtree, 3)?;
let f = (x & y) | z;
println!("Satisfying assignments: {}", f.model_count()?);Output:
Satisfying assignments: 5
The model count is the number of satisfying assignments: four have z true,
and one more has z false with x and y true. A vtree is a binary tree
that groups the variables; circuits you combine must share the same
Arc<Vtree>.
The worked examples cover what the library does:
- Build and transform functions by combining circuits, fixing variables and quantifying them out: the reachability example explores a transition system.
- Find and count solutions, and test equivalence or implication: the configuration example counts a backup application's valid configurations as a user changes their choices.
- Evaluate weighted models such as probabilities, changing the weights without rebuilding the circuit: the probability example answers a conditional-probability query, and custom algebras compute other quantities, such as a minimum configuration cost.
Further worked examples cover tables, saving and loading, variable grouping and resource limits. The API overview finds the operation for a task, the API reference gives its contract, and the data model explains the representation. Contributors can start with the architecture reference.
- tididi-cnf compiles CNF formulas into TDDs for model counting, weighted model counting and projected model counting, from Rust, Python or C.
- tddlog performs exact probabilistic inference for ProbLog, Bayesian networks and probabilistic programs, also in the browser.
Please cite A Canonical Generalization of OBDD, which introduced TDDs.
This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR0011269E224.