# Towards Verifying Nonlinear Integer Arithmetic

arXiv: https://arxiv.org/abs/1705.04302 · HTML: https://mlsanity.com/paper/1705.04302/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 May 2017.

## Built on by (most cited first, 1 of 1)

- [Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL](https://mlsanity.com/paper/2607.23715/) (2026)

## Abstract (arXiv)

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 nO(1) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and quasipolynomial- nO(log n) size proofs for these identities on Wallace tree multipliers.