[Caml-list] [ANN] mSAT 0.6

[Caml-list] [ANN] mSAT 0.6

[Guillaume Bury]

Hello,

I have the pleasure to announce the release of mSAT 0.6 [0], a modular
SAT-solver library in pure OCaml. SAT solvers are useful for NP-complete
constraint solving, and are commonly used directly in many tools
(including the package manager of eclipse), or indirectly as part of
SMT solvers (Satisfiability Modulo Theory).

mSAT is a modernized fork of alt-ergo-zero[1] that can be used both as a
pure SAT solver, and as a building block for writing SMT solvers.
To write a SMT solver based on mSAT, there is a functor that can be
instantiated with a custom term structure and a custom theory
responsible for propagation, following the Lazy SMT framework.  The
functor also provides an interface for MCSat-style solvers.
mSAT is also proof-producing (it can output boolean resolution proofs),
model-producing, and can output unsat-cores.
Its flexibility and availability as an OCaml library make it useful for
writing SMT solvers that feature experimental theories or theory
implementations. The documentation can be found online [2].

Performance-wise, mSAT should be in the fast end of what OCaml makes
possibles. Obviously, state of the art C solvers (minisat, picosat,
etc.) are still much better.

mSAT is developed by Guillaume Bury and Simon Cruanes, and available
on opam as "msat", under the permissive Apache license.

[0] https://github.com/Gbury/mSAT
[1] http://cubicle.lri.fr/alt-ergo-zero/
[2] https://gbury.github.io/mSAT/

-- 
Guillaume Bury