Install

pip install tididi

Wheels cover Python 3.10 and later on Linux (x86-64 and ARM64), macOS and Windows. Elsewhere pip builds the package from source, which needs a Rust toolchain.

Getting started

This example builds (x ∧ y) ∨ z and counts its satisfying assignments:

from tididi import Vtree, literal

vtree = Vtree.balanced(3)
x = literal(vtree, 1)
y = literal(vtree, 2)
z = literal(vtree, 3)
f = (x & y) | z
print("Satisfying assignments:", f.model_count())

Output:

Satisfying assignments: 5

Four assignments 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 vtree. Literals are signed variable numbers: 1 is x and -2 is ¬y. Boolean operations consume their operands, so use a.copy() & b.copy() to keep both; queries such as model_count() leave a circuit usable, and reusing a consumed circuit raises ConsumedCircuitError.

The tutorials in the Python guide cover what the library does, with executed output and downloadable scripts and notebooks:

• Build and transform functions by combining circuits, fixing variables and quantifying them out: the reachability tutorial explores a transition system.

• Find and count solutions, and test equivalence or implication: the configuration tutorial 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 tutorial answers a conditional-probability query, and custom algebras compute other quantities, such as a minimum configuration cost.

Further tutorials cover tables, saving and loading, variable grouping, resource limits and circuit statistics. The API reference documents every function.

Applications built on tididi

• 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 higher-level languages: ProbLog programs, Bayesian and Markov networks, and discrete probabilistic programs. It has Python, C and WebAssembly bindings and runs in the browser.

Develop

From bindings/python in a checkout, build in place and run the checks:

python -m venv .venv
. .venv/bin/activate
python -m pip install 'maturin>=1.9.4,<2'
maturin develop --release
python -m pip install '.[test,docs]'
python -m pytest
python -m sphinx -W --keep-going -b html docs docs/_build/html

On Windows activate with .venv\Scripts\activate instead. Sphinx executes the tutorials while building the pages; open docs/_build/html/index.html.

Citing

Please cite A Canonical Generalization of OBDD, which introduced TDDs.

Acknowledgements

This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR0011269E224.