BatSat

This is a Rust SAT solver forked from ratsat, a reimplementation of MiniSat.

For reference, a simple benchmark comparing it to minisat on a set of (easy) problems.

License

MIT licensed.

Features and Goals

Batsat is originally based on ratsat, a clone of minisat. However we want to extend batsat further and to provide the following features:

• proof production (in DRAT)
• easy access to unsat-cores (as subset of assumptions)
• ipasir interface for incremental solving
  • testing this interface
• debug framework using log (optional)
• OCaml bindings
• templated API to write SMT solvers
• simplification techniques from Minisat+ (as an optional internal structure)