On the Algebraic Proof Complexity of Constraint Satisfaction
Conneryd, Jonas LU
(2026)
- 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... (More) - 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.
(Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/ec4dd5a6-b9a3-412c-a37b-5b790e41dd3e
- author
- Conneryd, Jonas
LU
- supervisor
- opponent
-
- Prof. Razborov, Alexander, University of Chicago, USA.
- organization
- publishing date
- 2026
- type
- Thesis
- publication status
- published
- subject
- keywords
- computational complexity theory, proof complexity
- publisher
- Computer Science, Lund University
- defense location
- Lecture Hall E:1406, building E, Klas Anshelms väg 10, Faculty of Engineering LTH, Lund University, Lund. The dissertation will be live streamed, but part of the premises is to be excluded from the live stream.
- defense date
- 2026-09-25 13:00:00
- ISBN
- 978-91-90202-70-8
- 978-91-90202-69-2
- language
- English
- LU publication?
- yes
- id
- ec4dd5a6-b9a3-412c-a37b-5b790e41dd3e
- date added to LUP
- 2026-09-01 10:23:27
- date last changed
- 2026-09-01 14:11:24
@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}},
}