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

use crate::cnf::{Clause, CnfFormula};
use crate::preprocess::unit_propagation::*;
use crate::tests::common::clause;
use crate::tests::pmc_oracle::brute_force_mc;

fn clauses(cs: &[&[(u32, bool)]]) -> Vec<Clause> {
    cs.iter().copied().map(clause).collect()
}

/// The pass is EQUIVALENCE-preserving, and the forced literals it reports are
/// half of what it produced: they leave the clause set, so a caller that pins
/// them back as unit clauses holds a formula with exactly the models it started
/// with. Dropping them instead multiplies the count by two per forced variable.
#[test]
fn unit_propagation_preserves_the_model_count_of_its_input() {
    let input = CnfFormula {
        num_vars: 4,
        clauses: clauses(&[
            &[(0, true)],
            &[(0, false), (1, true)],
            &[(1, false), (2, true), (3, true)],
            &[(2, false), (3, true)],
        ]),
    };

    let (residual, forced) = propagate(&input.clauses, input.num_vars);
    assert!(
        !forced.is_empty(),
        "the fixture must give the pass something to propagate",
    );

    let mut restored = residual;
    restored.extend(forced.iter().map(|l| Clause::new(vec![*l])));
    assert_eq!(
        brute_force_mc(&CnfFormula {
            num_vars: input.num_vars,
            clauses: restored,
        }),
        brute_force_mc(&input),
        "propagating and re-pinning the forced literals changed the model count",
    );
}

#[test]
fn empty_formula() {
    let (result, forced) = propagate(&[], 3);
    assert!(result.is_empty());
    assert!(forced.is_empty());
}

#[test]
fn no_units() {
    let input = clauses(&[&[(0, true), (1, false)], &[(1, true), (2, true)]]);
    let (result, forced) = propagate(&input, 3);
    assert_eq!(result.len(), 2);
    assert!(forced.is_empty());
}

#[test]
fn single_unit() {
    let input = clauses(&[
        &[(0, true)],
        &[(0, false), (1, true)],
        &[(0, true), (2, true)],
    ]);
    let (result, forced) = propagate(&input, 3);
    // x0 forced. Clause 2 satisfied (contains x0). Clause 1 shortened to (x1).
    // (x1) is now unit -> x1 forced too.
    assert!(!forced.is_empty());
    // All forced variables' unit clauses are removed (re-added by caller).
    for c in &result {
        assert!(
            c.literals.len() > 1 || {
                let l = c.literals[0];
                !forced.iter().any(|f| f.var == l.var)
            }
        );
    }
}

#[test]
fn cascading_units() {
    let input = clauses(&[
        &[(0, true)],
        &[(0, false), (1, true)],
        &[(1, false), (2, true)],
    ]);
    let (result, forced) = propagate(&input, 3);
    assert_eq!(forced.len(), 3);
    assert!(result.is_empty());
}

#[test]
fn two_opposing_units_propagate_to_the_empty_clause() {
    let input = clauses(&[&[(0, true)], &[(0, false)]]);
    let (result, _forced) = propagate(&input, 1);
    assert!(result.iter().any(|c| c.literals.is_empty()));
}

#[test]
fn a_cascade_that_ends_in_a_conflict_propagates_to_the_empty_clause() {
    let input = clauses(&[&[(0, true)], &[(0, false), (1, true)], &[(1, false)]]);
    let (result, _forced) = propagate(&input, 2);
    assert!(result.iter().any(|c| c.literals.is_empty()));
}