External SAT Solvers

In addition to the abc, z3, and yices proof tactics used above, SAWScript can also invoke arbitrary external SAT solvers that read CNF files and produce results according to the SAT competition input and output conventions, using the external_cnf_solver tactic. For example, you can use PicoSAT to prove the theorem thm from the last example, with the following commands:

let picosat = external_cnf_solver "picosat" ["%f"];
prove_print picosat thm;x

The use of let is simply a convenient abbreviation. The following would be equivalent:

prove_print (external_cnf_solver "picosat" ["%f"]) thm;

The first argument to external_cnf_solver is the name of the executable. It can be a fully-qualified name, or simply the bare executable name if it’s in your PATH. The second argument is an array of command-line arguments to the solver. Any occurrence of %f is replaced with the name of the temporary file containing the CNF representation of the term you’re proving.

The external_cnf_solver tactic is based on the same underlying infrastructure as the abc tactic, and is generally capable of proving the same variety of theorems.

To write a CNF file without immediately invoking a solver, use the offline_cnf tactic, or the write_cnf top-level command.