# Towards Verifying Nonlinear Integer Arithmetic

## TL;DR

This paper advances the verification of nonlinear integer arithmetic by constructing short resolution proofs for multiplier circuit properties, overcoming previous conjectures about their non-existence, and enabling more efficient SAT-based verification.

## Contribution

It introduces methods to generate short resolution proofs for complex multiplier identities, significantly improving verification efficiency for nonlinear integer arithmetic.

## Key findings

- Short regular resolution proofs for degree 2 identities on various multipliers
- Quasipolynomial size proofs for Wallace tree multipliers
- Overcoming previous conjectures about proof length limitations

## Abstract

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 quasipolynomial- n^{O(\log n)} size proofs for these identities on Wallace tree multipliers.