IT/Description/HolSat.tex

49 The purpose of {\tt{HolSatLib}} is to provide a platform for experimenting with combinations of theorem proving and SAT solvers. Only black box functionality is provided at the moment; an incremental interface is not available.
53 Alternatively, the function {\tt SAT\_ORACLE} \index{HolSatLib!SAT\_ORACLE@\ml{SAT\_ORACLE}} has the same behaviour as {\tt SAT\_PROVE} but asserts the result of the solver without proof. The theorem thus asserted is tagged with ``{\tt{HolSatLib}}'' to indicate that it is unchecked. Since proof reconstruction can be expensive, the oracle facility can be useful during prototyping, or if proof is not required.
55 The following example illustrates the use of {\tt{HolSatLib}} for proving propositional tautologies:
81 Setting \t{show\_tags} to \t{true} makes the \HOL{} top-level print theorem tags. The \t{DISK\_THM} oracle tag has nothing to do with \t{HolSatLib}. It just indicates the use of theorems from \HOL{} libraries read in from permanent storage.
85 The next example illustrates using {\tt{HolSatLib}} for satisfiability testing. The idea is to negate the target term before passing it to {\tt{HolSatLib}}.
121 The ZChaff SAT solver has a proof production mode and is supported by {\tt{HolSatLib}}. However, the ZChaff end user license is not compatible with the \HOL{} license, so we are unable to distribute it with \HOL{}. If you wish to use ZChaff, download and unpack it in the directory {\tt src/HolSat/sat\_solvers/} under the main \HOL{} directory, and compile it with proof production mode enabled (which is not the default). This should create a binary {\tt zchaff} in the directory {\tt src/HolSat/sat\_solvers/zchaff/}. ZChaff can now be used as the external proof engine instead of MiniSat, by using the HolSatLib functions described above, prefixed with a ``{\tt Z}'', e.g., {\tt ZSAT\_PROVE}.
127 \subsection{The general interface}
129 The functions described above are wrappers for the function \texttt{GEN\_SAT}, which is the single entry point for {\tt{HolSatLib}}. \texttt{GEN\_SAT} can be used directly if more flexibility is required. \texttt{GEN\_SAT} takes a single argument, of type \texttt{sat\_config}, defined in \texttt{satConfig.sml}. This is an opaque record type, currently containing the following fields:
134 The input term.
137 The external SAT solver to use. The default is \texttt{SatSolvers.minisatp}. If ZChaff is installed (see \S\ref{subsec:hs_zchaff}), then \texttt{SatSolvers.zchaff} may also be used.
140 The name of a file in DIMACS format.\footnote{\url{http://www.satlib.org/Benchmarks/SAT/satformat.ps}}. Overrides \texttt{term} if set. The input term is instead read from the file.
143 The name of a proof trace file. Overrides \texttt{solver} if set. The file must be in the native format of {\tt{HolSatLib}}, and must correspond to a proof for \texttt{infile}, which must also be set. The included version of MiniSat has been modified to produce proofs in the native format, and ZChaff proofs are translated to this format using the included proof translator \texttt{src/HolSat/sat\_solvers/zc2hs} (type \texttt{zc2hs -h} for usage help). \texttt{zc2hs} is used internally by \texttt{ZSAT\_PROVE} etc.
178 The function {\tt dimacsTools.readDimacs}~{\it file}  reads a DIMACS format file and returns