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

//! Renumbering an UNSAT residual.
//!
//! An empty clause is a certificate, and compacting variable ids must not
//! lose it — including when every literal was eliminated and nothing is
//! left to renumber.

use super::*;

#[test]
fn renumber_preserves_empty_clause_unsat_certificate() {
    // var 0 is eliminated; var 1 survives and renumbers to local id 0.
    let fates = vec![DveFate::Defined, DveFate::Kept];
    let clauses = vec![
        Clause::new(Vec::new()),                         // UNSAT certificate
        Clause::new(vec![Literal::new(VarId(1), true)]), // survives
    ];
    let (formula, _map) = renumber_formula(&fates, 2, clauses);
    assert!(
        formula.clauses.iter().any(|c| c.literals.is_empty()),
        "empty clause (UNSAT certificate) must be preserved through renumber_formula",
    );
}

#[test]
fn renumber_empty_when_all_literals_eliminated_is_unsat() {
    let fates = vec![DveFate::Defined, DveFate::Kept]; // var 0 eliminated
    let clauses = vec![
        Clause::new(vec![Literal::new(VarId(0), true)]), // -> empty after renumber
        Clause::new(vec![Literal::new(VarId(1), false)]), // survives
    ];
    let (formula, _map) = renumber_formula(&fates, 2, clauses);
    assert!(
        formula.clauses.iter().any(|c| c.literals.is_empty()),
        "clause reduced to empty by elimination must be kept as UNSAT certificate",
    );
}