Abstract
Paul Beame
Title: Using Resolution and Cutting Planes for Verification of Nonlinear Bit-Vector Properties
Abstract: There has been great success using bit-vector solvers relying on CDCL SAT-solving to verify hardware and software systems that mix Boolean logic and linear arithmetic, but it has been a long-standing challenge to extend this to include multiplication. Even the best CDCL solvers have been unable to verify simple properties of multipliers, such as commutativity on numbers of relatively few bits. This failure and apparent exponential behavior of CDCL solvers led to the conjecture that there was an inherent road-block in its resolution complexity. We first sketch our work showing that there is no exponential road-block in resolution and describe our efforts to get CDCL solvers to find these resolution proofs and their limitations. In parallel with that work, others suggested methods based on polynomial calculus that can find optimal size proofs of these simple properties. Unfortunately, we can show other inherent limitations in extending these polynomial calculus methods to properties that involve individual output bits.
We show that pseudo-Boolean reasoning based on cutting planes proofs has the potential to overcome both these problems. Theoretically, we give optimal size cutting planes proofs of a sizable class of multiplier properties even at the bit level. We also describe how we were able to use pseudo-Boolean solvers with cutting planes reasoning to efficiently verify bit-level commutativity and equivalence properties of multipliers, as well as to verify other bit-level properties that even bit-vector solvers with preprocessing are unable to verify. These results provide new motivation for strengthening pseudo-Boolean solvers in their application of cutting planes reasoning. Joint work with Vincent Liew, Jo Devriendt, Jan Elffers, and Jakob Nordström
Marc Vinyals
Title: Hard Examples for Common Variable Decision Heuristics
Abstract: The CDCL algorithm, which is nowadays the top-performing algorithm to solve SAT in practice, is polynomially equivalent to resolution when we view it as a proof system, that is we replace some of its heuristics by nondeterministic choices.
In this talk we show that this is no longer true if we leave the heuristics in place; more precisely we build a family of formulas that have resolution proofs of polynomial size but require exponential time to decide in CDCL with a class of variable decision heuristics that includes the most common heuristics such as VSIDS.
Noah Fleming
Title: The Proof Complexity of Integer Programming
Abstract: In this talk, we will switch gears and talk about the proof complexity of practical integer programming and a proof system which is a natural generalization of DPLL to reason about linear inequalities. The branch-and-cut paradigm forms the basis of many of the modern integer programming solvers used in practice. Stabbing Planes was introduced in order to model branch-and-cut as a proof system. While very simple, Stabbing Planes proofs are surprisingly powerful: they can simulate Cutting Planes, and can efficiently refute any unsatisfiable system of linear equations over a finite field. In a surprising recent result, Dadush and Tiwari showed that these short Stabbing Planes refutations of the Tseitin formulas could be translated into Cutting Planes proofs. This raises the question of whether all Stabbing Planes can be efficiently translated into Cutting Planes. This would allow the substantial analysis done on Cutting Planes to be lifted to branch-and-cut based integer programming solvers. In a recent work, we gave a partial result to this question, showing that Stabbing Planes proofs can be translated into Cutting Planes somewhat efficiently provided a weak (quasi-polynomial) guarantee on the length of the coefficients in the proof.
In this talk, I will introduce and motivate the Stabbing Planes proof system. I will then discuss the known relationship between Stabbing Planes and Cutting Planes, as well as illustrate how Stabbing Planes can reason about systems of equations over finite fields.
Chunxiao (Ian) Li
Title: Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
Abstract: Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical explanation of whether restarts are indeed crucial to the power of CDCL solvers is lacking. There have been many attempts to capture the power of restarts by modelling solvers with and without restarts as proof systems. In this talk, I will first survey existing work on understanding the power of restarts, and then present several recent results on restarts when considering different configurations of SAT solvers.