Toward Verifying Nonlinear Integer Arithmetic
Paul W. Beame, Vincent Liew · Journal of the ACM · 2019
We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give n O (1) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and n O (log n ) size proofs for these identities on Wallace tree multipliers.