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

use crate::structures::literal::CLiteral;

/// Cells of a resolution buffer.
#[derive(Clone, Copy)]
pub enum Cell {
    /// Initial valuation
    Value(Option<bool>),

    /// The atom was not valued.
    None(CLiteral),

    /// The atom had a conflicting value.
    Conflict(CLiteral),

    /// The atom was part of resolution but was already proven.
    Strengthened,

    /// The atom was used as a pivot when reading a clause into the buffer.
    Pivot,
}