otter_sat 0.1.0

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
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

/*!
Miscelanous items related to [logging](log).

Calls to the log macro are made throughout the library.
These are intended to provide useful information for extending the library and/or fixing issues.

Note, no log implementation is provided.
For more details, see [log].
*/

/// Targets to be used within a [log]! macro.
pub mod targets {
    /// Logs related to [BCP](crate::procedures::bcp)
    pub const PROPAGATION: &str = "propagation";

    /// Logs related to [analysis](crate::procedures::analysis)
    pub const ANALYSIS: &str = "analysis";

    /// Logs related to clause deletion
    pub const REDUCTION: &str = "reduction";

    /// Logs related to the [clause database](crate::db::clause)
    pub const CLAUSE_DB: &str = "clause_db";

    /// Logs related to a valuation
    pub const VALUATION: &str = "valuation";

    /// Logs related to [backjumping](crate::procedures::backjump)
    pub const BACKJUMP: &str = "backjump";

    /// Logs related to preprocessing
    pub const PREPROCESSING: &str = "preprocessing";

    /// Logs related to [resolution](crate::resolution_buffer)
    pub const RESOLUTION: &str = "resolution";

    /// Logs related to subsumption
    pub const SUBSUMPTION: &str = "subsumption";

    /// Logs related to the [consequence queue](crate::db::consequence_q)
    pub const QUEUE: &str = "queue";
}