Jonas Conneryd's PhD defence

Thesis title: On the Algebraic Proof Complexity of Constraint Satisfaction

Author: Jonas Conneryd, Department of Computer Science, Lund University

Faculty opponent: Professor Alexander Razborov, University of Chicago, USA

Examination Committee:

• Professor Johan Wästlund, University of Gothenburg
• Associate Professor Per Austrin, KTH Royal Institute of Technology
• Associate Professor Vladimir Podolskii, Tufts University, USA
• Deputy: Professor Jacek Malec, Lund University

Session chair: Senior Lecturer Elin Anna Topp, Lund University

Supervisors:

• Main supervisor: Professor Tatyana Turova, Lund University
• Senior Lecturer Michael Doggett, Lund University

Location: E:1406, E-huset, Klas Anshelms väg 10/Ole Römers väg 3, Lund

Here is a link to download the thesis

Abstract

This thesis comprises three papers in the field of proof complexity, in which the objects of study are certificates of unsatisfiability. In algebraic proof complexity, the aim is to prove lower bounds on the complexity of certifying that there is no common root of a given set of polynomials. We will be especially concerned with the polynomial calculus proof system, where this is accomplished by iteratively deriving new polynomials in the ideal generated by the input until reaching the constant polynomial 1.

In Paper A, we prove asymptotically optimal lower bounds on the size and degree required for polynomial calculus to refute the k-colorability of a sparse random graph sampled either from the Erdős–Rényi distribution or the uniform distribution over regular graphs.

In Paper B, we show that the so-called Alekhnovich-Razborov method for proving polynomial calculus degree lower bounds also yields level lower bounds for an algorithm called cohomological k-consistency, which is a general-purpose method for solving constraint satisfaction problems (CSPs). Together with the degree lower bounds from Paper A, which are established using this method, this result establishes optimal cohomological k-consistency level lower bounds for approximate graph coloring. Through this connection, we also provide an alternative proof of an optimal level lower bound for random instances of so-called lax and null-constraining CSPs, originally due to Chan and Ng.

Finally, in Paper C, we systematically investigate polynomial calculus over other variable domains than {0, 1}. Over other domains, the usual methods for proving size lower bounds break down. Using a new, unified framework, we prove optimal size lower bounds for random graph coloring in Bayer's formulation over roots of unity as well as for the functional pigeonhole principle over {1,- 1}-valued variables. In addition, we prove that polynomial calculus where each {0, 1}-valued variable also has a {1, -1}-valued counterpart is non-automatable, which informally means that efficiently searching for proofs in this proof system is impossible unless P=NP. As a complement to our lower bounds for variable domains consisting of roots of unity, we prove that polynomial calculus over non-roots of unity simulates the cutting planes proof system with polynomially bounded coefficients.