logicng 0.1.0-alpha.3

A Library for Creating, Manipulating, and Solving Boolean Formulas
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

use std::collections::{BTreeMap, BTreeSet};
use std::sync::Arc;

use itertools::Itertools;

use crate::datastructures::UbTree;
use crate::formulas::{EncodedFormula, FormulaFactory, Literal, LIT_PRECEDENCE};

/// This transformation performs subsumption on a given CNF and returns a new
/// CNF. I.e. performs as many subsumptions as possible.
///
/// A subsumption in a CNF means, that e.g. a clause `A | B | C` is subsumed by
/// another clause `A | B` and can therefore be deleted for an equivalent CNF.
pub fn cnf_subsumption(formula: EncodedFormula, f: &FormulaFactory) -> EncodedFormula {
    assert!(formula.is_cnf(f), "CNF subsumption can only be applied to formulas in CNF");
    if formula.precedence() >= LIT_PRECEDENCE || formula.is_or() {
        formula
    } else {
        assert!(formula.is_and());
        let ub_tree = generate_subsumed_ubtree(formula, f);
        let mut clauses = Vec::new();
        for literals in ub_tree.all_sets() {
            clauses.push(f.clause(&literals.iter().copied().collect_vec()));
        }
        f.and(&clauses)
    }
}

/// This transformation performs subsumption on a given DNF and returns a new
/// DNF. I.e. performs as many subsumptions as possible.
///
/// A subsumption in a DNF means, that e.g. a minterm {@code A & B & C} is
/// subsumed by another minterm {@code A & B} and can therefore be deleted for
/// an equivalent DNF.
pub fn dnf_subsumption(formula: EncodedFormula, f: &FormulaFactory) -> EncodedFormula {
    assert!(formula.is_dnf(f), "DNF subsumption can only be applied to formulas in DNF");
    if formula.precedence() >= LIT_PRECEDENCE || formula.is_and() {
        formula
    } else {
        assert!(formula.is_or());
        let ub_tree = generate_subsumed_ubtree(formula, f);
        let mut minterms = Vec::new();
        for literals in ub_tree.all_sets() {
            minterms.push(f.and(&literals.iter().map(|&l| EncodedFormula::from(l)).collect::<Box<[_]>>()));
        }
        f.or(&minterms)
    }
}

fn generate_subsumed_ubtree(formula: EncodedFormula, f: &FormulaFactory) -> UbTree<Literal> {
    let mut mapping: BTreeMap<usize, Vec<Arc<BTreeSet<Literal>>>> = BTreeMap::new();
    for &term in &*formula.operands(f) {
        let literals = term.literals(f);
        mapping.entry(literals.len()).or_default().push(literals);
    }
    let mut ub_tree = UbTree::new();
    for (_, value) in mapping {
        for set in value {
            if ub_tree.first_subset(set.as_ref()).is_none() {
                ub_tree.add_set((*set).clone());
            }
        }
    }
    ub_tree
}