Prepare Boolean constraints for counting and circuit compilation.

Compilers of decision diagrams and circuits, SDDs and TDDs among them, take a formula in CNF and a vtree: a binary tree over the formula's variables that fixes the shape of the circuit they build. Their time and memory follow that shape; on the same formula, one vtree compiles in seconds and another does not finish. vitri simplifies the formula first, then builds several vtrees for what is left and hands the compiler the one that scores best. One Rust library serves the command line, Rust, Python, C and the browser.

The vtree --mode compile --vtree force builds for the tutorial's twelve-variable formula, drawn from its --dot output. A darker node has a higher clause load; docs/vtrees.md explains the labels.

Install

• Command line: cargo install vitri --locked, after the build prerequisites. The latest release also has an x86-64 Linux archive of the executable.
• Rust: cargo add vitri, with the same build prerequisites. The crate documentation starts with a worked example.
• Python: pip install pyvitri, imported as vitri. See the Python README.
• C and C++: a build from source. See the C README.
• Browser: drop a DIMACS file into the page. Nothing is uploaded; the tool runs in the tab.

The native builds run on Linux; macOS and Windows are not supported.

Getting started

This prepares the tutorial's formula, which encodes the rules of a small scheduling problem in twelve variables:

curl -fL https://raw.githubusercontent.com/Tractables/vitri/main/docs/example.cnf -o choices.cnf
vitri choices.cnf --mode mc --out-dir bundle/ --budget-ms 60000

Output:

input:        choices.cnf (12 vars, 25 clauses, mode mc)
reduced:      9 vars, 13 clauses  (count(original) = count(reduced) * 2^0)
vtree:        portfolio (9 leaves, 17 nodes)
components:   1 (0 free variables)
wrote:        bundle/reduced.cnf
              bundle/preprocess.json
              bundle/vtree.vtree
              bundle/components.json
elapsed:      60 ms

A compiler reads reduced.cnf with vtree.vtree. Its count of the reduced formula, times the factor on the reduced line, is the count of the input; preprocess.json records that factor. --budget-ms is a time budget for the whole run, not a hard limit, and the constructions scale their effort to it. The tutorial compiles the bundle and checks the count.

What vitri does:

• Preprocess for the task. --mode states what preprocessing must preserve: model counting, weighted or projected counting, or compilation. docs/preprocessing.md lists the modes, the stages each one runs and how the record restores the count.
• Choose a vtree. A portfolio of constructions builds candidates and ranks them on scores read off the formula, without compiling. --vtree picks a construction and --dot draws the result; docs/vtrees.md covers both and how to bring your own decomposition. The showcase runs every construction on one competition instance and compares their scores.
• Hand any compiler a standard bundle. DIMACS and the SDD vtree format, split into connected components; docs/bundle.md gives every file and field.

docs/env.md lists the optional VITRI_* environment variables and docs/building.md the toolchain and the vendored C++ build. vitri links one build of CaDiCaL and publishes it as vitri::sat for programs that need a SAT solver beside it.

Applications built on vitri

• tididi-cnf compiles CNF formulas into Tree Decision Diagrams for model counting, weighted model counting and projected model counting, with vitri's preprocessing and vtrees, also in the browser.

Acknowledgements

vitri builds on the algorithms listed in ACKNOWLEDGEMENTS.md, and THIRD-PARTY.md lists the components it vendors and their licences. This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR0011269E224.