迈向非线性整数算术的验证

我们通过展示如何为最广泛使用的乘法器电路的许多性质构造简短消解证明，消除了使用CDCL SAT求解器高效验证非线性整数算术的一个关键障碍。此类简短证明曾被猜想不存在。更确切地说，我们给出了关于阵列乘法器、对角线乘法器和Booth乘法器上任意二阶恒等式的 n^{O(1)} 规模正则消解证明，以及关于Wallace树乘法器上这些恒等式的拟多项式规模 n^{O(\log n)} 证明。