PIMS - SFU Theory Seminar: Antonina Kolokolova

How does representation of a problem affect the complexity of solving it? What is the interplay between the richness of a domain in which a statement is expressed and the complexity of proving that statement? Not only this is a fundamental question in logic, it also has a plethora of practical applications: given a class of problems, practitioners want to know how to encode them and which solver to use to solve them most efficiently.

Here we present a proof complexity approach to this question, in particular using tools of proof complexity to study satisfiability modulo theories (SMT) framework. In SMT, propositional satisfiability solvers operate over Boolean combinations of atoms from an underlying theory (such as theory of linear arithmetic or uninterpreted functions with equality), using a dedicated theory solver to analyse viability of supposed satisfying assignments from the theory perspective, and derive new facts by theory reasoning. A natural question is just how much it helps to augment propositional, resolution-based reasoning with the power of the theory.

We start by presenting a class of proof systems for resolution over a theory, and show that the correspondence between SAT solvers based on conflict-driven clause learning with restarts and general resolution can be extended to SMT. We then show that even a theory of uninterpreted functions, decidable in near-linear time, helps enormously: resolution over that theory can simulate a much more powerful Frege (natural deduction) system (and with an additional rule, even extended Frege system). Based on joint work with Vijay Ganesh, Robert Robere and Arnold Beckmann.