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

use std::time::Duration;

/// Counts for various things which count, roughly.
pub struct Counters {
    /// A count of every conflict seen during a solve.
    pub total_conflicts: usize,

    /// A count of conflicts seen since the last restart.
    ///
    /// As u32 rather than a usize for easier interaction with scheduling variables.
    pub fresh_conflicts: u32,

    /// A count of all decisions made.
    pub total_decisions: usize,

    /// The total number of iterations through a solve.
    pub total_iterations: usize,

    /// The number of restarts through a solve.
    pub restarts: usize,

    /// The time taken during a solve.
    pub time: Duration,

    /// The current element in the luby sequence.
    pub luby: crate::generic::luby::Luby,
}

impl Default for Counters {
    fn default() -> Self {
        Counters {
            fresh_conflicts: 0,

            total_decisions: 0,
            total_iterations: 0,
            total_conflicts: 0,

            restarts: 0,
            time: Duration::from_secs(0),

            luby: crate::generic::luby::Luby::default(),
        }
    }
}