val satOracle : sat_solver -> Term.term -> Thm.thm
STRUCTURE
HolSatLib
SYNOPSIS
Invokes supplied SAT solver on the argument term, returning a tagged theorem if a model is found, otherwise returning a tagged theorem indicating that the negation of the supplied term is valid.
DESCRIBE
The supplied term should be a term of propositional logic and must be in conjunctive normal form.
FAILURE
Fails if the SAT solver fails abnormally.
EXAMPLE
- load "HolSatLib"; open HolSatLib;
(* output omitted *)
> val it = () : unit

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

- satOracle grasp ``(x \/ ~y \/ z) /\ (~z \/ y)``;
> val it = [oracles: grasp] [axioms: ] [] 
           |- z /\ y ==> (x \/ ~y \/ z) /\ (~z \/ y) : thm

- satOracle grasp ``(x \/ ~y \/ z) /\ ~z /\ y /\ ~x``;
> val it = [oracles: grasp] [axioms: ] [] 
           |- ~((x \/ ~y \/ z) /\ ~z /\ y /\ ~x)
COMMENTS
If one is not prepared to trust the solver, then one can use satProve which verifies the model within HOL. However, satProve will fail if no model is found. The SAT solver must be a supported one: see the HolSat section of the HOL System Description for details.
SEEALSO
satProve
HOL  Kananaskis-4