@phdthesis{ec4dd5a6-b9a3-412c-a37b-5b790e41dd3e,
  abstract     = {{This thesis comprises three papers in the field of <i>proof complexity</i>, in which the objects of study are certificates of unsatisfiability. In <i>algebraic</i> 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 <i>polynomial calculus</i> proof system, where this is accomplished by iteratively deriving new polynomials in the ideal generated by the input until reaching the constant polynomial 1.<br/><br/>In Paper A, we prove asymptotically optimal lower bounds on the size and degree required for polynomial calculus to refute the <i>k</i>-colorability of a sparse random graph sampled either from the Erdős–Rényi distribution or the uniform distribution over regular graphs. <br/><br/>In Paper B, we show that the so-called <i>Alekhnovich-Razborov</i> method for proving polynomial calculus degree lower bounds also yields level lower bounds for an algorithm called <i>cohomological k-consistency</i>, 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 <i>k</i>-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 <i>lax and null-constraining </i>CSPs, originally due to Chan and Ng. <br/><br/>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 <i>non-automatable</i>, 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 <i>non</i>-roots of unity simulates the <i>cutting planes</i> proof system with polynomially bounded coefficients. <br/>}},
  author       = {{Conneryd, Jonas}},
  isbn         = {{978-91-90202-70-8}},
  keywords     = {{computational complexity theory; proof complexity}},
  language     = {{eng}},
  publisher    = {{Computer Science, Lund University}},
  school       = {{Lund University}},
  title        = {{On the Algebraic Proof Complexity of Constraint Satisfaction}},
  url          = {{https://lup.lub.lu.se/search/files/259610608/thesis-no-papers.pdf}},
  year         = {{2026}},
}