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
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

//! The FORCE vtree builder.
//!
//! Shared by both topics: the structured fixture [`axis_formula`], the config
//! builder [`cfg_with`], and the quality measure [`max_load`].

use crate::cnf::CnfFormula;
use crate::decompose::force::*;
use crate::tests::common::{assert_covers_all_vars, clause_dimacs};
use crate::vtree::Vtree;

mod axes;
mod build;

/// A deterministic ~100-variable formula.
fn axis_formula() -> CnfFormula {
    let n = 100u32;
    let mut state = 0x9E37_79B9_7F4A_7C15u64;
    let mut rv = || {
        state ^= state << 13;
        state ^= state >> 7;
        state ^= state << 17;
        (state % n as u64) as i32 + 1
    };
    let mut clauses = Vec::new();
    for _ in 0..300 {
        let a = rv();
        let mut b = rv();
        while b == a {
            b = rv();
        }
        let mut c = rv();
        while c == a || c == b {
            c = rv();
        }
        clauses.push(clause_dimacs(&[a, -b, c]));
    }
    CnfFormula {
        num_vars: n,
        clauses,
    }
}

fn cfg_with(mutate: impl FnOnce(&mut ForceConfig)) -> ForceConfig {
    let mut c = ForceConfig::new(ForceMode::Mst);
    mutate(&mut c);
    c
}

/// Max clause-LCA load over internal nodes, through the same helpers the feedback
/// loop optimizes against.
fn max_load(vt: &Vtree, f: &CnfFormula) -> u32 {
    let (_lca, loads) = crate::score::clause_lca_nodes(vt, f);
    max_internal_load(vt, &loads)
}