A framework for verified use of an external AIG+SAT solver with ACL2
Matt Kaufmann
April 13, 2011

Abstract.

We provide a framework for proving ACL2 theorems with the help of an
external SAT solver, but without dependence on the correctness of that
solver.  The solver is the ZZ tool of Niklas Een, a C program based on
MiniSAT that proves unsatisfiability of and-inverter graphs (AIGs).
Our talk focuses on the proof-checker as well as the use of two
certification runs in order to avoid trust tags (this will be
explained).  As time permits (which it probably won't, really), I'll
mention a connection with the GL framework of Sol Swords.

The talk (but not necessarily the notes without the talk) is intended
to be self-contained for anyone familiar with ACL2.  My goal, in
addition to presenting our framework, is to illustrate several
features of ACL2 developed in recent years.