Verifying SAT and SMT in Coq for a fully automated decision procedure
Michaël Armand, Gilbert Charles Faure, Chantal Keller, Laurent Théry, Benjamin Werner, Inria Sophia-Antipolis · 2011
Enjoying the power of SAT and SMT solvers in the Coq proof assistant without compromising soundness requires more than a yes/no answer from them. SAT and SMT solvers should also return a proof witness that can be checked by an external tool. We propose a fully certified checker for such witnesses written in Coq. It can currently check witnesses from the SAT solvers ZChaff and MiniSat and from the SMT solver VeriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq’s logic by calling external provers and carefully checking their answers.