BARC talk by Vincent Liew

Thursday, 21 November 2019, Vincent Liew, PhD student at the University of Washington, USA, will give a talk on "Proof complexity with multiplier circuits".

Title:
Proof complexity with multiplier circuits

Abstract:
We discuss the problem of verifying the arithmetic properties of integer multiplier circuits such as commutativity and distributivity. Such verification problems arise not only in hardware verification, but also in verifying software that uses multiplication. The standard approach would be to encode the desired property as a CNF formula, then feed the formula into a SAT-solver. However, while modern SAT-solvers have become highly efficient for many problems, they all scale poorly on problems involving multiplier circuits.
We examine the prospects of achieving efficient multiplier verification from the lens of proof complexity. Current SAT-solving algorithms implicitly walk through a resolution proof, and hence their runtime is limited by resolution proof size. To explain the slow performance of SAT-solvers, it was conjectured in 2015 that the resolution proofs associated with verifying properties of multiplier circuits are exponentially large. Our previous work in 2017 found that this conjecture is false: there are polynomial-size resolution proofs for any degree two ring identity. On the other hand, these polynomials were of rather high degree, so even if a SAT-solver found these proofs, its runtime may still be impractical.
The natural next step is to consider solvers based on more powerful proof systems such as polynomial calculus or cutting planes, with the hope that better proofs can be found in these systems. In our ongoing work, we have shown that the cutting planes proof system is capable of giving proofs with nearly optimal size for a large class of degree two ring identities. We give these proofs in the format of an extended version of cutting planes that allows one to write inequalities containing a bounded number of nonlinear terms. Proofs in this extended system correspond to standard cutting planes proofs that are larger by a small factor. This extended system allows us to write the cutting planes proofs in a rather understandable way.

Bio:
Vincent Liew is a PhD student in the theory group in the Allen School of Computer Science and Engineering at the University of Washington, USA, where he is advised by Paul Beame. His current research aims to understand and improve verification tools like SAT-solvers from the perspective of proof complexity. More broadly, he is interested in applying the perspective of a theorist to problems from other fields. Previously he attended MIT, where he received his B.S. in Mathematics and B.S. in Physics in 2013.

The talk will be followed by 1-1½ hours of more informal, technical discussions in The Creative Room (BARC, 1st floor). The purpose is to go over the material in more detail, and to have the opportunity to ask lots of questions and discuss ideas. After a theoretical talk, we go deeper into technicalities, look at the actual definitions, and prove at least some of the key ingredients in the results including all (or at least some of) the gory technical details glossed over in a polished seminar presentation. For a more applied talk, we might discuss questions of implementation or discuss detailed experimental results. As usual, this second part is entirely optional, and can safely be skipped by everybody who feels that a regular 1-hour talk is sufficient to meet their needs. No excuses needed; no questions asked...