splr/solver/
mod.rs

1/// Module `solver` provides the top-level API as a SAT solver.
2/// API to instantiate
3mod build;
4/// Module 'conflict' handles conflicts.
5mod conflict;
6/// Module `restart` provides restart heuristics.
7pub mod restart;
8/// CDCL search engine
9mod search;
10/// Stage manger (was Stabilizer)
11mod stage;
12/// Module `validate` implements a model checker.
13mod validate;
14
15pub use self::{
16    build::SatSolverIF,
17    restart::{RestartIF, RestartManager},
18    search::SolveIF,
19    stage::StageManager,
20    validate::ValidateIF,
21};
22
23use crate::{assign::AssignStack, cdb::ClauseDB, state::*, types::*};
24
25/// Normal results returned by Solver.
26#[derive(Debug, Eq, PartialEq)]
27pub enum Certificate {
28    /// It is satisfiable; `vec` is such an assignment sorted by var order.
29    SAT(Vec<i32>),
30    /// It is unsatisfiable.
31    UNSAT,
32}
33
34/// The return type of `Solver::solve`.
35/// This captures the following three cases:
36/// * `Certificate::SAT` -- solved with a satisfiable assignment set,
37/// * `Certificate::UNSAT` -- proved that it's an unsatisfiable problem, and
38/// * `SolverError::*` -- caused by a bug
39pub type SolverResult = Result<Certificate, SolverError>;
40
41/// define sub-modules' responsibilities
42#[derive(Clone, Copy, Debug, Eq, PartialEq)]
43pub enum SolverEvent {
44    /// asserting a var.
45    Assert(VarId),
46    /// conflict by unit propagation.
47    Conflict,
48    /// eliminating a var.
49    Eliminate(VarId),
50    /// Not in use
51    Instantiate,
52    /// increment the number of vars.
53    NewVar,
54    /// re-initialization for incremental solving.
55    Reinitialize,
56    /// restart
57    Restart,
58    /// start a new stage of Luby stabilization. It holds new scale.
59    Stage(usize),
60
61    #[cfg(feature = "clause_vivification")]
62    /// Vivification: `true` for start, `false` for end.
63    Vivify(bool),
64}
65
66/// The SAT solver object consisting of 6 sub modules.
67/// ```
68/// use crate::splr::*;
69/// use crate::splr::{assign::{AssignIF, VarManipulateIF}, state::{State, StateIF}, types::*};
70/// use std::path::Path;
71///
72/// let mut s = Solver::try_from(Path::new("cnfs/sample.cnf")).expect("can't load");
73/// assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250);
74/// assert_eq!(s.asg.derefer(assign::property::Tusize::NumUnassertedVar), 250);
75/// if let Ok(Certificate::SAT(v)) = s.solve() {
76///     assert_eq!(v.len(), 250);
77///     // But don't expect `s.asg.var_stats().3 == 0` at this point.
78///     // It returns the number of vars which were assigned at decision level 0.
79/// } else {
80///     panic!("It should be satisfied!");
81/// }
82/// assert_eq!(Solver::try_from(Path::new("cnfs/unsat.cnf")).expect("can't load").solve(), Ok(Certificate::UNSAT));
83/// ```
84#[derive(Clone, Debug, Default)]
85pub struct Solver {
86    /// assignment management
87    pub asg: AssignStack,
88    /// clause container
89    pub cdb: ClauseDB,
90    /// misc data holder
91    pub state: State,
92}
93
94/// Example
95///```
96/// use crate::splr::*;
97///
98/// let v: Vec<Vec<i32>> = vec![];
99/// assert!(matches!(
100///     Certificate::try_from(v),
101///     Ok(Certificate::SAT(_))
102/// ));
103/// assert!(matches!(
104///     Certificate::try_from(vec![vec![0_i32]]),
105///     Err(SolverError::InvalidLiteral)
106/// ));
107///
108/// // `Solver` has another interface.
109/// assert!(matches!(
110///     Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())),
111///     Err(Err(SolverError::InvalidLiteral))
112/// ));
113///```
114impl<V: AsRef<[i32]>> TryFrom<Vec<V>> for Certificate {
115    type Error = SolverError;
116    fn try_from(vec: Vec<V>) -> SolverResult {
117        Solver::try_from((Config::default(), vec.as_ref())).map_or_else(
118            |e: SolverResult| match e {
119                Ok(cert) => Ok(cert),
120                Err(SolverError::EmptyClause) => Ok(Certificate::UNSAT),
121                Err(e) => Err(e),
122            },
123            |mut solver| solver.solve(),
124        )
125    }
126}
127
128/// Iterator for Solver
129/// * takes `&mut Solver`
130/// * returns `Option<Vec<i32>>`
131///    * `Some(Vec<i32>)` -- satisfiable assignment
132///    * `None` -- unsatisfiable anymore
133/// * Some internal error causes panic.
134#[cfg(feature = "incremental_solver")]
135pub struct SolverIter<'a> {
136    solver: &'a mut Solver,
137    refute: Option<Vec<i32>>,
138}
139
140#[cfg(feature = "incremental_solver")]
141impl Solver {
142    /// return an iterator on Solver. **Requires 'incremental_solver' feature**
143    ///```ignore
144    ///use splr::Solver;
145    ///use std::path::Path;
146    ///
147    ///for v in Solver::try_from(Path::new("cnfs/sample.cnf")).expect("panic").iter() {
148    ///    println!(" - answer: {:?}", v);
149    ///}
150    ///```
151    pub fn iter(&mut self) -> SolverIter {
152        SolverIter {
153            solver: self,
154            refute: None,
155        }
156    }
157}
158
159#[cfg(feature = "incremental_solver")]
160impl<'a> Iterator for SolverIter<'a> {
161    type Item = Vec<i32>;
162    fn next(&mut self) -> Option<Self::Item> {
163        if let Some(ref v) = self.refute {
164            debug_assert!(1 < v.len());
165            match self.solver.add_clause(v) {
166                Err(SolverError::Inconsistent) => return None,
167                Err(SolverError::EmptyClause) => return None,
168                Err(e) => panic!("s UNKNOWN: {:?} by adding {:?}", e, v),
169                Ok(_) => self.solver.reset(),
170            }
171            self.refute = None;
172        }
173        match self.solver.solve() {
174            Ok(Certificate::SAT(ans)) => {
175                let rft: Vec<i32> = ans.iter().map(|i| -i).collect::<Vec<i32>>();
176                self.refute = Some(rft);
177                Some(ans)
178            }
179            Ok(Certificate::UNSAT) => None,
180            e => panic!("s UNKNOWN: {:?}", e),
181        }
182    }
183}
184
185#[cfg(test)]
186mod tests {
187    use super::*;
188    use crate::assign;
189
190    #[cfg_attr(not(feature = "no_IO"), test)]
191    fn test_solver() {
192        let config = Config::from("cnfs/sample.cnf");
193        if let Ok(s) = Solver::build(&config) {
194            assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250);
195            assert_eq!(
196                s.asg.derefer(assign::property::Tusize::NumUnassertedVar),
197                250
198            );
199        } else {
200            panic!("failed to build a solver for cnfs/sample.cnf");
201        }
202    }
203
204    macro_rules! run {
205        ($vec: expr) => {
206            println!(
207                "{:>46} =| {:?}",
208                format!("{:?}", $vec),
209                match Solver::try_from((Config::default(), $vec.as_ref())).map(|mut s| s.solve()) {
210                    Err(e) => e,
211                    Ok(Ok(u @ Certificate::UNSAT)) => Ok(u),
212                    Ok(s) => s,
213                }
214            );
215        };
216    }
217
218    macro_rules! sat {
219        ($vec: expr, $should_be: pat) => {
220            println!("{:>46} =| ", format!("{:?}", $vec));
221            let result = Certificate::try_from($vec);
222            println!("{:?}", result);
223            assert!(matches!(result, $should_be));
224        };
225        ($vec: expr) => {
226            println!(
227                "{:>46} =| {:?}",
228                format!("{:?}", $vec),
229                Certificate::try_from($vec)
230            );
231        };
232    }
233
234    #[test]
235    fn test_on_memory_solving() {
236        let mut v: Vec<Vec<i32>> = Vec::new();
237        run!(v);
238        v.push(Vec::new());
239        run!(v);
240        run!(vec![vec![1]]);
241        run!(vec![vec![1], vec![-1]]);
242        run!(vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]);
243        run!(vec![
244            vec![1, 2],
245            vec![-1, 3],
246            vec![1, -3],
247            vec![-1, -2],
248            vec![-2, -3]
249        ]);
250        run!(vec![
251            vec![1, 2],
252            vec![-1, 3],
253            vec![-1, -3],
254            vec![-1, -2],
255            vec![1, -2]
256        ]);
257
258        // auto conversion via `as_ref`
259        let (v1, v2, v3, v4, v5) = (vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2], vec![-3]);
260        run!(vec![&v1, &v2, &v3, &v4, &v5]); // : Vec<&[i32]>
261        run!([&v1, &v2, &v3, &v4, &v5]); // [&[i32]; 5]
262
263        // let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
264        // let s = Solver::try_from((Config::default(), v.as_ref()));
265        // match s.map_or_else(|e| e, |mut solver| solver.solve()) {
266        //     Ok(Certificate::SAT(ans)) => println!("s SATISFIABLE: {:?}", ans),
267        //     Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"),
268        //     Err(e) => panic!("{}", e),
269        // }
270        let v0: Vec<Vec<i32>> = vec![];
271        sat!(v0, Ok(Certificate::SAT(_)));
272        let v1: Vec<Vec<i32>> = vec![vec![]];
273        sat!(v1, Ok(Certificate::UNSAT));
274        sat!(vec![vec![1i32]], Ok(Certificate::SAT(_)));
275        sat!(vec![vec![1i32], vec![-1]], Ok(Certificate::UNSAT));
276        sat!(vec![vec![1i32, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]);
277        sat!(vec![
278            vec![1i32, 2],
279            vec![-1, 3],
280            vec![1, -3],
281            vec![-1, -2],
282            vec![-2, -3]
283        ]);
284        sat!(vec![
285            vec![1i32, 2],
286            vec![-1, 3],
287            vec![-1, -3],
288            vec![-1, -2],
289            vec![1, -2]
290        ]);
291        let (v1, v2, v3, v4, v5) = (
292            vec![1i32, 2],
293            vec![-1i32, 3],
294            vec![1i32, -3],
295            vec![-1i32, 2],
296            vec![-3i32],
297        );
298        sat!(vec![&v1, &v2, &v3, &v4, &v5]); // : Vec<&[i32]>
299    }
300
301    #[cfg(feature = "incremental_solver")]
302    #[test]
303    fn test_solver_iter() {
304        let mut slv = Solver::instantiate(
305            &Config::default(),
306            &CNFDescription {
307                num_of_variables: 8,
308                ..CNFDescription::default()
309            },
310        );
311        assert_eq!(slv.iter().count(), 256);
312    }
313    #[cfg(feature = "incremental_solver")]
314    #[test]
315    fn test_add_var_on_incremental_solver() {
316        let mut slv = Solver::instantiate(
317            &Config::default(),
318            &CNFDescription {
319                num_of_variables: 4,
320                ..CNFDescription::default()
321            },
322        );
323        assert!(slv.add_clause(vec![-1, -2]).is_ok());
324        assert!(slv.add_clause(vec![-3, -4]).is_ok());
325        assert!(slv.add_assignment(-2).is_ok());
326        let a = slv.add_var() as i32;
327        assert!(slv.add_clause(vec![1, 3, 4, -a]).is_ok());
328        assert!(slv.add_clause(vec![1, -3, -4, -a]).is_ok());
329        assert!(slv.add_clause(vec![-1, 3, -4, -a]).is_ok());
330        assert!(slv.add_clause(vec![-1, -3, 4, -a]).is_ok());
331        assert!(slv.add_clause(vec![-1, -3, -4, a]).is_ok());
332        assert!(slv.add_clause(vec![-1, 3, 4, a]).is_ok());
333        assert!(slv.add_clause(vec![1, -3, 4, a]).is_ok());
334        assert!(slv.add_clause(vec![1, 3, -4, a]).is_ok());
335        let b = slv.add_var() as i32;
336        assert!(slv.add_clause(vec![1, 3, -b]).is_ok());
337        assert!(slv.add_clause(vec![1, 4, -b]).is_ok());
338        assert!(slv.add_clause(vec![3, 4, -b]).is_ok());
339        assert!(slv.add_clause(vec![-1, -3, b]).is_ok());
340        assert!(slv.add_clause(vec![-1, -4, b]).is_ok());
341        assert!(slv.add_clause(vec![-3, -4, b]).is_ok());
342        assert!(slv.add_clause(vec![-1, -b]).is_ok());
343        assert!(slv.add_clause(vec![-a, -b]).is_ok());
344        // let solns: Vec<Vec<i32>> = slv.iter().collect();
345        // Use the result of
346        // cargo run --features incremental_solver --example all-solutions -- cnfs/isseu-182.cnf
347        assert_eq!(slv.iter().count(), 4);
348    }
349    #[cfg(feature = "incremental_solver")]
350    #[test]
351    // There was an inconsistency in AssignStack::var_order.
352    fn test_add_var_and_add_assignment() {
353        let mut slv = Solver::instantiate(
354            &Config::default(),
355            &CNFDescription {
356                num_of_variables: 3 as usize,
357                ..CNFDescription::default()
358            },
359        );
360
361        slv.add_var();
362        assert!(slv.add_clause(vec![-1, 4]).is_ok());
363        slv.add_var();
364        assert!(slv.add_clause(vec![-2, 5]).is_ok());
365        slv.add_var();
366        assert!(slv.add_clause(vec![-1, -2, 6]).is_ok());
367        slv.add_var();
368        assert!(slv.add_clause(vec![-5, 7]).is_ok());
369        slv.add_var();
370        assert!(slv.add_clause(vec![-6, 8]).is_ok());
371        slv.add_var();
372        assert!(slv.add_clause(vec![-4, 9]).is_ok());
373        slv.add_var();
374        assert!(slv.add_clause(vec![-3, 10]).is_ok());
375        slv.add_var();
376        assert!(slv.add_clause(vec![-5, -3, 11]).is_ok());
377        assert!(slv.add_clause(vec![-6, -3, 11]).is_ok());
378        slv.add_var();
379        assert!(slv.add_clause(vec![-4, -3, 12]).is_ok());
380        assert!(slv.add_assignment(-11).is_ok());
381        assert!(slv.solve().is_ok());
382    }
383}
splr/solver/mod.rs

splr/solver/
mod.rs
