Crate vitri 

vitri: CNF preprocessing and vtree construction for circuit compilation.

A raw DIMACS CNF goes in; a reduced CNF, the arithmetic to lift a model count over it back to the original, and a ranked set of vtrees over it come out. Nothing here depends on a particular diagram compiler — the crate is standalone, and a d-DNNF, SDD or tree-decision-diagram (TDD) compiler consumes its output.

Start here

Three calls, in order:

1. CnfFormula::from_dimacs parses the instance.
2. run preprocesses it and builds the vtree over what preprocessing left, in the one order those two run in. The returned VitriRun also reports the raw input’s structural profile; run owns that measurement and uses it for structure-sensitive vtree selection. A caller that needs to establish the run before beginning this work uses frontend and then FrontendSession::prepare; run is that pair in one call.
3. VitriRun::write_to_dir writes every file the result can name.

Those three, and the types they take and hand back, are re-exported at the crate root: the example below names no module.

The two halves are also callable on their own — bundle::preprocess and component::build_vtree — for a caller that compiles from the values rather than from files.

Process model

On unix, bundle::preprocess runs its budgeted preprocessing stage in a child process created with fork(). The stage is a single uninterruptible native call, so the fork is what makes its budget real: the parent SIGKILLs a child that outlives the deadline, and the child’s page tables bound how much memory the stage can commit to the parent. Everything else runs in the calling process, and the result comes back over a pipe. The two projected reductions are the exception and run inline: what they hold when the deadline passes is the deliverable, so killing them would throw away the answer rather than bound it, and their overrun is bounded by an input-size gate instead.

This crate creates no threads, and the fork requires the caller to be single-threaded at that call: a lock held by another of the caller’s threads when the fork happens is held forever in the child. On non-unix targets the stage runs inline instead, and the budget bounds only the work between stages.

A worked example

The flow the standalone binary is a shell over. Every flag it parses is a field of the one RunConfig, whose Default is the production configuration.

use std::fs::File;
use std::io::BufReader;
use std::path::Path;

use vitri::{
    CnfFormula, CnfMeta, ComponentWriteOptions, RunConfig, RunPaths, RunVtree, SelectionCtx,
};

let out_dir = Path::new("bundle");

let config = RunConfig { budget_ms: Some(60_000), ..RunConfig::default() };
config.validate()?;

let reader = BufReader::new(File::open("instance.cnf")?);
let (formula, meta): (CnfFormula, CnfMeta) = CnfFormula::from_dimacs(reader)?;
let run = vitri::run(&formula, &meta, &config, &SelectionCtx::plain())?;
let paths: RunPaths = run.write_to_dir(out_dir, ComponentWriteOptions::default())?;
println!("wrote {}", paths.bundle.reduced_cnf.display());

// Preprocessing can settle the instance by itself, either by resolving every
// variable — the lift is then the whole answer — or by refuting it. Both are
// outcomes rather than errors, and neither has a vtree.
match &run.vtree {
    RunVtree::Built(built) => println!("{} vtree nodes", built.vtree.num_nodes()),
    RunVtree::FullyResolved => println!("count(original) = the record's lift"),
    RunVtree::Refuted => println!("count(original) = 0"),
}

It is written against Box<dyn Error> because opening the file is std::io’s failure, not this crate’s: every fallible entry point here, the writers included, returns VitriError.

Module reference

