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

/// The source of a clause.
#[derive(Clone, Copy)]
pub enum ClauseSource {
    /// A *unit* clause obtained via BCP.
    BCP,

    /// A *unit* clause set by free decision on the value of the contained atom.
    PureUnit,

    /// A clause read from a formula.
    Original,

    /// A clause derived via resolution (during analysis, etc.)
    Resolution,
}