The HOL library HolSatLib provides a very simple harness for invoking SAT solvers on HOL terms. Currently the following solvers are supported
These solvers all require input in the standard DIMACS format for conjunctive normal form (CNF). It should be straightforward to add other DIMACS compatible SAT solvers.
The purpose of HolSatLib is to provide a platform for experimenting with combinations of theorem proving and SAT. HOL-4 can be used to deductively manipulate terms into CNF as required for SAT analysis, and then the results of the analysis can be reimported into HOL and either checked or just trusted.
HolSatLib has only been tested under Linux, though it should be possible to run it under Windows.
MICHAEL J. C. GORDON