HOL: Description

The HolSat Library

The purpose of 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.

HolSatLib provides a function 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.

Alternatively, the function SAT_ORACLE has the same behaviour as SAT_PROVE but asserts the result of the solver without proof. The theorem thus asserted is tagged with "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.

The following example illustrates the use of HolSatLib for proving propositional tautologies:

> load "HolSatLib"; open HolSatLib;   ... output elided ...

> show_tags := true;
val it = (): unit

> SAT_PROVE ``(a ==> b) /\ (b ==> a) <=> (a=b)``;
val it =
   [oracles: DISK_THM] [axioms: ] [] ⊢ (a ⇒ b) ∧ (b ⇒ a) ⇔ (a ⇔ b):
   thm

> SAT_PROVE ``(a ==> b) ==> (a=b)``
  handle HolSatLib.SAT_cex th => th;
val it =
   [oracles: DISK_THM] [axioms: ] [] ⊢ ¬a ∧ b ⇒ ¬((a ⇒ b) ⇒ (a ⇔ b)):
   thm

> SAT_ORACLE ``(a ==> b) /\ (b ==> a) <=> (a=b)``;
val it =
   [oracles: DISK_THM, HolSatLib] [axioms: ] []
   ⊢ (a ⇒ b) ∧ (b ⇒ a) ⇔ (a ⇔ b): thm

Setting show_tags to true makes the HOL top-level print theorem tags. The DISK_THM oracle tag has nothing to do with HolSatLib. It just indicates the use of theorems from HOL libraries read in from permanent storage.

Note that in the case where the putative tautology has a falsifying interpretation, a counter-model can be obtained by capturing the special exception SAT_cex, which contains a theorem asserting the counter-model.

The next example illustrates using HolSatLib for satisfiability testing. The idea is to negate the target term before passing it to HolSatLib.

> SAT_PROVE ``~((a ==> b) ==> (a=b))``
  handle HolSatLib.SAT_cex th => th;
val it =
   [oracles: DISK_THM] [axioms: ] [] ⊢ a ∧ ¬b ⇒ ¬¬((a ⇒ b) ⇒ (a ⇔ b)):
   thm

> SAT_PROVE ``~(a /\ ~a)``;
val it = [oracles: DISK_THM] [axioms: ] [] ⊢ ¬(a ∧ ¬a): thm

As expected, if the target term is unsatisfiable we get a theorem saying as much.

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 tautLib (see Section 8.11.1 below).

If MiniSat failed to build when HOL was built, or proof replay fails for some other reason, SAT_PROVE falls back to a DPLL-based propositional tautology prover implemented in SML, due to Michael Norrish (see the HOL Tutorial). 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.

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 HolSatLib has only been tested on Linux, and on Windows XP using MinGW.

tautLib

tautLib predates 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 tautLib signature now act as wrappers around calls to HolSatLib. However, the wrappers are able to provide the following extra functionality on top of HolSatLib:

1. They can handle top level universal quantifiers.
2. 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.

For details, see the source file src/taut/tautLib.sml which contains comprehensive comments. Note however that the extra functionality in tautLib was not engineered for very large problems and can become a performance bottleneck.

Support for other SAT solvers

The ZChaff SAT solver has a proof production mode and is supported by 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 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 zchaff in the directory 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 "Z", e.g., ZSAT_PROVE.

A file 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.

Other 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 https://github.com/HOL-Theorem-Prover/HOL.

The general interface

The functions described above are wrappers for the function GEN_SAT, which is the single entry point for HolSatLib. GEN_SAT can be used directly if more flexibility is required. GEN_SAT takes a single argument, of type sat_config, defined in satConfig.sml. This is an opaque record type, currently containing the following fields:

1. term : Term.term

   The input term.

2. solver : SatSolvers.sat_solver

   The external SAT solver to use. The default is SatSolvers.minisatp. If ZChaff is installed (see Section 8.11.2), then SatSolvers.zchaff may also be used.

3. infile : string option

   The name of a file in DIMACS format.¹ Overrides term if set. The input term is instead read from the file.

4. proof : string option

   The name of a proof trace file. Overrides solver if set. The file must be in the native format of HolSatLib, and must correspond to a proof for 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 src/HolSat/sat_solvers/zc2hs (type zc2hs -h for usage help). zc2hs is used internally by ZSAT_PROVE etc.

5. is_cnf : bool

   If true then the input term is expected to be a negated CNF term. This is set automatically if infile is set. Typically a user will never need to modify this field directly.

6. is_proved : bool

   If true then HOL will prove the SAT solver's results.

A special value base_config : sat_config is provided for which the term is 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 src/HolSat/satConfig.sig. For example, to invoke ZChaff (assuming it is installed), on a file zchaff.cnf containing a DIMACS-formatted problem, we do:

> open satConfig;   ... output elided ...

> val c = base_config |> set_infile "zchaff.cnf"
                      |> set_solver SatSolvers.zchaff;
val c =
   {flags = {is_cnf = true, is_proved = true}, infile = SOME "zchaff.cnf",
    proof = NONE, pterm = “T”, solver =
    SatSolver
     {URL = "http://www.princeton.edu/~chaff/zchaff", end_string =
      "Random Seed Used", executable =
      "/Users/michaeln/HOL/src/HolSat/sat_solvers/zchaff/zchaff",
      failure_string = "UNSAT", name = "zchaff", notime_run = fn, only_true =
      false, post_exe =
      SOME "/Users/michaeln/HOL/src/HolSat/sat_solvers/zc2hs/zc2hs",
      post_run = fn, start_string = "Instance Satisfiable", time_run = fn}}:
   sat_config

> GEN_SAT c;
Exception- SAT_cex
  ⊢ v1 ∧ v5 ∧ v4 ∧ v3 ⇒
    ¬((v1 ∨ ¬v5 ∨ v4) ∧ (¬v1 ∨ v5 ∨ v3 ∨ v4) ∧ (¬v3 ∨ ¬v4)) raised

Normally, HolSatLib will delete the files generated by the SAT solver, such as the output proof, counter-model, and result status. However, if infile is set, the files are not deleted, in case they are required elsewhere.

Notes

On Linux and MacOS, g++ must be installed on the system for MiniSat and zc2hs to build.

Temporary files are generated using the Moscow ML function 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, HolSatLib calls may fail mysteriously.

The function dimacsTools.readDimacs file reads a DIMACS format file and returns a CNF HOL term corresponding to the SAT problem in the file named by file. Since DIMACS uses numbers to denote variables, and numbers are not legal identifiers in HOL, each variable number is prefixed with the string "v". This string is defined in the reference variable dimacsTools.prefix and can be changed if required. This function can be used independently of HolSatLib to read in DIMACS format files.

1. http://www.satlib.org/Benchmarks/SAT/satformat.ps ↩