Interactive theorem provers suffer from a disadvantage implied by the name: in the proof of a nontrivial theorem, manual guidance by the user is often required. By contrast, Boolean satisfiability (SAT) solvers are powerful tools for propositional logic that do not need manual guidance. In the area of formal verification, one can often reduce the given problem to a SAT problem. Thus, an interactive theorem prover that could take advantage of a SAT solver could potentially be a significant improvement.
This paper proposes a technique for doing this that does not involve embedding a SAT solver in the theorem prover. The idea is for the theorem prover to verify a proof generated by the SAT solver, thus avoiding soundness bugs in the SAT solver, amongst other issues that would arise if the result from the SAT solver were simply asserted as a theorem. However, more is needed if this idea is to be truly effective. The heart of the paper concerns the complex details of the translation of the SAT solver’s result into a form in which the theorem prover can speed up its verification of the proof. The author describes with illustrative examples the process whereby partial results from the SAT solver can be memoized--for example, the SAT solver will, in the course of its reasoning, find and refind a number of conflicts that cannot be satisfied.
Amjad provides enough background to make the paper reasonably self-contained. The experimental results show that the speedups obtained are significant.