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

//! Recursive-vtree adapter for goatd's hypergraph partitioner.

#[cfg(test)]
mod tests;

use std::sync::Arc;

use crate::cnf::CnfFormula;
use crate::vtree::Vtree;

use super::{BisectDials, Bisection};
use super::{BisectionSolver, local_index};

pub(crate) const IMBALANCE_BALANCED: f64 = 0.03;
pub(crate) const IMBALANCE_PORTFOLIO_RELAXED: f64 = 0.40;

pub(crate) fn multilevel_hg_bisect(
    num_vertices: usize,
    hyperedges: &[Vec<u32>],
    hyperedge_weights: Option<&[u32]>,
    dials: BisectDials,
) -> Result<Vec<u8>, String> {
    let num_vertices = u32::try_from(num_vertices)
        .map_err(|_| "hypergraph vertex count does not fit in u32".to_string())?;
    let hypergraph =
        ::goatd::partition::Hypergraph::new(num_vertices, hyperedges, hyperedge_weights)
            .map_err(|error| error.to_string())?;
    let config =
        ::goatd::partition::HypergraphBisectionConfig::new(dials.imbalance, dials.base_seed)
            .with_effort(dials.effort_scale);
    ::goatd::partition::multilevel_hypergraph_bisect(&hypergraph, config)
        .map(::goatd::partition::Bisection::into_parts)
        .map_err(|error| error.to_string())
}

pub(crate) struct HypergraphBisectSolver {
    pub dials: BisectDials,
}

impl BisectionSolver for HypergraphBisectSolver {
    fn partition(
        &mut self,
        vars: &[u32],
        formula: &CnfFormula,
    ) -> Result<Option<Bisection>, String> {
        let local_idx = local_index(vars);
        let mut hyperedges = Vec::new();
        for clause in &formula.clauses {
            let mut pins: Vec<u32> = clause
                .literals
                .iter()
                .filter_map(|literal| local_idx.get(&literal.var.0).copied())
                .collect();
            pins.sort_unstable();
            pins.dedup();
            if pins.len() >= 2 {
                hyperedges.push(pins);
            }
        }
        if hyperedges.is_empty() {
            return Ok(None);
        }
        let weights: Vec<u32> = hyperedges
            .iter()
            .map(|hyperedge| (hyperedge.len() - 1) as u32)
            .collect();
        let parts = multilevel_hg_bisect(vars.len(), &hyperedges, Some(&weights), self.dials)?;
        Ok(Bisection::from_side_bits(vars, &parts))
    }
}

pub(crate) fn vtree_from_hg_bisect(
    formula: &CnfFormula,
    dials: BisectDials,
) -> Result<Arc<Vtree>, String> {
    let mut solver = HypergraphBisectSolver { dials };
    super::run_bisection(formula, &mut solver)
}