python

vitri for Python

Python bindings for vitri, built with PyO3 and maturin. vitri preprocesses a DIMACS CNF, records how to lift a model count of the reduced formula back to the original, and builds a vtree for the reduced formula.

Use

import vitri

with open("formula.cnf", "rb") as stream:
    result = vitri.prepare(stream.read(), mode="mc", budget_ms=60_000)

result.status            # "built", "fully_resolved" or "refuted"
result.summary["lift"]   # how a count of the reduced formula becomes the input's
result.reduced_cnf       # the formula to compile, as DIMACS text
result.vtree             # the vtree over it in SDD format, or None unless built
result.write("bundle/")  # the files `vitri formula.cnf --out-dir bundle/` writes

help(vitri.prepare) covers the settings, the errors, calls from threads and budgets. The bundle reference describes the files. examples/ counts models with PySDD over the emitted vtree, and runs a call under a hard time limit.

Platforms

The Python workflow builds a wheel for CPython 3.10 and later on x86-64 Linux with glibc 2.34 or newer. It carries GMP 6.3.0 as shared libraries, with its licence texts; the GMP source is attached to each GitHub release. The wheel is not published to an index yet: install it from the workflow's artifact, or build from source. Anywhere else, build from source.

Building from source

The extension compiles the vitri sources in this repository, so it needs the toolchain and system packages listed in building.md, and maturin. PEP 639 resolves license-files against this directory and forbids .., so the notices are copied in first:

.github/scripts/collect-notices.sh bindings/python/notices
pip install maturin
maturin build --release --manifest-path bindings/python/Cargo.toml

maturin develop installs the extension into the active virtual environment for pytest bindings/python/tests. Give pytest --vitri-cli PATH to also compare the bundles with those of the vitri executable.