HolSatLib


The HOL library HolSatLib provides a very simple harness for invoking SAT solvers on HOL terms. Currently the following solvers are supported

Solver Home Page Download
SATO http://www.cs.uiowa.edu/~hzhang/sato.html ftp://cs.uiowa.edu/pub/hzhang/sato/sato.tar.gz
GRASP http://sat.inesc.pt/~jpms/grasp http://sat.inesc.pt/~jpms/grasp/sat-grasp.st.linux.tar.gz
ZCHAFF http://www.ee.princeton.edu/~chaff http://www.ee.princeton.edu/~chaff/zchaff/zchaff.2001.2.17.linux.gz

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
University of Cambridge
Computer Laboratory
Room FE19
William Gates Building
JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
work phone: +44 1223 334627
work fax: +44 1223 334678
email: mjcg@cl.cam.ac.uk