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.
MIT licensed.
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)