1%\documentclass[12pt]{article} 2 3%\usepackage{alltt} 4%\usepackage{epsfig} 5%\usepackage{pstricks} 6%\usepackage{xspace} 7%\usepackage{url} 8%\usepackage{makeidx} 9%\usepackage{index} 10%\usepackage{multind} 11 12 13\renewcommand{\t}[1]{\mbox{\small\tt #1}} 14%\newcommand{\prev}[1]{#1} 15 16%\newcommand{\varord}[1]{#1} 17 18%\newcommand{\ma}[1]{{{$#1$}}} 19%\newcommand{\id}[1]{#1} 20 21\newcommand\Hol{HOL} 22 23%\newcommand{\els}{\mid} 24%\newcommand{\Imp}{\Rightarrow} 25 26%\renewcommand{\prod}{\mbox{\tt{*}}} 27%\newcommand{\SP}{~} 28%\newcommand{\SPP}{~} 29 30%\newcommand{\homedir}{\mbox{$\sim$}} 31 32%\newcommand{\Turn}{\(\turn\)} 33%\newcommand{\And}{\(\wedge\)} 34%\newcommand{\Or}{\(\vee\)} 35%\newcommand{\Not}{\(\neg\)} 36%\newcommand{\Forall}{\(\forall\)} 37%\newcommand{\Exists}{\(\exists\)} 38%\newcommand{\Mapsto}{\(\mapsto\)} 39 40%\input{../LaTeX/commands} 41 42\setcounter{sessioncount}{0} 43 44%\begin{document} 45\index{HolSatLib|(} 46\index{SAT solvers|see {HolSatLib}} 47\index{decision procedures!propositional satisfiability} 48 49The 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. 50 51{\tt{HolSatLib}} provides a function {\tt SAT\_PROVE} \index{HolSatLib!SAT\_PROVE@\ml{SAT\_PROVE}} for propositional satisfiability testing and for proving propositional tautologies. It uses an external SAT solver (currently MiniSat 1.14p) to find an unsatisfiability proof or satisfying assignment, and then reconstructs the proof or checks the assignment deductively in \HOL. 52 53Alternatively, 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. 54 55The following example illustrates the use of {\tt{HolSatLib}} for proving propositional tautologies: 56 57\begin{session} 58\begin{verbatim} 59- load "HolSatLib"; open HolSatLib; 60(* output omitted *) 61> val it = () : unit 62 63- show_tags := true; 64> val it = () : unit 65 66- SAT_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; 67> val it = [oracles: DISK_THM] [axioms: ] [] 68 |- (a ==> b) /\ (b ==> a) = (a = b) : thm 69 70- SAT_PROVE ``(a ==> b) ==> (a=b)`` 71 handle HolSatLib.SAT_cex th => th; 72> val it = [oracles: DISK_THM] [axioms: ] [] 73 |- ~a /\ b ==> ~((a ==> b) ==> (a = b)) : thm 74 75- SAT_ORACLE ``(a ==> b) /\ (b ==> a) = (a=b)``; 76> val it = [oracles: DISK_THM, HolSatLib] [axioms: ] [] 77 |- (a ==> b) /\ (b ==> a) = (a = b) : thm 78\end{verbatim} 79\end{session} 80 81Setting \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. 82 83Note that in the case where the putative tautology has a falsifying interpretation, a counter-model can be obtained by capturing the special exception {\tt{SAT\_cex}}, which contains a theorem asserting the counter-model. 84 85The next example illustrates using {\tt{HolSatLib}} for satisfiability testing. The idea is to negate the target term before passing it to {\tt{HolSatLib}}. 86 87\begin{session} 88\begin{verbatim} 89- SAT_PROVE ``~((a ==> b) ==> (a=b))`` 90 handle HolSatLib.SAT_cex => th; 91> val it = [oracles: DISK_THM ] [axioms: ] [] 92 |- a /\ ~b ==> ~~((a ==> b) ==> (a = b)) : thm 93 94- SAT_PROVE ``~(a /\ ~a)``; 95> val it = [oracles: DISK_THM ] [axioms: ] [] 96 |- ~(a /\ ~a) : thm 97\end{verbatim} 98\end{session} 99 100As expected, if the target term is unsatisfiable we get a theorem saying as much. 101 102{\tt{HolSatLib}} can only handle purely propositional terms (atoms must be propositional variables or constants) involving the usual propositional connectives as well as Boolean-valued conditionals. If you wish to prove tautologies that are instantiations of propositional terms, use {\tt{tautLib}} (see \S\ref{tautlib} below). 103 104If MiniSat failed to build when \HOL{} was built, or proof replay fails for some other reason, \t{SAT\_PROVE} falls back to a DPLL-based propositional tautology prover implemented in SML, due to Michael Norrish (see the \HOL{} Tutorial). {\tt{HolSatLib}} prints out a warning if this happens. On problems with more than a thousand or so clauses (in conjunctive normal form (CNF)), the SML prover will likely take too long to be of any use. 105 106{\tt{HolSatLib}} will delete temporary files generated by the SAT solver, such as the proof file and any statistics. This is to avoid accumulating thousands of possibly large files. Currently {\tt HolSatLib} has only been tested on Linux, and on Windows XP using MinGW. 107 108\subsection{{\tt tautLib}}\label{tautlib} 109 110{\tt tautLib} predates {\tt{HolSatLib}} by over a decade. It used a Boolean case analysis algorithm suggested by Tom Melham and implemented by R.~J.~Boulton. This algorithm has since been superseded and the functions in the {\tt tautLib} signature now act as wrappers around calls to {\tt{HolSatLib}}. However, the wrappers are able to provide the following extra functionality on top of {\tt{HolSatLib}}: 111 112\begin{enumerate} 113\item They can handle top level universal quantifiers. 114\item They can reason about (the propositional structure of) terms that are instances of purely propositional terms. This is done by a preprocessing step that replaces each unique instantiation with a fresh propositional variable. 115\end{enumerate} 116 117For details, see the source file \t{src/taut/tautLib.sml} which contains comprehensive comments. Note however that the extra functionality in {{\tt tautLib}} was not engineered for very large problems and can become a performance bottleneck. 118 119\subsection{Support for other SAT solvers}\label{subsec:hs_zchaff} 120 121The 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}. 122 123A file \texttt{resolve\_trace} may be created in the current working directory, when working with ZChaff. This is the proof trace file produced by ZChaff, and is hardwired. 124 125Other SAT solvers are currently not supported. If you would like such support to be added for your favourite solver, please send a feature request via \url{http://github.com/mn200/HOL}. 126 127\subsection{The general interface} 128 129The 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: 130 131\begin{enumerate} 132\item{\texttt{term : Term.term}} 133 134The input term. 135\item{\texttt{solver : SatSolvers.sat\_solver}} 136 137The 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. 138\item{\texttt{infile : string option}} 139 140The 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. 141\item{\texttt{proof : string option}} 142 143The 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. 144\item{\texttt{is\_cnf : bool}} 145 146If true then the input term is expected to be a negated CNF term. This is set automatically if \texttt{infile} is set. Typically a user will never need to modify this field directly. 147\item{\texttt{is\_proved : bool}} 148 149If true then \HOL{} will prove the SAT solver's results. 150\end{enumerate} 151 152A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver is MiniSat, the options are unset, the CNF flag is false and the proof flag is true. This value can be inspected and modified using getter and setter functions provided in \texttt{src/HolSat/satConfig.sig}. For example, to invoke ZChaff (assuming it is installed), on a file \texttt{unsat.cnf} containing an unsatisfiable problem, we do: 153 154\begin{session} 155\begin{verbatim} 156- open satConfig; 157(* output omitted *) 158 159- val c = (set_infile "unsat.cnf" o set_solver SatSolvers.zchaff) base_config; 160> val c = <sat_config> : sat_config 161 162- GEN_SAT c; 163> val it = [oracles: DISK_THM ] [axioms: ] [] 164 |- ~<unsat.cnf term here> : thm 165\end{verbatim} 166\end{session} 167 168If the problem were satisfiable, the model can be captured via exception, as shown earlier. 169 170Normally, {\tt{HolSatLib}} will delete the files generated by the SAT solver, such as the output proof, counter-model, and result status. However, if \texttt{infile} is set, the files are not deleted, in case they are required elsewhere. 171 172\subsection{Notes} 173 174On Linux and MacOS, \texttt{g++} must be installed on the system for MiniSat and \texttt{zc2hs} to build. 175 176Temporary files are generated using the Moscow ML function \t{FileSys.tmpName}. This usually writes to the standard temporary file space on the operating system. If that file space is full, or if it is inaccessible for some other reason, {\tt{HolSatLib}} calls may fail mysteriously. 177 178The function {\tt dimacsTools.readDimacs}~{\it file} reads a DIMACS format file and returns 179a CNF \HOL{} term corresponding to the SAT problem in the file named by {\it file}. Since DIMACS uses numbers to denote variables, and numbers are not legal identifiers in \HOL{}, each variable number is prefixed with the string ``{\tt v}''. This string is defined in the reference variable {\tt dimacsTools.prefix} and can be changed if required. This function can be used independently of {\tt{HolSatLib}} to read in DIMACS format files. 180 181\index{HolSatLib|)} 182 183%\end{document} 184%%% Local Variables: 185%%% mode: latex 186%%% TeX-master: "description" 187%%% End: 188