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:

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