Abstract
Many natural computational problems, such as satisfiability and systems of equations, can be expressed in a unified way as constraint satisfaction problems (CSPs). In this talk I will show that the usual reductions preserving the complexity of the constraint satisfaction problem preserve also its proof complexity. As an application, I will present gap theorems, which say that CSPs that admit small size refutations in some classical proof systems are exactly the constraint satisfaction problems which can be solved by Datalog.
This is joint work with Albert Atserias.