MathSAT 5

FM FBK
UniTN
An SMT Solver for Formal Verification & More

Using a 3rd-party SAT solver with MathSAT

Starting from version 5.2, it is possible to use an external, 3rd-party SAT solver as the DPLL engine of MathSAT.

The external SAT solver should implement the msat_ext_dpll_interface interface, and call a number of callback functions for interacting with the rest of MathSAT during the search.

We have created two example implementations using the Minisat (version 2.2.0) and Cleaneling (version 00g) SAT solvers. The code is available in the examples/extsat/ directory of the MathSAT distribution.

Contents Home
People
Documentation
Download
Publications
Links
mathsat [AT] fbk [DOT] eu
mathsat-announce mailing list