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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

//! A decomposition turned into a vtree: the edge shapes, and every reading

use super::*;

/// The only bag covers two of the three declared variables, so the third
/// reaches the vtree through the append of variables no bag holds at all.
#[test]
fn test_td_to_vtree_isolated_vars() {
    let td = make_td(vec![vec![0, 1]], vec![], 2);
    let vtree = td_to_vtree(&td, 3);

    assert_eq!(vtree.num_leaves(), 3);
}

/// Single-variable TD with a single bag. Smallest valid input — checks the
/// 1-leaf vtree path doesn't trip the balanced-combine fallback.
#[test]
fn test_td_to_vtree_single_var_single_bag() {
    let td = make_td(vec![vec![0]], vec![], 1);
    let vtree = td_to_vtree(&td, 1);
    assert_covers_all_vars(&vtree, 1, "one bag holding one variable");
}

/// Multi-component TD where one component has an isolated variable not in any
/// bag. Mixes both recovery paths: component join, and the append of variables
/// that appear in no bag at all.
#[test]
fn test_td_to_vtree_multi_component_plus_isolated_var() {
    // bag0 = {0, 1}, bag1 = {2, 3}, no edges. Variable 4 in no bag.
    let td = make_td(vec![vec![0, 1], vec![2, 3]], vec![], 4);
    let vtree = td_to_vtree(&td, 5);
    assert_covers_all_vars(&vtree, 5, "two components plus a variable no bag holds");
}

/// Single bag stuffed with all variables. The wide-bag stress case — the in-bag
/// ordering heuristics all reduce to identity when there is no clause-affinity
/// signal to break ties.
#[test]
fn test_td_to_vtree_single_wide_bag() {
    let all_vars: Vec<u32> = (0..16).collect();
    let td = make_td(vec![all_vars], vec![], 16);
    let vtree = td_to_vtree(&td, 16);
    assert_covers_all_vars(&vtree, 16, "one bag holding every variable");
}

#[test]
fn test_td_to_vtree_hypergraph_binarization() {
    let td = make_td(vec![vec![0, 1, 2], vec![2, 3]], vec![(0, 1)], 4);

    let reading = Reading {
        root: Some(Root::First),
        place: Some(Place::Deep),
        binarize: Some(Binarization::Hypergraph),
    };
    let vtree = td_to_vtree_reading(&td, 4, reading, None, None);
    assert_eq!(vtree.num_leaves(), 4);
}

/// Bag-tree edges are undirected structure, not an ordering signal. Two
/// decompositions that differ only in the order those edges were supplied must
/// therefore produce the same vtree under the same fixed reading.
#[test]
fn equivalent_bag_edge_orders_convert_to_the_same_vtree() {
    let bags = vec![vec![0], vec![0, 1], vec![0, 2], vec![0, 3], vec![0, 4]];
    let ascending = make_td(bags.clone(), vec![(0, 1), (0, 2), (0, 3), (0, 4)], 5);
    let descending = make_td(bags, vec![(0, 4), (0, 3), (0, 2), (0, 1)], 5);
    let reading = Reading {
        root: Some(Root::First),
        place: Some(Place::Deep),
        binarize: Some(Binarization::Balanced),
    };

    let first = td_to_vtree_reading(&ascending, 5, reading, None, None);
    let second = td_to_vtree_reading(&descending, 5, reading, None, None);

    assert!(
        first.same_tree(&second),
        "equivalent undirected bag trees must not encode edge insertion order",
    );
}

/// Every reading the three dimensions name, on a decomposition that is one path
/// and on one that falls into two components, with and without the formula the
/// clause-driven binarizations read.
///
/// A reading chooses a shape; none of them may choose a different variable set,
/// and a conversion that dropped or duplicated a leaf would produce a vtree no
/// consumer can score against the formula it was built for.
#[test]
fn every_reading_gives_one_leaf_per_variable() {
    let path = make_td(
        vec![vec![0, 1], vec![1, 2], vec![2, 3], vec![3, 4]],
        vec![(0, 1), (1, 2), (2, 3)],
        5,
    );
    let split = make_td(vec![vec![0, 1, 2], vec![3, 4], vec![5, 6]], vec![(1, 2)], 7);
    let path_formula = make_formula(5, vec![vec![1, 2], vec![2, 3], vec![3, 4], vec![4, 5]]);
    let split_formula = make_formula(7, vec![vec![1, 2, 3], vec![4, 5], vec![6, 7], vec![-4, 6]]);

    for (shape, td, num_vars, formula) in [
        ("a path", &path, 5u32, &path_formula),
        ("two components", &split, 7, &split_formula),
    ] {
        for place in [Place::Shallow, Place::Deep] {
            for root in [Root::First, Root::Centroid, Root::Leaf] {
                for binarize in [
                    Binarization::Edge,
                    Binarization::Hypergraph,
                    Binarization::Balanced,
                ] {
                    let reading = Reading {
                        root: Some(root),
                        place: Some(place),
                        binarize: Some(binarize),
                    };
                    for read_formula in [None, Some(formula)] {
                        let vtree = td_to_vtree_reading(td, num_vars, reading, read_formula, None);
                        let what = format!(
                            "{shape} under {reading:?} (formula: {})",
                            read_formula.is_some(),
                        );
                        assert_eq!(
                            vtree.num_leaves(),
                            num_vars,
                            "{what} changed the leaf count"
                        );
                        assert_covers_all_vars(&vtree, num_vars, &what);
                    }
                }
            }
        }
    }
}