A Path Paved by Proof Complexity Towards Verifying Nonlinear Integer Arithmetic

Thesis (Ph.D.)--University of Washington, 2020Automated theorem provers have long struggled to efficiently reason about bit-precise properties of integer multiplication. Despite major advances in the efficiency of automated reasoning, from the Binary Decision Diagrams of the 1980s to the SAT solvers of today, integer multiplication has persisted as a major bottleneck in hardware and software verification. In this thesis, we use proof complexity to pave a new path towards verifying nonlinear integer arithmetic. We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. We present several results on the proof complexity of fundamental multiplier identities. In the resolution proof system, we construct polynomial size proofs for degree two ring identities, refuting a widely believed conjecture that such proofs must be exponentially large. In the polynomial calculus proof system, we give optimal length proofs for word-level ring identities. But we also show that extracting simple bit-level consequences from a word-level property can require an exponentially large polynomial calculus derivation. In the cutting planes proof system, we give optimal length proofs for a large class of degree two identities, at both the word-level and the bit-level. We then present experiments testing the CDCL SAT solving approach (corresponding to resolution) and the pseudo-Boolean approach (corresponding to cutting planes) that uncover the potential of using pseudo-Boolean solvers to efficiently reason with mixtures of arithmetic and bit-level constraints. We demonstrate that pseudo-Boolean solvers can verify, at both the word-level and bit-level, the commutativity of a multiplier as well as the equivalence of different multiplier architectures. We also find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers