From DRUP to PAC and Back
Daniela Kaufmanna, Armin Biereb and Manuel Kauersc
Johannes Kepler University Linz, Altenbergerstr. 69, 4040 Linz, Austria
adaniela.kaufmann@jku.at
barmin.biere@jku.at
cmanuel.kauers@jku.at
ABSTRACT
Currently the most efficient automatic approach to verify gate-level multipliers combines SAT solving and computer algebra. In order to increase confidence in the verification, proof certificates are generated. However, due to different solving techniques, these certificates require two different proof formats, namely DRUP and PAC. A combined proof has so far been missing. Correctness of this approach can thus only be trusted up to the correctness of compositional reasoning. In this paper we show how to generate a single proof in one proof format, which then allows to certify correctness using one simple proof checker. We further investigate empirically the effect on proof generation and checking time as well as on proof size. It turns out that PAC proofs are much more compact and faster to check.
