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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

#![doc(html_root_url = "https://docs.rs/splr/0.7.0")]
/*!
# A modern CDCL SAT solver in Rust

Splr is a pure Rustic SAT solver, based on [Glucose 4.1](https://www.labri.fr/perso/lsimon/glucose/).
It adopts various research results on SAT solvers:

- CDCL, watch literals, and so on from [Minisat](http://minisat.se) and the ancestors
- Glucose-like dynamic blocking/forcing restarts based on [EMAs](https://arxiv.org/abs/1506.08905)
- heuristics adaptation
- pre/in-process simplification based on clause subsumption and variable elimination
- Chronological backtrack and non-chronological backjump
- Learning Rate Based Branching and Reason Side Rewarding
- Rephase
- Search stabilization
- clause vivification

*Many thanks to SAT researchers.*

# Examples

## Build a solver from a configuration based on a CNF file, then solve it.

```
use splr::*;

let config = Config::from("tests/sample.cnf");
if let Ok(mut s) = Solver::build(&config) {
    if let Ok(ans) = s.solve() {
        println!("{:?}", ans);
    }
}
```

## On-memory direct conversion from a vec to a solution

```
use {splr::*, std::convert::TryFrom};

let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
match Certificate::try_from(v).expect("panic!") {
    Certificate::UNSAT => 0,
    Certificate::SAT(vec) => vec.len(),
};
```

## Incremental solver

Splr provides 'incremental solver mode' if you built it with feature 'incremental_solver'.
This document covers extra functions only if you built it with `cargo doc --features incremental_solver`.

*/
/// Crate `assign` implements Boolean Constraint Propagation and decision var selection.
pub mod assign;
/// Crate `cdb` provides [`Clause`](`crate::cdb::Clause`) object and its manager [`ClauseDB`](`crate::cdb::ClauseDB`).
pub mod cdb;
/// Crate `config` provides solver's configuration and CLI.
pub mod config;
/// Crate `processor` implements a simplifier: clause subsumption and var elimination.
pub mod processor;
/// Crate `solver` provides the top-level API as a SAT solver.
pub mod solver;
/// Crate `state` is a collection of internal data.
pub mod state;
/// Crate `types` provides various building blocks, including some common traits.
pub mod types;

pub use {
    config::Config,
    solver::{Certificate, SatSolverIF, SolveIF, Solver, ValidateIF},
    types::{Ema, Ema2, EmaIF, PropertyDereference, PropertyReference, SolverError},
};

/// Splr version number.
pub const VERSION: &str = env!("CARGO_PKG_VERSION");

#[macro_use]
extern crate bitflags;