vitri 0.2.0

CNF preprocessing and vtree construction (variable trees) for circuit compilation and model counting: preprocesses a DIMACS CNF, records the arithmetic to lift a model count back to the original, and builds a good vtree for it — for any d-DNNF/SDD/TDD compiler, or any model counter that takes a vtree.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

//! CNF and vtree adapters for the goatd decomposition library.

mod elimination;
mod polishing;
mod sat_score;
mod schedule;
pub use polishing::{GoatdLift, GoatdPolishing};

pub(crate) use elimination::{
    INTERNAL_ELIMINATION_SEED, MINFILL_SPEC, VIEW_SUFFIXES, elimination_order_samples,
    elimination_spec, elimination_spec_names, minfill_td_from_edges, vtree_from_elimination,
    vtree_from_minfill,
};
pub use schedule::GoatdKnobs;
pub(crate) use schedule::{
    MAX_GOATD_CANDIDATES, candidate_param, vtree_from_goatd, vtrees_from_goatd_refined,
};