PlatSat

This is a Rust SAT solver forked from batsat 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.

Platsat changes

• #![forbid(unsafe_code)]
• no_std
• added API to make implementing push/pop easier
• optimized adding lemmas from an SMT theory

BREAKING CHANGES

• renamed Theory::explain_propagation to Theory::explain_propagation_clause and changed the required form of the explanation

Platsat extends batsat by making it safe () and , as well as improving the SMT solver API

Batsat 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