/batsat

A Rust SAT solver originally based on MiniSat

Primary LanguageRustOtherNOASSERTION

BatSat

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

build status

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)