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
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

use crate::formulas::{EncodedFormula, FormulaFactory};
use crate::handlers::{ClauseLimitFactorizationHandler, FactorizationHandler};
use crate::operations::transformations::cnf::CnfAlgorithm::Tseitin;
use crate::operations::transformations::cnf::{CancellableCnfAlgorithm, CnfAlgorithm};

use super::CnfEncoder;

/// Constructs the _CNF_ of a formula with factorization and the given
/// [`AdvancedFactorizationConfig`].
pub fn advanced_cnf_encoding(
    formula: EncodedFormula,
    f: &FormulaFactory,
    config: &AdvancedFactorizationConfig,
    state: &mut CnfEncoder,
) -> EncodedFormula {
    if formula.is_and() {
        let new_ops = formula.operands(f).iter().map(|&op| single_advanced_encoding(op, f, config, state)).collect::<Box<[_]>>();
        f.and(&new_ops)
    } else {
        single_advanced_encoding(formula, f, config, state)
    }
}

fn single_advanced_encoding(
    formula: EncodedFormula,
    f: &FormulaFactory,
    config: &AdvancedFactorizationConfig,
    state: &mut CnfEncoder,
) -> EncodedFormula {
    CancellableCnfAlgorithm::FactorizationWithHandler(config.handler())
        .transform(formula, f)
        .unwrap_or_else(|_| (*config.fallback_algorithm).transform(formula, f, state))
}

/// Configuration for advanced _CNF_ algorithms.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct AdvancedFactorizationConfig {
    distribution_boundary: u64,
    created_clause_boundary: u64,
    atom_boundary: u64,
    fallback_algorithm: Box<CnfAlgorithm>,
}

impl Default for AdvancedFactorizationConfig {
    fn default() -> Self {
        Self { distribution_boundary: u64::MAX, created_clause_boundary: 1000, atom_boundary: 12, fallback_algorithm: Box::new(Tseitin) }
    }
}

impl AdvancedFactorizationConfig {
    /// Sets the boundary how many distributions should be performed in the
    /// factorization before the method is switched.
    #[must_use]
    pub const fn distribution_boundary(mut self, distribution_boundary: u64) -> Self {
        self.distribution_boundary = distribution_boundary;
        self
    }

    /// Sets the boundary how many clauses should be created in the
    /// factorization before the method is switched.
    #[must_use]
    pub const fn created_clause_boundary(mut self, created_clause_boundary: u64) -> Self {
        self.created_clause_boundary = created_clause_boundary;
        self
    }

    /// Sets the boundary for how many atoms in a formula factorization is
    /// performed in Tseitin and Plaisted & Greenbaum.
    ///
    /// The default value is 12.
    #[must_use]
    pub const fn atom_boundary(mut self, atom_boundary: u64) -> Self {
        self.atom_boundary = atom_boundary;
        self
    }

    /// Sets the fallback algorithm for the advanced CNF encoding. When the
    /// boundaries for the factorization are met, the encoding switches to this
    /// algorithm.
    ///
    /// The default value is [`CnfAlgorithm::TSEITIN`](`CnfAlgorithm`).
    #[must_use]
    pub fn fallback_algorithm(mut self, fallback_algorithm: CnfAlgorithm) -> Self {
        self.fallback_algorithm = Box::new(fallback_algorithm);
        self
    }

    /// Creates an new handler based on this configuration.
    pub fn handler(&self) -> Box<dyn FactorizationHandler> {
        Box::new(ClauseLimitFactorizationHandler::new(self.distribution_boundary, self.created_clause_boundary))
    }
}