Shadowgraph

745commits

6contributors

6languages

Tech stack & purpose

MSAT is an OCaml library providing a modular SAT/SMT solver derived from Alt-Ergo Zero, capable of producing proofs. The project operates in the formal methods domain, implementing the CDCL(T) algorithm through a functor-based architecture that accepts custom formula representations and theory modules. Built in OCaml and using dune for builds, MSAT includes ready-to-use SAT solving capabilities, formula AST support via Tseitin conversion, and example applications such as a Sudoku solver demonstrating the CDCL(T) approach. The work was presented at ICFP 2017 and is authored by Gbury.