Integrating SAT, QBF and SMT Solvers
with Interactive Theorem Provers Tjark Weber Workshop on Trusted Extensions of Interactive Theorem Provers August 11, 2010 System Overview Motivation Validation Automation SMT propositional logic equality uninterpreted functions arrays quantifiers linear arithmetic bit-vectors data types SAT QBF Boolean variables negation disjunction conjunction propositional logic Boolean quantifiers Demo LCF-style Theorem Proving Theorems are implemented as an abstract data type. There is a fixed number of constructor functions - one for each axiom/inference rule of higher-order logic. More complicated proof procedures must be implemented by composing these functions. Selected HOL4 Inference Rules Sequent Clauses Resolution, LCF-style Q-resolution is propositional resolution followed by forall-reduction. Q-Resolution Propositional Resolution How can we implement this efficiently on top of existing LCF-style kernels? Q-Resolution, LCF-style Example Forall-Reduction, LCF-style Z3 uses 34 different inference rules. Satisfiability Modulo Theories Proof Structure Proofs are directed acyclic graphs. Each node corresponds to an inference step.
Children are premises of inferences. Leaves are axioms/input formulas.
A designated root note concludes . Proofs can be checked by depth-first postorder traversal. 1. A single primitive inference/theorem instantiation.
2. Combinations of primitive inferences/theorem instantiations.
3. Automated proof procedures (e.g., for linear arithmetic).
4. Combinations of the above. Combinations of Primitive Inferences Avoiding Automated Proof Procedures Combinations of primitive inferences
Instantiation of schematic theorems
Generalization wrt. background theories
Memoization Speed-ups of up to 3 orders of magnitude! Evaluation Integrating SAT, QBF and SMT Solvers
with Interactive Theorem Provers http://www.cl.cam.ac.uk/~tw333/ SAT QBF SMT LCF-style proof checking is feasible for SAT, QBF and SMT. It scales to large formulas and proofs with millions of inferences.
Naive solutions are slow - an efficient implementation is crucial! Also, some kernel optimizations were necessary.
Our integrations provide a high degree of automation in Isabelle and HOL4, and high assurance for the external solvers' results. Conclusions Evaluation on 69 invalid QBF problems from the 2005 fixed instance and 2006 preliminary QBF-Eval data sets
up to 131 alternating quantiers, 24,562 variables, 35,189 clauses For QBF validation, HOL4's name-carrying kernel is about 75 times faster (after optimizations) than the kernel that uses de Bruijn indices internally. QBF certificate validation in HOL4 is about 25 times faster than proof search with Squolem. All certificates are checked successfully! Certificate validation in Isabelle/HOL is about 19 times slower than proof search with Z3. Timeouts are due to theory reasoning; Z3's proofs are not detailed enough. 75% of SMT-LIB problems are checked successfully! (joint work with Hasan Amjad and Sascha Böhme)See the full transcript