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

#![deny(missing_docs)]

//! `rsat` is a SAT Solver.
//!
//! ## An example using the CDCL solver
//!
//! ```rust
//! use rsat::cdcl::{Solver, SolverOptions};
//! use solhop_types::{Var, Solution};
//!
//! let options = SolverOptions::default();
//! let mut solver = Solver::new(options);
//! let vars: Vec<Var> = solver.new_vars(3);
//! solver.add_clause(vec![vars[0].pos_lit()]);
//! solver.add_clause(vec![vars[1].neg_lit()]);
//! solver.add_clause(vec![vars[0].neg_lit(), vars[1].pos_lit(), vars[2].pos_lit()]);
//!
//! assert_eq!(solver.solve(vec![]), Solution::Sat(vec![true, false, true]));
//!
//! assert_eq!(solver.solve(vec![vars[2].neg_lit()]), Solution::Unsat);
//!
//! assert_eq!(solver.solve(vec![]), Solution::Sat(vec![true, false, true]));
//!
//! solver.add_clause(vec![vars[2].neg_lit()]);
//! assert_eq!(solver.solve(vec![]), Solution::Unsat);
//! ```

/// Stochastic local search solver module.
pub mod sls;

/// CDCL solver module.
pub mod cdcl;