MathSAT 5

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.