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

//! Count-preserving BCP simplification for the `pmc` and `pwmc` chains.
//!
//! Runs unit propagation (BCP) on the formula to fixpoint, id-preservingly:
//! variable ids are never renumbered, so the projected chain's `show_set` and weight
//! tables stay keyed to original DIMACS ids.
//!
//! ## Why forced show vars are the crux
//!
//! After BCP a forced variable appears in no remaining clause, so it is absent
//! from the vtree — exactly like a variable that never occurred. But the two
//! contribute differently to a *projected* count:
//!
//!   * a genuinely-free show var (never constrained) → factor 2 (PMC) /
//!     (w⁺+w⁻) (PWMC): both polarities extend to a model;
//!   * a *forced* show var (pinned by a unit cascade) → factor 1 (PMC) /
//!     w_forced-polarity (PWMC): only one polarity extends.
//!
//! A downstream free-show correction counts every absent show var as free, so
//! this module RE-PINS each forced show var with a unit clause: the var
//! occurs again, the compile weights it at exactly factor 1 / its forced
//! polarity, and no downstream correction is owed. Forced *hidden* vars stay
//! removed (correctly ∃-absorbed) — only show vars need the re-pin.
//!
//! A show var absent because its clauses were *satisfied* rather than
//! unit-forced is genuinely free and stays uncounted here: `propagate` only
//! reports unit-forced literals, so no unit is re-pinned for it.

use crate::cnf::{CnfFormula, ShowMask};

/// Result of count-preserving BCP over the projected chain.
pub(super) struct BcpResult {
    /// Reduced formula, variable ids preserved, with a unit clause re-pinning
    /// every forced show var. If UNSAT, contains a single empty clause and
    /// `unsat` is set.
    pub(super) formula: CnfFormula,
    /// True iff BCP derived the empty clause (formula is UNSAT).
    pub(super) unsat: bool,
}

/// Run BCP to fixpoint, re-pinning forced counted-vars.
///
/// A projected instance always declares a show set before reaching this module,
/// so there is no "no show set" case to handle here — `show` is the free-show
/// universe outright.
pub(super) fn bcp_simplify(formula: &CnfFormula, show: &ShowMask) -> BcpResult {
    use crate::cnf::Clause;

    let (mut clauses, forced) =
        crate::preprocess::unit_propagation::propagate(&formula.clauses, formula.num_vars);
    let unsat = crate::cnf::contains_empty_clause(&clauses);

    if !unsat {
        for &l in forced.iter().filter(|l| show.is_show(l.var)) {
            clauses.push(Clause::new(vec![l]));
        }
    }

    BcpResult {
        formula: CnfFormula {
            num_vars: formula.num_vars,
            clauses,
        },
        unsat,
    }
}