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
//! Varisat is a [CDCL][cdcl] based SAT solver written in rust. Given a boolean formula in //! [conjunctive normal form][cnf], it either finds a variable assignment that makes the formula //! true or finds a proof that this is impossible. //! //! In addition to this API documentation, Varisat comes with a [user manual]. //! //! [cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning //! [cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form //! [user manual]: https://jix.github.io/varisat/manual/0.2.0/ #[macro_use] pub mod lit; pub mod checker; pub mod cnf; pub mod dimacs; pub mod solver; mod analyze_conflict; mod binary; mod cdcl; mod clause; mod context; mod decision; mod glue; mod incremental; mod load; mod proof; mod prop; mod schedule; mod simplify; mod state; mod tmp; mod vec_mut_scan; #[cfg(test)] mod test;