otter_sat/config/
vsids.rs

1/*!
2Ways to apply VSIDS (variable state independent decay sum) during during resolution-based analysis.
3
4See [Understanding VSIDS branching heuristics in conflict-driven clause-learning sat solvers](https://arxiv.org/abs/1506.08905) for an overview of VSIDS .
5*/
6
7use std::str::FromStr;
8
9/// Supported VSIDS variants.
10#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
11#[allow(clippy::upper_case_acronyms)]
12pub enum VSIDS {
13    /// A variant which mimics the VSIDS used by [Chaff](https://dl.acm.org/doi/10.1145/378239.379017).\
14    /// When learning a clause by applying resolution to a sequence of clauses every atom occurring in the learnt clause is bumped.
15    Chaff = 0,
16
17    /// A variant which mimics the VSIDS used by [MiniSAT](https://link.springer.com/chapter/10.1007/978-3-540-24605-3_37).\
18    /// When learning a clause by applying resolution to a sequence of clauses every atom occurring in some clause used during resolution (including the learnt clause) is bumped.
19    MiniSAT,
20}
21
22impl std::fmt::Display for VSIDS {
23    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
24        match self {
25            Self::Chaff => write!(f, "Chaff"),
26            Self::MiniSAT => write!(f, "MiniSAT"),
27        }
28    }
29}
30
31impl VSIDS {
32    /// The minimum VSIDS type.
33    pub const MIN: VSIDS = VSIDS::Chaff;
34
35    /// The maximum VSIDS type.
36    pub const MAX: VSIDS = VSIDS::MiniSAT;
37}
38
39impl FromStr for VSIDS {
40    type Err = ();
41
42    fn from_str(s: &str) -> Result<Self, Self::Err> {
43        match s {
44            "Chaff" => Ok(Self::Chaff),
45            "MiniSAT" => Ok(Self::MiniSAT),
46            _ => Err(()),
47        }
48    }
49}
otter_sat/config/vsids.rs

otter_sat/config/
vsids.rs