• vtree: the vtree structure itself — nodes, topology, ordering, LCA, (de)serialization, and the two rotations (rotate_left / rotate_right) a consumer searches vtree space with under a cost model of its own. Two trees compare with Vtree::same_tree; a rotation renumbers, so the serialization is not the comparison. The type a consumer compiles against.
• cnf: the DIMACS VarId/Literal/Clause/CnfFormula types + parser (vtree::VarId and vtree::Literal re-export the first two — one definition).
• bundle: the composite entry point (bundle::run) and the export surface — reduced CNF + count-lift record + vtree serialization, i.e. what the standalone vitri binary writes out. A library caller also gets what the written bundle does not carry: what each preprocessing step did (bundle::StageReport) and the count lift split across the steps that earned it (bundle::CountLift), plus preprocessing wall/probe telemetry (bundle::PreprocessTelemetry). Vtree results likewise report the whole construction wall on component::VtreeBuild::construction_ms.
• dot: Graphviz rendering of a vtree — the bare structure, or heat-mapped and labelled from a per-node annotation table the caller fills (this crate’s own clause-load/context-width numbers, or a compiler’s own).
• preprocess: the CNF preprocessing passes — this crate’s own simplify chain and Arjun, whose stages docs/preprocessing.md lists in order. They are crate-internal — a caller runs them through bundle, which owns which chain a counting mode gets. What it does publish is the vocabulary bundle::PreprocessRecord is written in — the variable correspondences and the Arjun policy the config carries — and the preprocess module documents which.
• projection: projection-safe operations for formulas a consumer derives after the main preprocessing run: bounded hidden-variable elimination and SAT-backed proofs that shown variables determine selected hidden ones.
• sat: the CaDiCaL handle those passes are built on, published because a process holds exactly one CaDiCaL — a consumer that adds a second SAT solver beside this crate links cleanly and then corrupts its heap, so it uses this one. docs/sat.md records the constraint.
• decompose: vtree construction heuristics (treewidth/partition-driven), the CNF-facing counterpart to the vtree structure in vtree. It also answers one question about a formula without building anything: conditioned_primal_width_ub, an upper bound on the primal graph’s width after a conditioning choice. goatd, named throughout this crate and in the goatd-* vtree specs, is this crate’s own pure-Rust tree-decomposition solver: min-fill / min-degree elimination with safe reductions and a refinement pass.
• score: what a vtree is ranked on — clause load, context width and the combined cost vtree_cost, read off a (vtree, formula) pair without compiling anything, every one of them lower-is-better. VtreeScores fuses the five that selection reads and that an emitted candidate set carries. It depends on vtree and cnf alone, so a consumer can score a vtree of its own against the same metrics this crate selected by. It also publishes StructureProfile, the formula-only shape measurement two decisions in this crate read.
• spec, component: the two orchestration layers over construction — spec turns a --vtree spec string into ONE vtree, component splits a formula into independent components, apportions the budget across them, builds a vtree each, and grafts the result. component is the selection path the standalone tool takes.
• candidates: the ranked set of scored candidate vtrees a portfolio construction can retain beside its winner.
• config: RunConfig, the explicit configuration the public entry points take — budget, vtree spec, which preprocessing stages run, SimplifyPolicy, component handling. One budget covers the whole run, and ConstructionBudget says how much of what is left vtree construction may spend — a share of it by default, the whole of it for a caller that has already carved the window itself, or a count of the WORK construction may do (Deterministic), which is what makes the vtree it selects the same on every machine. An embedded caller uses Default and sets the fields it needs; nothing it configures comes from the environment unless it asks, through the two opt-in constructors RunConfig::from_env_defaults and SelectionCtx::with_env_defaults. Configuration is not the whole story: however the config was built, the vendored stack reads three VITRI_* variables of its own with getenv, which this crate validates before any shim exists. A caller that wants a run sealed off from the shell clears VITRI_* from the environment; docs/env.md names every variable and who reads it when. VITRI_BUDGET_MS supplies RunConfig::budget_ms’s default there, and is the one variable whose unusable value reads as unset rather than failing. The rules that scale every internal sub-budget from that field — which travels to them as an argument — and env, which parses every VITRI_* value the crate reads, are crate-internal.
• diagnostics: process-global diagnostics switch — library output is silent by default; the crate’s own binary opts in.
• error: VitriError, the one error type every fallible entry point here returns. Nothing in this crate exits or aborts the calling process — a failure comes back as a value.

The vendored C/C++ stacks (FlowCutter tree decomposition, CaDiCaL/Arjun preprocessing) and the associated build.rs live here. All are built unconditionally; the crate has no on/off feature surface.

Re-exports

pub use bundle::components::ComponentWriteOptions;

pub use bundle::FrontendRetryConfig;

pub use bundle::FrontendSession;

pub use bundle::RetryBudget;

pub use bundle::RunPaths;

pub use bundle::RunVtree;

pub use bundle::VitriRun;

pub use bundle::frontend;

pub use bundle::run;

pub use cnf::CnfFormula;

pub use cnf::CnfMeta;

pub use config::DvePolicy;

pub use config::RunConfig;

pub use config::SimplifyPolicy;

pub use decompose::SelectionCtx;

pub use error::VitriError;

pub use num_rational;

Modules

bundle

Export bundle: the reduced formula, the arithmetic that lifts a count over it back to the original, and the vtree — the artifacts a third-party knowledge compiler needs in order to compile this instance.

candidates

The ranked candidate set: the vtrees the portfolio built and scored on the way to picking one, kept instead of dropped.

cnf

CNF formula types.

component

Per-component vtree orchestration: split a formula into its independent components, build one vtree per component under a shared budget, and graft them into a single whole-formula vtree.

config

RunConfig — the explicit, call-site-visible configuration for this crate’s public entry points.

decompose

Treewidth-based vtree construction.

diagnostics

Diagnostic output control.

dot

Graphviz (DOT) rendering of a vtree.

error

VitriError — the one error type every fallible entry point in this crate returns.

preprocess

CNF preprocessing passes applied before compilation.

projection

Projection-preserving operations for derived CNFs.

sat

The SAT solver vitri uses, exposed so a consumer does not link a second one.

score

Structural scores for a (vtree, formula) pair — what candidate selection ranks on, read off the tree’s shape without compiling anything.

spec

Vtree construction dispatch: a parsed --vtree spec to the backend that builds it.

vtree

Variable tree (vtree): the structural backbone of a compiled diagram.