# Graph Colouring is Hard for Algorithms Based on
Hilbert’s Nullstellensatz and Gröbner Bases††thanks: This is the full-length
version of the paper with the same title that appeared in _Proceedings of the
32nd Annual Computational Complexity Conference (CCC ’17)_.

Massimo Lauria
Sapienza — Università di Roma, Italy
<EMAIL_ADDRESS>Jakob Nordström
University of Copenhagen, Denmark, and Lund University, Sweden
<EMAIL_ADDRESS>
(August 28, 2024)

###### Abstract

We consider the graph $k$-colouring problem encoded as a set of polynomial
equations in the standard way over $0/1$-valued variables. We prove that there
are bounded-degree graphs that do not have legal $k$-colourings but for which
the polynomial calculus proof system defined in [Clegg et al. ’96, Alekhnovich
et al. ’02] requires linear degree, and hence exponential size, to establish
this fact. This implies a linear degree lower bound for any algorithms based
on Gröbner bases solving graph $k$-colouring using this encoding. The same
bound applies also for the algorithm studied in a sequence of papers [De Loera
et al. ’08, ’09, ’11, ’15] based on Hilbert’s Nullstellensatz proofs for a
slightly different encoding, thus resolving an open problem mentioned in [De
Loera et al. ’08, ’09, ’11] and [Li et al. ’16]. We obtain our results by
combining the polynomial calculus degree lower bound for functional pigeonhole
principle (FPHP) formulas over bounded-degree bipartite graphs in [Mikša and
Nordström ’15] with a reduction from FPHP to $k$-colouring derivable by
polynomial calculus in constant degree.

##  1 Introduction

Given an undirected graph $G=(V,E)$ and a positive integer $k$, can the
vertices $v\in V$ be coloured with at most $k$ colours so that no vertices
connected by an edge have the same colour? This _graph colouring problem_ is
perhaps one of the most extensively studied NP-complete problems. It is widely
believed that any algorithm for this problem has to run in exponential time in
the worst case, and indeed the currently fastest algorithm for $3$-colouring
runs in time $O(1.3289^{n})$ [BE05]. A survey on various algorithms and
techniques for so-called exact algorithms is [Hus15].

Many graph colouring instances of interest might not exhibit worst-case
behaviour, however, and therefore it makes sense to study algorithms without
worst-case guarantees and examine how they perform in practice. Dually, it can
be of interest to study weak models of computation, which are nevertheless
strong enough to capture the power of such algorithms, and prove unconditional
lower bounds for these models. Obtaining such lower bounds is the goal of this
work.

###  1.1 Brief Background

Since current state-of-the-art algorithms for propositional satisfiability
such as _conflict-driven clause learning (CDCL)_ [BS97, MS99, MMZ+01] are
ultimately based on the _resolution proof system_ [Bla37], it is perhaps not
so surprising that this approach can be used to solve graph colouring problems
as well. According to [BCMM05], McDiarmid developed a method for deciding
$k$-colourability that captures many concrete algorithms [McD84]. This method,
viewed as a proof system, is simulated by resolution.

There are exponential lower bounds for resolution proofs of
non-$k$-colourability that apply to any such method. In particular, the paper
[BCMM05] presents average-case exponential lower bounds for random graph
$k$-colouring instances sampled so that the graphs are highly likely not to be
$k$-colourable. This result is obtained by proving width lower bounds, i.e.,
lower bounds on the size of a largest clause in any resolution refutations of
the formulas, and then using that linear width lower bounds implies
exponential size lower bounds [BW01].

Another possible approach is to attack the $k$-colouring problem using
algebra. Various algebraic methods have been considered in [Mat74, Mat04,
Lov94, AT92]. The thesis [Bay82] contains the first explicit attempt we know
of to encode the ${3}$-colouring problem using Hilbert’s Nullstellensatz. At a
high level, the idea is to write the problem as a set of polynomial equations
$\\{f_{i}(x_{1},\ldots,x_{n})=0\mid i\in[m]\\}$ over a suitable field
$\mathbb{F}$ so that legal colourings correspond to solutions, and if this is
done in the right way it holds that this system of equations has no solution
if and only if there are polynomials $g_{1},\ldots,g_{m}$ such that
$\sum_{i=1}^{m}g_{i}f_{i}=1$. This latter equality is referred to as a
_Nullstellensatz certificate_ of non-colourability, and the _degree_ of this
certificate is the largest degree of any polynomial $g_{i}f_{i}$ in the sum.
Later papers based on Nullstellensatz and Gröbner bases such as [De 95, Mnu01,
HW08] have attracted a fair amount of attention. For this work, we are
particularly interested in the sequence of papers [DLMM08, DLMO09, DLMM11,
DMP+15], which uses an encoding of the $k$-colouring problem that will be
discussed more in detail later in the paper.

There seem to be no formally proven lower bounds for these algebraic methods.
On the contrary, the authors of [DLMO09] report that essentially all of the
benchmarks they have studied have Nullstellensatz certificates of constant
(and very small) degree. Indeed, no lower bounds for graph colouring is known
for the corresponding proof systems _Nullstellensatz_ [BIK+94] or the stronger
system _polynomial calculus_ [CEI96, ABRW02]. Intriguingly, in a close
parallel to the case for resolution it is known that strong enough lower
bounds on polynomial calculus degree imply exponential lower bounds on proof
size [IPS99], but the techniques for proving degree lower bounds are much less
developed than the width lower bound techniques for resolution.

There have been degree lower bounds proven for polynomial calculus refutations
of concrete systems of polynomial equations, but in most cases these have been
encodings of obviously false statements (such as negations of the pigeonhole
principle or graph handshaking lemma), rather than computationally hard
problems. For some of these problems degree lower bounds can be obtained by
making an affine transformation from $\\{0,1\\}$-valued variables to
$\\{-1,+1\\}$-valued variables [BGIP01, BI10], but this only works for
polynomial equations with the right structure and only for fields of
characteristic distinct from $2$. A general and powerful method, which is
independent of the field characteristic, was developed in [AR03], but has
turned out to be not so easy to to apply (except in a few papers such as
[GL10a, GL10b]). A slightly different, and formally speaking somewhat
incomparable, version of the approach in [AR03] was recently presented in
[MN15], and this latter paper also more clearly highlighted the similarities
and differences between resolution width lower bound techniques and polynomial
calculus degree lower bound techniques. The new framework in [MN15] was used
to establish a new degree lower bound which plays a key role in our paper.

###  1.2 Our Contributions

We exhibit explicit families of non-$k$-colourable graphs of bounded vertex
degree such that the canonical encoding of the corresponding $k$-colouring
instances into systems of polynomial equations over $\\{0,1\\}$-valued
variables require linear degree to be refuted in polynomial calculus.

######  Theorem 1.1 (informal).

For any constant $k\geq 3$ there are explicit families of graphs
$\\{G_{n}\\}_{n\in\mathbb{N}}$ of size $\mathrm{O}(n)$ and constant vertex
degree, which are not $k$-colourable but for which the polynomial calculus
proof system requires linear degree, and hence exponential size, to prove this
fact, regardless of the underlying field.

Our degree lower bound also applies to a slightly different encoding with
primitive $k$th roots of unity used in [DLMM08, DLMM11] to build $k$-colouring
algorithms based on Hilbert’s Nullstellensatz. These algorithms construct
certificates of non-$k$-colourability by solving linear systems of equations
over the coefficients of all monomials up to a certain degree.

Just as the algorithms in [DLMM08, DLMM11], our lower bound does not work for
all fields (the field must have an extension field in which there is a
primitive $k$th root of unity). For simplicity, we state below a concrete
result for Nullstellensatz certificates over $\mathrm{GF}(2)$ for
non-${3}$-colourability, which is one of the main cases considered in [DLMM08,
DLMM11].

######  Corollary 1.2.

There are explicit families of non-${3}$-colourable graphs such that the
algorithms based on Hilbert’s Nullstellensatz over $\mathrm{GF}(2)$ in
[DLMM08, DLMM11] need to find certificates of linear degree, and hence must
solve systems of linear equations of exponential size, in order to certify
non-${3}$-colourability.

We remark that Corollary 1.2 answers an open question raised in, for example,
[DLMM08, DLMO09, DLMM11, LLO16].

Finally, we want to mention that the graph colouring instances that we
construct turn out to be easy for the proof system _cutting planes_ [CCT87],
which formalizes the integer linear programming algorithm in [Gom63, Chv73]
and underlies so-called _pseudo-Boolean_ SAT solvers such as, for instance,
_Sat4j_ [LP10, S4j].

######  Proposition 1.3.

The graph colouring instances for the non-$k$-colourable graphs in Theorem 1.1
have polynomial-size refutations in the cutting planes proof system.

###  1.3 Techniques

Perhaps somewhat surprisingly, no heavy-duty machinery is required to
establish Theorem 1.1. Instead, all that is needed is a nifty reduction. Our
starting point is the so-called _functional pigeonhole principle (FPHP)
formula_ restricted to a bipartite graph of bounded left degree $k$. This
formula expresses the claim that a set of pigeons $i\in I$ can be mapped to a
set of pigeonholes $j\in J$ in a one-to-one fashion, where in addition the
pigeons are constrained so that every pigeon can choose not between all
available holes but only between a set of $k$ holes as specified by the
bipartite graph. Clearly, FPHP formulas are unsatisfiable when $\lvert
I\rvert>\lvert J\rvert$.

Any instance of a graph FPHP formula can be viewed as a constraint
satisfaction problem by ordering the available holes for every pigeon in some
arbitrary but fixed way, and then keeping track of where each pigeon is mapped
by recording the ordinal number of its chosen pigeonhole. If the $c$th hole
for pigeon $i$ and the $c^{\prime}$th hole for pigeon $i^{\prime}$ is one and
the same hole $j$, then pigeons $i$ and $i^{\prime}$ cannot be allowed to make
choices $c$ and $c^{\prime}$ simultaneously. If we view this constraint as an
edge in graph with the pigeons $I$ as vertices, this is already close to a
graph colouring instance, except that what is forbidden for the neighbours $i$
and $i^{\prime}$ is not the same colour $c$ but some arbitrary pair of
possibly distinct colours $(c,c^{\prime})$. However, the idea outlined above
can be turned into a proper reduction from graph FPHP formulas to
$k$-colouring instances by using appropriately constructed gadgets of constant
size.

We then combine this reduction with the recent polynomial calculus degree
lower bound in [MN15], which works as long as the underlying bipartite graph
is a _boundary expander_ (a.k.a.  _unique-neighbour expander_). More
precisely, we show that the reduction from FPHP to graph $k$-colouring
sketched above can be computed in polynomial calculus in low degree.
Therefore, any low-degree polynomial calculus refutations of the graph
$k$-colouring instances could be used to obtain low-degree refutations of FPHP
instances, but [MN15] tells us that FPHP instances over expander graphs
require linear degree.

In order to obtain Corollary 1.2, we assume that we have a low-degree
Nullstellensatz certificate (or, more generally, a polynomial calculus proof)
of non-colourability for the roots-of-unity encoding in [DLMM08, DLMM11]. Then
it is not hard to show that if the field we are working in contains a
primitive $k$th root of unity, we can apply a linear variable substitution to
obtain a polynomial calculus refutation in essentially the same degree of the
colouring instance in the encoding with $\\{0,1\\}$-valued variables. The
corollary now follows from Theorem 1.1.

As should be clear from the discussion above, the hardness of our graph
colouring instances ultimately derives from the pigeonhole principle. However,
this combinatorial principle is well-known to be easy for cutting planes. We
establish Proposition 1.3 by showing that cutting planes can unpack the
reduction described above to recover the original pigeonhole principle
instance, after which this instance can be efficiently refuted.

###  1.4 Outline of This Paper

The rest of this paper is organized as follows. We start by presenting some
proof complexity preliminaries and discussing how to encode the graph
colouring problem in Section 2. In Section 3 we describe our graph
$k$-colouring instances and prove that they are hard for polynomial calculus,
and in Section 4 we show that the same instances are easy for cutting planes.
We conclude in Section 5 by discussing some directions for future research.

##  2 Preliminaries

Throughout this paper $x_{1},\ldots,x_{n}$ denote $\\{0,1\\}$-valued
variables, where we think of $1$ as true and $0$ as false. We write
$\mathbb{N}=\\{0,1,2,\ldots\\}$ for the natural numbers and denote
$\mathbb{N}^{+}=\mathbb{N}\setminus\\{0\\}$. For $n\in\mathbb{N}^{+}$ we use
the standard notation $[n]=\\{1,2,\ldots,n\\}$. For a set $E$, we use the
shorthand $e\neq e^{\prime}\in E$ to index over pairs of distinct elements
$e,e^{\prime}\in E$, $e\neq e^{\prime}$.

###  2.1 Proof Complexity

_Polynomial calculus (PC)_ [CEI96] is a proof system based on algebraic
reasoning where one expresses constraints over Boolean variables as polynomial
equations and applies algebraic manipulations to deduce new equations. The
constraints are over $\\{0,1\\}$-valued variables $x_{1},\ldots,x_{n}$, and
each constraint is encoded as a polynomial $Q$ in the ring
$\mathbb{F}[x_{1},\ldots,x_{n}]$, where $\mathbb{F}$ is some fixed field. The
intended meaning is that $Q=0$ if and only if the constraint is satisfied, but
we omit “$=0$” below and only write the polynomial $Q$. A _PC derivation_ of a
polynomial $R$ from a set of polynomials
$\mathcal{S}=\\{Q_{1},\ldots,Q_{m}\\}$ is a sequence $(P_{1},\ldots,P_{\tau})$
such that $P_{\tau}=R$ and for $1\leq t\leq\tau$ the polynomial $P_{t}$ is
obtained by one of the following derivation rules:

  * •

Boolean axiom: $P_{t}$ is $x^{2}-x$ for some variable $x$;

  * •

Initial axiom: $P_{t}$ is one of the polynomials $Q_{j}\in\mathcal{S}$;

  * •

Linear combination: $P_{t}=\alpha P_{i}+\beta P_{j}$ for $1\leq i,j<t$ and
some $\alpha,\beta\in\mathbb{F}$;

  * •

Multiplication: $P_{t}=xP_{i}$ for $1\leq i<t$ and some variable $x$.

A _PC refutation_ of $\mathcal{S}$ is a derivation of the multiplicative
identity $1$ of $\mathbb{F}$ from $\mathcal{S}$. Note that the Boolean axioms
make sure that variables can only take values $0$ and $1$. For this reason, we
can assume without loss of generality that all polynomials appearing in PC
derivations are multilinear.

The _size_ of a polynomial $P$ is the number of distinct monomials in it when
it is expanded out as a linear combination of monomials,111Just to make
terminology precise, in this paper a _monomial_ is a product of variables, a
_term_ is a monomial multiplied by a non-zero coefficient from the field
$\mathbb{F}$, and a _polynomial_ is always considered as a linear combinations
of terms over pairwise distinct monomials. and the _degree_ of $P$ is the
largest (total) degree of any monomial in $P$. The size of a PC derivation
$\pi$ is the sum of the sizes of all polynomials in $\pi$, and the degree is
the maximal degree of any polynomial in $\pi$. One can also define the
_length_ of a PC derivation as the number of derivation steps in it, but this
not so interesting a measure since it may fail to take account of polynomials
of exponential size.222Indeed, if multiplication is defined to multilinearize
polynomials automatically, as in, e.g., [AR03], then any unsatisfiable CNF
formula encoded into polynomials in the natural way can be refuted in linear
length—see [MN15] for details. A fundamental fact about PC is that the size
and degree measures are tightly related as stated next.

######  Theorem 2.1 ([IPS99]).

For any set $\mathcal{S}$ of inconsistent polynomials of degree at most
$d^{\prime}$ over $n$ variables it holds that if the minimum degree of any PC
refutation for $\mathcal{S}$ is at least $d$, then any PC refutation of
$\mathcal{S}$ has size
$\exp\bigl{(}\Omega\bigl{(}(d-d^{\prime})^{2}/n\bigr{)}\bigr{)}$.

In particular, if the polynomials in $\mathcal{S}$ have constant degree but
require refutations of degree linear in the number of variables $n$, then any
refutation must have exponential size.

We remark that there is also a slightly more general version of this proof
system known as _polynomial calculus (with) resolution (PCR)_ [ABRW02]. The
difference is that PCR has separate formal variables $x$ and $\overline{x}$ to
represent both positive and negative literals when translating CNF formulas
into sets of polynomials, as well as _complementarity axioms_
$x+\overline{x}-1$ to ensure that $x$ and $\overline{x}$ take opposite values.
This yields a nicer and more well-behaved proof system. The change from PC to
PCR does not affect the degree needed to refute an inconsistent set of
polynomial equations, however, and Theorem 2.1 holds also for PCR. Therefore,
the lower bounds we show in this paper apply both to PC and PCR. The presence
of Boolean axioms allows to derive $\prod_{i}x_{i}^{\ell_{i}}-\prod_{i}x_{i}$
for $\ell_{i}\geq 1$ in degree $\sum_{i}\ell_{i}$ and polynomial size.
Therefore whenever we need to derive some polynomial it is sufficient to
derive its multilinear version.

Another aspect worth noticing is that it makes perfect sense to define
polynomial calculus also for sets of polynomial equations that do not include
Boolean axioms $x^{2}-x$. One variant studied in the literature is to add
include axioms $x^{k}-1$ instead, i.e., to insist that the value of $x$ should
be a $k$th root of unity. In such a setting it is no longer necessarily true
that large degree implies large size, however.

In this paper we will also consider _cutting planes (CP)_ [CCT87], which is a
proof system based on manipulation of inequalities
$\sum_{i}a_{i}x_{i}\geq\gamma$ where $a_{i}$ and $\gamma$ are integers and
$x_{1},\ldots,x_{n}$ are $\\{0,1\\}$-valued variables. A _CP derivation_ of an
inequality $B$ from a set of inequalities
$\mathcal{S}=\\{A_{1},\ldots,A_{m}\\}$ is a sequence $(B_{1},\ldots,B_{\tau})$
such that $B_{\tau}=B$ and for $1\leq t\leq\tau$ the inequality $B_{t}$ is
obtained by one of the following derivation rules:

  * •

Variable axiom: $B_{t}$ is either $x\geq 0$ or $-x\geq-1$ for some variable
$x$.

  * •

Initial axiom: $B_{t}$ is some $A_{j}\in\mathcal{S}$;

  * •

Sum: $B_{t}=B_{i}+B_{j}$ for $1\leq i,j<t$.

  * •

Scalar multiplication: $B_{t}=cB_{i}$ for $1\leq i<t$ and $c\in\mathbb{N}$;

  * •

Division: The inequality $B_{t}$ is

$\sum_{i}\frac{a_{i}}{c}x_{i}\geq\left\lceil\frac{\gamma}{c}\right\rceil$
(2.1)

where $c$ divides all $a_{1},\ldots,a_{n}$ and $\sum_{i}a_{i}x_{i}\geq\gamma$
is some inequality $B_{i}$ for $1\leq i<t$.

A CP refutation of $\mathcal{S}=\\{A_{1},\ldots,A_{m}\\}$ is a derivation from
$\mathcal{S}$ of the inequality $0\geq 1$. In what follows, we will often
write $\sum_{i}a_{i}x_{i}\leq\gamma$ as an alias for
$\sum_{i}-a_{i}x_{i}\geq-\gamma$, and we will also use
$\sum_{i}a_{i}x_{i}=\gamma$ as a shorthand for the two inequalities
$\sum_{i}a_{i}x_{i}\leq\gamma$ and $\sum_{i}a_{i}x_{i}\geq\gamma$.

The _length_ of a CP derivation is the number of derivation steps in it. The
_size_ of a linear inequality $\sum_{i}a_{i}x_{i}\geq\gamma$ is the number of
variables plus the bit size of representations of the constant term $\gamma$
and all coefficients $a_{i}$, and the size of a CP derivation $\pi$ is the sum
of the sizes of all inequalities in $\pi$. We do not know of any degree-like
measure for CP that would yield relation as that between size and degree for
PC in Theorem 2.1. One usually does not distinguish too carefully between
length and size for CP since by [BC96] all coefficients in a CP refutation can
be assumed to have at most exponential size, and are hence representable with
a linear number of bits.

For a partial mapping $\rho:D\to R$ from a domain $D$ to a range $R$ we let
$\operatorname{dom}(\rho)$ denote the set of element with an image. For $d\in
D\setminus\operatorname{dom}(\rho)$ we write $\rho(d)=*$. Given a partial
assignment or _restriction_ $\rho$ of variables $x_{1},\ldots,x_{n}$ to values
in $\\{0,1\\}$ and a polynomial $P$ or a linear inequality $A$, we denote by
${{P}\\!\\!\upharpoonright_{\rho}}$ and ${{A}\\!\\!\upharpoonright_{\rho}}$
the polynomial and linear inequality obtained from $P$ and $A$ by restricting
the variables in the domain of $\rho$ to the corresponding values and making
obvious syntactic simplifications. Given a derivation $\pi$ in PC or CP, we
denote by ${{\pi}\\!\\!\upharpoonright_{\rho}}$ the sequence of restricted
polynomials or linear inequalities, respectively. It is straightforward to
verify that if $\pi$ is a CP derivation of an inequality $A$ from
$\mathcal{S}$, then ${{\pi}\\!\\!\upharpoonright_{\rho}}$ can be viewed (after
simple syntactic manipulations) as a derivation of
${{A}\\!\\!\upharpoonright_{\rho}}$ from
${{\mathcal{S}}\\!\\!\upharpoonright_{\rho}}$ of at most the same length, and
the same holds for PC with respect to size and degree.

###  2.2 The Graph Colouring Problem

A _legal $k$-colouring_ of an undirected graph $G=(V,E)$ with vertices
$V(G)=V$ and edges $E(G)=E$ is a mapping $\chi:V\to[k]$ such that for every
edge $(u,v)\in E$ it holds that $\chi(u)\neq\chi(v)$. The _chromatic number_
$\chi(G)$ of $G$ is the smallest $k$ such that a legal $k$-colouring of $G$
exists. In the rest of this paper, colourings will often be assumed to be
legal unless specified otherwise, so we will sometimes omit this prefix when
no misunderstanding can occur. Also, it will sometimes be convenient to number
the $k$ colours $0,1,\ldots,k-1$ instead of $1,2,\ldots,k$, and we will be
fairly relaxed about this issue, implicitly identifying colours $0$ and $k$
whenever convenient.

Given a graph $G$ we can encode the $k$-colourability problem in a natural way
as a system of polynomial equations over Boolean variables

$\displaystyle\sum^{k}_{j=1}x_{v,j}$ $\displaystyle=1$ $v\in V(G)$, (2.2a)
$\displaystyle x_{v,j}x_{v,j^{\prime}}$ $\displaystyle=0$ $v\in V(G)$, $j\neq
j^{\prime}\in[k]$, (2.2b) $\displaystyle x_{u,j}x_{v,j}$ $\displaystyle=0$
$(u,v)\in E(G)$, $j\in[k]$, (2.2c)

with the intended meaning that $x_{v,j}=1$ if vertex $v$ has colour
$\chi(v)=j$. It is clear that this system of equations has a solution if and
only if the graph $G$ is $k$-colourable.

We will also be interested in an alternative algebraic representation of the
$k$-colouring problem appearing, e.g., in [DLMM08, DLMO09, DLMM11]. In this
encoding every vertex $v\in V$ has a single associated variable $y_{v}$ which
takes values in $\\{1,\omega,\omega^{2},\ldots,\omega^{k-1}\\}$, where
$\omega$ is a primitive $k$th root of unity. The intended meaning is that
$y_{v}=\omega^{j}$ if vertex $v$ has colour $j\in\\{0,1,\ldots,k-1\\}$. The
colouring constraints are enforced by the polynomial equations

$\displaystyle y_{v}^{k}$ $\displaystyle=1$ $v\in V(G)$, (2.3a)
$\displaystyle\sum^{k-1}_{j=0}{(y_{u})}^{j}{(y_{v})}^{k-1-j}$
$\displaystyle=0$ $(u,v)\in E(G)$, (2.3b)

where the polynomials live in a polynomial ring over a field of characteristic
that is not a positive number dividing $k$. Clearly, Equation (2.3a) forces
the vertex $v$ to take some colour. A moment of thought reveals that Equation
(2.3b) correctly encodes an edge constraint: if $y_{u}=\omega^{a}$ and
$y_{v}=\omega^{b}$, then the sum evaluates to
$\omega^{b(k-1)}\sum^{k-1}_{j=0}\omega^{j(a-b)}$, which equals $0$ when $a\neq
b$ and $k\omega^{b(k-1)}\neq 0$ otherwise. The latter formulation of
$k$-colouring only makes sense if the characteristic of the underlying field
$\mathbb{F}$ is either $0$ or a positive integer that does not divide $k$. In
this case, we also know that there exists an extension field $\mathbb{E}$ of
$\mathbb{F}$ that contains a primitive $k$th root of unity $\omega$ [Lan05,
Chapter VI.3].

A simple but important observation for us is that the choice of the polynomial
encoding is not too important if we want to study how large degree is needed
in polynomial calculus when proving that some graph $G$ is not $k$-colourable,
provided that the field we are in contains, or can be extended to contain, a
primitive $k$th root of unity.

######  Proposition 2.2.

Suppose that Equations (2.3a)–(2.3b) have a polynomial calculus refutation of
degree $d$ over some field $\mathbb{F}$ of characteristic that is not a
positive number dividing $k$. Then $\mathbb{F}$ can be extended to a field
$\mathbb{E}$ containing a primitive $k$th root of unity $\omega$, and it holds
that Equations (2.2a)–(2.2c) have a polynomial calculus refutation over
$\mathbb{E}$ of degree $\max\\{2k,d\\}$.

###### Proof.

By the assumption on the characteristic of $\mathbb{F}$, we already argued
that there exists some extension field $\mathbb{E}$ of $\mathbb{F}$ that
contains a primitive $k$th root of unity $\omega$. We plan to translate a
polynomial calculus refutation $\pi$ of Equations (2.3a)–(2.3b), into a
refutation of Equations (2.2a)–(2.2c), and the first step of this process is
to apply the linear substitutions

$y_{v}\mapsto\sum^{k}_{j=1}x_{v,j}\omega^{j}$ (2.4)

to all variables in all polynomials in $\pi$ to obtain a new sequence of
polynomials $\pi^{\prime}$ in variables $x_{v,j}$. These substituted
polynomials in $\pi^{\prime}$ have coefficients in $\mathbb{E}$ and we will
use them to form the skeleton of our new refutation. In order to turn
$\pi^{\prime}$ into a refutation of Equations (2.2a)–(2.2c) we are going to

  * •

show that for every application of a derivation rule in $\pi$, it is possible
to derive the corresponding substituted consequence from the substituted
premises with no increase in the degree;

  * •

show that the substituted axioms in $\pi^{\prime}$ can be derived from
Equations (2.2a)–(2.2c) in degree $2k$.

The first item is almost immediate. All applications of the linear combination
rule in $\pi$ remain valid in $\pi^{\prime}$, since the substitution is a
linear operator. When $y_{u}p$ is derived from $p$ in $\pi$ by the means of an
application of the multiplication rule, in the new refutation we need to
derive $\sum^{k}_{j=1}x_{v,j}\omega^{j}p^{\prime}$ from $p^{\prime}$, where
$p^{\prime}$ is the substituted version of $p$. To do that it is sufficient to
derive each $x_{v,j}p^{\prime}$ from $p^{\prime}$ and then take a linear
combination. Notice that the degree of this derivation is the same as in
$\pi$.

It remains to argue is that the substituted versions of the initial axioms
(2.3a)–(2.3b) in $\pi$ can be derived from the axioms (2.2a)–(2.2c) available
to the new refutation. We first derive the substituted version of the axiom
$y_{v}^{k}-1$ (which is just axiom (2.3a) with the additive $1$ moved to the
left side), namely

${\left(\sum^{k}_{j=1}x_{v,j}\omega^{j}\right)}^{k}-1\enspace,$ (2.5)

which after expansion becomes

$\sum^{k}_{j=1}x_{v,j}^{k}\omega^{jk}-1+Q\enspace.$ (2.6)

where each monomial in $Q$ contains some factor on the form
$x_{v,j}x_{v,j^{\prime}}$ for $j\neq j^{\prime}$. We use that $\omega^{k}$ is
$1$ and we rewrite (2.6) as

$\sum^{k}_{j=1}\sum_{\ell=0}^{k-2}x_{v,j}^{\ell}(x_{v,j}^{2}-x_{v,j})+\left(\sum^{k}_{j=1}x_{v,j}-1\right)+Q\enspace,$
(2.7)

The $Q$ part is derivable from axioms (2.2b), and the rest can be derived from
boolean axioms and axiom (2.2a).

Now we focus on the substituted axiom (2.3b), which is

$\sum^{k-1}_{j=0}{\left(\sum^{k}_{a=1}x_{u,a}\omega^{a}\right)}^{j}{\left(\sum^{k}_{b=1}x_{v,b}\omega^{b}\right)}^{k-1-j}\enspace.$
(2.8)

It will be more convenient for us to first derive the polynomial of degree
$2k-1$

$\sum^{k-1}_{j=0}{\left(\sum^{k}_{a=1}x_{u,a}\omega^{a}\right)}^{k+j}{\left(\sum^{k}_{b=1}x_{v,b}\omega^{b}\right)}^{2k-1-j}\enspace,$
(2.9)

and then show that it is equivalent to (2.8) using the equation (2.5) proved
above. After expansion polynomial (2.9) becomes

$\sum^{k-1}_{j=0}\sum^{k}_{a=1}\sum^{k}_{b=1}x_{u,a}^{k+j}x_{v,b}^{(2k-1-j)}\omega^{(k+j)a}\omega^{(2k-1-j)b}\quad+\quad
Q^{\prime}\enspace,$ (2.10)

where each monomial in $Q^{\prime}$ contains either some factor
$x_{u,a}x_{u,a^{\prime}}$ for $a\neq a^{\prime}$ or some
$x_{v,b}x_{v,b^{\prime}}$ for $b\neq b^{\prime}$. Since $k+j$ and $2k-1+j$ are
both greater than zero for $j\in[0,k-1]$, the Boolean axioms can be used to
prove the equivalence of each $x_{u,a}^{k+j}x_{v,b}^{(2k-1-j)}$ with
$x_{u,a}x_{v,b}$. This fact, together with the fact that $\omega^{k}=1$,
allows us to reduce to the derivation of

$\sum^{k-1}_{j=0}\sum^{k}_{a=1}\sum^{k}_{b=1}x_{u,a}x_{v,b}\omega^{ja}\omega^{(k-1-j)b}\quad+\quad
Q^{\prime}\enspace.$ (2.11)

All monomial in $Q^{\prime}$ are derivable from axioms (2.2b). To derive first
summand we change the order of the summation and split it into two parts,
depending on whether $a=b$, to obtain

$\sum^{k}_{a=1}x_{u,a}x_{v,a}\sum^{k-1}_{j=0}\omega^{ja}\omega^{(k-1-j)a}\quad+\quad\sum^{k}_{a=1}\sum^{k}_{b=1,b\neq
a}x_{u,a}x_{v,b}\underbrace{\left(\omega^{b(k-1)}\sum^{k-1}_{j=0}\omega^{j(a-b)}\right)}_{\text{equal
to $0$ for $a\neq b$}}\enspace.$ (2.12)

The axioms (2.2c) allow to derive the first part of (2.12), while the second
part is identically zero. In conclusion we have shows how to derive
substituted axioms (2.5) and (2.8) in degree $\leq 2k$ and therefore we have
concluded the translation of refutation $\pi$. ∎

For later use, we note that we can also encode the $k$-colourability problem
for a graph $G$ as a system of linear inequalities

$\displaystyle\sum^{k}_{j=1}x_{v,j}$ $\displaystyle\geq 1$ $v\in V(G)$,
(2.13a) $\displaystyle x_{v,j}+x_{v,j^{\prime}}$ $\displaystyle\leq 1$ $v\in
V(G)$, $j\neq j^{\prime}\in[k]$, (2.13b) $\displaystyle x_{u,j}+x_{v,j}$
$\displaystyle\leq 1$ $(u,v)\in E(G)$, $j\in[k]$, (2.13c) in a format amenable
to cutting planes reasoning.

##  3 Worst-Case Lower Bound for Polynomial Calculus

We now show how to explicitly construct a family of graphs which are not
$k$-colourable but for which polynomial calculus proofs of this fact (over any
field) require degree linear in the number of vertices in the graphs. We do
this in three steps:

  1. 1.

First, we show how to reduce instances of _functional pigeonhole principle
(FPHP) formulas_ defined over bipartite graphs of bounded degree to graph
colouring instances so that there is a one-to-one mapping of pigeons to holes
if and only if the graph is $k$-colourable.

  2. 2.

Then we show that polynomial calculus is able to carry out this reduction in
constant degree, so that a low-degree PC proof of graph non-colourability can
be used to obtain a low-degree refutation of the corresponding FPHP instance.

  3. 3.

Finally, we appeal to a linear lower bound on degree for refuting FPHP
instances over bipartite expander graphs from [MN15].

Let us start by giving a precise description of our functional pigeonhole
principle instances. We have a set of pigeons $I$ which want to fly into a set
of holes $J$, with each pigeon flying into exactly one hole in a one-to-one
fashion. However, the choices of holes for the pigeons are constrained, so
that pigeon $i$ can fly only to the holes in $J({i})\subseteq J$, where we
have $\lvert J({i})\rvert=k$. If we use variables $p_{i,j}$ to denote that
pigeon $i$ flies into hole $j$, we can write the constraints on such a mapping
as a set of polynomial equations

$\displaystyle\sum_{j\in J({i})}p_{i,j}$ $\displaystyle=1$ $i\in I$, (3.1a)
$\displaystyle p_{i,j}p_{i,j^{\prime}}$ $\displaystyle=0$ $i\in I$, $j\neq
j^{\prime}\in J({i})$. (3.1b) $\displaystyle p_{i,j}p_{i^{\prime},j}$
$\displaystyle=0$ $i\neq i^{\prime}\in I$, $j\in J({i})\cap J({i^{\prime}})$.
(3.1c)

Note that an instance encoded by Equations (3.1a)–(3.1c) can also be naturally
viewed as a bipartite graph $B$ with left vertex set $I$, right vertex set
$J$, and edges from each $i\in I$ to all $j\in J({i})$. In what follows, we
will mostly reason about FPHP instances in terms of their representations as
bipartite graphs.

In the standard setting, we let $I=[n]$ and $J=[n-1]$ for some
$n\in\mathbb{N}$, in which case the collection of constraints (3.1a)–(3.1c) is
clearly unsatisfiable. Nevertheless, it was shown in [MN15] that if the
underlying bipartite graph is a so-called _boundary expander_ , then any PC
refutation of Equations (3.1a)–(3.1c) requires $\Omega(n)$ degree and thus, by
Theorem 2.1, exponential size. The _boundary_ of some set $X$ of vertices in a
(either simple or bipartite) graph $G$ is the set of vertices in
$V(G)\setminus X$ that have exactly one neighbor in $X$. Informally, a
(bipartite) boundary expander is (bipartite) graph for which every set of
(left) vertices of reasonable size has large boundary. For our results we do
not need to go into the technical details of the lower bound for FPHP. It
suffices to use the following claim as a black box.

######  Theorem 3.1 (By the proof of [MN15]).

For any integer $k\geq 3$, consider a family of bipartite graphs
$\\{B_{n}\\}_{n\in\mathbb{N}}$ with

  * •

$n$ vertices on the left side, $n-1$ vertices on the right side, left degree
$k$, and right degree $\mathrm{O}(k)$,

  * •

there are universal constants $\alpha,\delta$ so that for any $n\in\mathbb{N}$
and any set $I$ of at most $\alpha n$ vertices on the left side of $B_{n}$,
the size of the boundary of $I$ is at least $\delta|I|-1$.

Any polynomial calculus refutation of the constraints (3.1a)–(3.1c)
corresponding to $B_{n}$ requires degree $\Omega(n)$.

To be precise, the lower bound in Theorem 3.1 was proven for a slightly
different encoding of Equations (3.1a)–(3.1c)—namely the one obtained from the
natural translation of CNF formulas into polynomial equations—but the two
encodings imply each other and can be used to derive each other in degree
$\mathrm{O}(k)$ by the implicational completeness of polynomial calculus.
Hence, the lower bound holds for both encodings.

We proceed to describe the reduction from functional pigeonhole principle
instances to graph colouring instances. Our starting point is an FPHP instance
on a bipartite graph $B$ with pigeons $I=[n]$ and holes $J$ where every pigeon
has exactly $d_{I}=k$ holes to choose from and every hole can take
$\mathrm{O}(k)$ pigeons; i.e., the bipartite graph $B$ is left-regular of
degree $k$ and has right degree $\mathrm{O}(k)$. Based on this instance we
construct a graph $G=G(B)$ such that $G$ is $k$-colourable if and only if the
functional pigeonhole principle on $B$ is satisfiable.

By way of overview, the graph $G(B)$ has $n$ special vertices corresponding to
the pigeons, and the colours of these vertices encode how the pigeons are
mapped to holes. For every pair of pigeons $i,i^{\prime}$ that can be mapped
to the same hole $j$ we add a gadget that forbids the colouring of the pigeon
vertices $i$ and $i^{\prime}$ that corresponds to them being mapped to hole
$j$. These gadgets have a couple of pre-coloured vertices, but we eliminate
such pre-colouring by adding one more simple gadget.

In more detail, the main idea behind the reduction is to view the choices
$J({i})$ for each pigeon $i\in I$ as taking the first, second, …, $k$th edge.
We fix an arbitrary enumeration of the elements of $J({i})$ for each $i\in I$,
associating distinct numbers $1,2,\ldots,k$ to the edges out of the vertex $i$
in $B$. We say that _pigeon $i$ flies to hole $j$ using its $c$th edge_ if the
edge connecting pigeon $i$ to hole $j$ is labelled by $c\in[k]$, and use the
notation ${i}\leftarrow{c}$ for this (suppressing the information about the
hole $j$). Pigeon $i$ taking the $c$th edge corresponds to the special $i$th
pigeon vertex being coloured with colour $c$.

Consider two distinct pigeons $i\neq i^{\prime}\in I$ and a hole $j\in
J({i})\cap J({i^{\prime}})$. If pigeon $i{}$ flies to hole $j$ using its $c$th
edge and pigeon $i{}^{\prime}$ flies to hole $j$ using its $c^{\prime}$th
edge, then the translation of the injectivity constraint (3.1c) expressed in
terms of $k$-colourings is that vertices $i$ and $i{}^{\prime}$ cannot be
simultaneously coloured by colours $c$ and $c^{\prime}$, respectively.

(a) Gadget ruling out ${i}\leftarrow{c}$ and ${i^{\prime}}\leftarrow{c}$.

(b) Gadget ruling out ${i}\leftarrow{c}$ and
${i^{\prime}}\leftarrow{c^{\prime}}$ for $c\neq c^{\prime}$.

Figure 1: Injectivity constraint gadgets
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ for $k=4$.

Let us now give a precise description of the graph gadgets we employ to
enforce such injectivity constraints. These will be partially pre-coloured
graphs $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ as depicted in
Figures 1(a) and 1(b). The gadget constructions start with two disjoint
$k$-cliques for pigeons $i$ and $i^{\prime}$. For the sake of exposition we
call the former the left clique and the latter the right clique, although the
construction fully symmetric. We refer to the vertices in the left clique as
$\ell_{1},\ldots,\ell_{k}$ numbered in a clockwise fashion starting with the
first vertex at the bottom, and in a symmetric fashion the vertices in the
right clique are referred to as $r_{1},\ldots,r_{k}$ numbered anti-clockwise
starting at the bottom.

To the first vertex $\ell_{1}$ in the left $k$-clique we connect the vertex
$i$. To vertices $\ell_{2},\ldots,\ell_{k-1}$ we connect a new vertex pre-
coloured with colour $c$. For the right $k$-clique we do a similar
construction: to the first vertex $r_{1}$ we connect the vertex $i^{\prime}$
and to the next $k-2$ vertices $r_{2},\ldots,r_{k-1}$ we connect a new vertex
pre-coloured with colour $c^{\prime}$.

The final step of the construction depends on whether $c=c^{\prime}$ or not.
If $c=c^{\prime}$, then we add an edge between the final two vertices
$\ell_{k}$ and $r_{k}$ in the cliques. If $c\neq c^{\prime}$, then we instead
merge these two vertices into a single vertex as shown in Figure 1(b). We want
to stress that except for $i$ and $i^{\prime}$ all vertices in the
construction are new vertices that do not occur in any other gadget. Let us
collect for the record some properties of this gadget construction.

######  Claim 3.2.

The pre-coloured graph gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ has the following
properties:

  1. 1.

$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ has $\mathrm{O}(k)$
vertices.

  2. 2.

$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ has two pre-coloured
vertices of degree $\mathrm{O}(k)$.

  3. 3.

For every $(b,b^{\prime})\neq(c,c^{\prime})$ there is a legal $k$-colouring
$\chi$ of $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ extending
the pre-colouring and satisfying $\chi({i})=b$ and
$\chi({i^{\prime}})=b^{\prime}$. No such legal $k$-colouring of
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ exists for
$(b,b^{\prime})=(c,c^{\prime})$.

###### Proof.

The first two properties obviously hold by construction.

To prove Property 3, let us focus on the left clique in either of the two
variant of the gadget. If $\chi({i})=c$, then clearly vertex $\ell_{1}$ in the
left clique cannot take colour $c$. Since the pre-coloured vertex connected to
vertices $\ell_{2},\ldots,\ell_{k-1}$ of the clique also has colour $c$, and
since any legal colouring must use all available colours for the clique, this
forces $\chi({\ell_{k}})=c$. If $\chi({i})\neq c$, however, then we can colour
vertex $\ell_{1}$ with colour $c$, and then choose any permutation of the
remaining colours for the other vertices in the left clique, giving the vertex
$\ell_{k}$ at least two distinct colours to choose between after the other
clique vertices $\ell_{2},\ldots,\ell_{k-1}$ connected to the pre-coloured
vertex have been coloured.

Consider now the case $c=c^{\prime}$, so that we have the graph gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c})}$ in Figure 1(a). By symmetry,
if $\chi({i^{\prime}})=c^{\prime}$, then this forces $\chi({r_{k}})=c$, but
there are at least two choices for the colour of $r_{k}$ if
$\chi({i^{\prime}})\neq c^{\prime}$. It follows that if ${i}\leftarrow{c}$ and
${i^{\prime}}\leftarrow{c}$, then vertices $\ell_{k}$ and $r_{k}$ both have to
get the same colour $c$ to avoid conflicts in the left and right $k$-cliques,
respectively, which causes a conflict along the edge $(\ell_{k},r_{k})$. As
long as one of $i$ and $i^{\prime}$ is assigned a colour other than $c$,
however, $G_{({i},{i^{\prime}})\not\leftarrow({c},{c})}$ can be legally
$k$-coloured.

For $c\neq c^{\prime}$ we instead have the graph gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ in Figure 1(b).
Following the same line of reasoning as above, if ${i}\leftarrow{c}$, then the
left $k$-clique forces $\ell_{k}$ to take colour $c$, and if
${i^{\prime}}\leftarrow{c^{\prime}}$, then the right $k$-clique forces
$r_{k}=\ell_{k}$ to take colour $c^{\prime}\neq c$, which is a conflict. If
${i}\leftarrow{c}$ but ${i^{\prime}}\not\leftarrow{c^{\prime}}$, however, then
$\ell_{k}$ can first be coloured with colour $c$ to satisfy the left
$k$-clique, after which the $k$-colouring of the right $k$-clique can be
completed taking $\chi({\ell_{k}})$ into consideration, and the reasoning is
symmetric if ${i^{\prime}}\leftarrow{c^{\prime}}$ but ${i}\not\leftarrow{c}$.
The case when both ${i}\not\leftarrow{c}$ and
${i^{\prime}}\not\leftarrow{c^{\prime}}$ is dealt with in a similar way. This
establishes the claim. ∎

We write $\widehat{G}=\widehat{G}(B)$ to denote the graph consisting of the
union of all gadgets $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$
for all $i\neq i^{\prime}\in I$ and all $c,c^{\prime}$ such that if pigeon $i$
uses its $c$th edge and pigeon $i^{\prime}$ uses its $c^{\prime}$th edge in
$B$, then they both end up in the same hole $j\in J$. All vertices
corresponding to pigeons $i\in I$ are shared between gadgets
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ in $\widehat{G}$, but
apart from this all subgraphs
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ are vertex-disjoint.
We next state some properties of $\widehat{G}$.

######  Lemma 3.3.

Consider an FPHP instance encoded by Equations (3.1a)–(3.1c) for a left-
regular bipartite graph with left degree $d_{I}=k$ and bounded right degree
$d_{J}=\mathrm{O}(k)$, and let $\widehat{G}$ be the partially $k$-coloured
graph obtained as described above. Then $\widehat{G}$ has
$\mathrm{O}\bigl{(}k^{4}\lvert I\rvert\bigr{)}$ vertices and maximal vertex
degree $\mathrm{O}(k^{2})$, and the number of pre-coloured vertices is
$\mathrm{O}\bigl{(}k^{2}\lvert I\rvert\bigr{)}$. Furthermore, the partial
$k$-colouring of $\widehat{G}$ can be extended to a complete, legal
$k$-colouring of $\widehat{G}$ if and only if there is a way to map each
pigeon $i\in I$ to some hole $j\in J$ without violating any constraint in
(3.1a)–(3.1c).

###### Proof.

Without loss of generality we can assume that $\lvert J\rvert\leq k\lvert
I\rvert$ (otherwise there are holes that cannot be used by any pigeon and that
can thus be discarded). Each gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ has $\mathrm{O}(k)$
vertices and there are at most $(d_{J})^{2}=\mathrm{O}\bigl{(}k^{2}\bigr{)}$
distinct pairs of pigeons that can fly to any single hole $j$, meaning that we
have a total of at most $\mathrm{O}\bigl{(}k^{2}\lvert J\rvert\bigr{)}$
injectivity constraint gadgets
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$. Therefore, by a
crude estimate $\widehat{G}$ has at most $\mathrm{O}\bigl{(}k^{4}\lvert
I\rvert\bigr{)}$ vertices in total.

By Claim 3.2 at most $\mathrm{O}\bigl{(}k^{2}\lvert I\rvert\bigr{)}$ vertices
in $\widehat{G}$ are pre-coloured. Each pigeon vertex labelled by $i\in I$ is
involved in at most $d_{I}d_{J}=\mathrm{O}\bigl{(}k^{2}\bigr{)}$ injectivity
constraint gadgets, so such vertices have degree
$\mathrm{O}\bigl{(}k^{2}\bigr{)}$, while all other vertices have degree
$\mathrm{O}(k)$.

For any complete colouring of $\widehat{G}$ extending the pre-colouring, the
colours $\chi({i})=c_{i}$ assigned to pigeon vertices $i\in I$ define a
mapping from pigeons to holes via the chosen edges $c_{i}$. It follows from
Claim 3.2 that this colouring is legal only if pigeons are mapped to holes in
a one-to-one fashion, which implies that Equations (3.1a)–(3.1c) are
satisfiable. In the other direction, for any one-to-one mapping of pigeons to
holes we can colour vertex $i$ by the colour $c_{i}$ corresponding to the edge
it uses to fly to its hole, and such a colouring can be combined with the pre-
colouring complete, to produce a legal $k$-colouring. ∎

To finalize our reduction we need to get rid of the pre-coloured vertices in
$\widehat{G}$. To this end, we first make the following observation. Recall
that for every every pigeon $i\in I$ we fixed an enumeration of the edges to
holes $j\in J({i})$ in $B$, so that the choice of an edge corresponds to the
choice of a colour. Suppose we apply some arbitrary but fixed permutation
$\sigma$ on $[k]$ to all such enumerations for the pigeons $i\in I$. Clearly,
this does not change the instance in any significant way. If it was the case
before that pigeon $i$ and $i^{\prime}$ could not simultaneously take the
$c$th and $c^{\prime}$th edges, respectively, then now these pigeons cannot
simultaneously take the $\sigma(c)$th and $\sigma(c^{\prime})$th edges,
respectively. In other words, Lemma 3.3 is invariant with respect to any
permutation of the colours $[k]$, and we could imagine the reduction as first
picking some permutation $\sigma$ and then constructing $\widehat{G}$ with
respect to this permutation.

A simple way of achieving this effect would be to construct a separate “pre-
colouring $k$-clique” consisting of $k$ special vertices
$\gamma_{1},\ldots,\gamma_{k}$, and then identify all vertices in
$\widehat{G}$ pre-coloured with colour $c$ with the vertex $\gamma_{c}$. It is
not hard to see that the resulting graph would be $k$-colourable if and only
if the pre-colouring of $\widehat{G}$ could be extended to a complete, legal
$k$-colouring, and using Lemma 3.3 we would obtain a valid reduction from the
functional pigeonhole principle to graph $k$-colouring. However, the final
graph would have degree $\Omega\bigl{(}k^{3}\lvert I\rvert\bigr{)}$, and we
would like to obtain a graph of bounded degree.

Figure 2: Pre-colouring gadget with uncoloured vertices to be identified with
the pre-coloured vertices in $\widehat{G}$.

To keep the graph vertex degree independent of the size $\lvert I\rvert$ of
the left-hand side of the FPHP bipartite graph $B$, we instead construct a
pre-colouring gadget using a slight modification of the above idea. Consider a
set $\\{\gamma_{1},\gamma_{2},\ldots,\gamma_{M}\\}$ of new vertices, for $M$
to be fixed later. For every segment of $k$ consecutive vertices
$\\{\gamma_{t},\gamma_{t+1},\ldots,\gamma_{t+k-1}\\}$ we add all edges
$\bigl{\\{}(\gamma_{c},\gamma_{c^{\prime}})\,\bigl{|}\vphantom{(\gamma_{c},\gamma_{c^{\prime}})\,\,c\neq
c^{\prime}\in\\{t,t+1,\ldots,t+k-1\\}}\mspace{-2.05mu}\bigr{.}\,c\neq
c^{\prime}\in\\{t,t+1,\ldots,t+k-1\\}\bigr{\\}}$ so that they form a
$k$-clique as illustrated in Figure 2 (where as in Figure 1 we have $k=4$).
Next, we go through all the pre-coloured vertices in $\widehat{G}$: if a
vertex should be pre-coloured by $c$, then we identify it with the first
vertex $\gamma_{t}$ such that $t\equiv c\pmod{k}$ and such that $\gamma_{t}$
has not already been assigned at a previous step to some other pre-coloured
vertex. If we choose $M=\mathrm{O}\bigl{(}k^{3}\lvert I\rvert\bigr{)}$, then
we are guaranteed to have enough vertices $\gamma_{t}$ to be able to process
all pre-coloured vertices in this way.

Our final graph $G=G(B)$ is the previous graph $\widehat{G}$ with pre-coloured
vertices identified with (uncoloured) vertices in the additional pre-colouring
gadget as just described. Clearly, $G$ is $k$-colourable if and only if the
pre-colouring of $\widehat{G}$ can be completed to a legal $k$-colouring. We
summarize the properties of our reduction in the following proposition.

######  Proposition 3.4.

Given a graph FPHP formula over a left-regular bipartite graph $B$ with left
degree $d_{I}=k$ and bounded right degree $d_{J}=\mathrm{O}(k)$, there is an
explicit construction of a graph $G=G(B)$ such that $G$ has
$\mathrm{O}\bigl{(}k^{4}\lvert I\rvert\bigr{)}$ vertices of maximal vertex
degree $\mathrm{O}(k^{2})$ and is $k$-colourable if and only if it is possible
to map pigeons to holes in accordance with the restrictions in $B$ in a one-
to-one fashion, i.e., if and only if Equations (3.1a)–(3.1c) are
simultaneously satisfiable.

###### Proof.

The number of vertices of $G=G(B)$ is at most the number of vertices of
$\widehat{G}=\widehat{G}(B)$ plus $M=\mathrm{O}\bigl{(}k^{3}\lvert
I\rvert\bigr{)}$ additional vertices enforcing the pre-colouring. The pre-
coloured vertices in the injectivity constraint gadgets get at most $2k-1$ new
neighbours, so their degree is still $\mathrm{O}(k)$. Hence, the number of
vertices and the vertex degree bound in Lemma 3.3 remain valid.

To prove the soundness and completeness of the reduction, note that any
colouring $(c_{1},\ldots,c_{M})$ of $(\gamma_{1},\ldots,\gamma_{M})$ is
completely determined by the colouring of the first $k$-clique
$\\{\gamma_{1},\ldots,\gamma_{k}\\}$, so that $c_{t}=c_{t^{\prime}}$ holds
whenever $t\equiv t^{\prime}\pmod{k}$.

Assume that $G$ has a $k$-colouring $\chi$. Every vertex that was pre-coloured
with colour $c\in[k]$ in $\widehat{G}$ has colour $\chi({\gamma_{c}})$ in $G$.
This means that the colouring of $G$ induces, up to renaming of colours, a
completion of the partial colouring of $\widehat{G}$. By Lemma 3.3, this
implies that the FPHP instance is satisfiable.

In the other direction, if the FPHP instance is satisfiable we do as in the
proof of Lemma 3.3 and colour each vertex $i$ by the colour $c_{i}$
corresponding to the edge it uses to fly to its hole in some one-to-one
mapping. We also colour vertices $\gamma_{1},\ldots,\gamma_{k}$ with colours
$\chi({\gamma_{t}})=t$, and extend this colouring to the rest of the vertices
in the pre-colouring gadget in Figure 2. By Lemma 3.3 this partial colouring
can be completed to obtain a legal $k$-colouring. ∎

Since our reduction encodes local injectivity constraints into local colouring
constraints, it stands to reason that we should be able to translate between
these two types of constraints using low degree derivations. In particular, it
seems reasonable to expect that any low-degree refutation of the $k$-colouring
problem for $G(B)$ should yield a low-degree refutation for the functional
pigeohole principle on $B$. This is indeed the case, as stated in the next
lemma.

######  Lemma 3.5.

Consider the graph $G=G(B)$ obtained from a bipartite graph $B$ as in
Proposition 3.4. If the $k$-colourability constraints (2.2a)–(2.2c) for $G$
have a PC refutation in degree $d$, then the functional pigeonhole principle
constraints (3.1a)–(3.1c) defined over $B$ have a PC refutation of degree at
most $2d$.

We will spend what remains of this section on proving this lemma. The proof is
quite similar in spirit to that of Proposition 2.2. We start by assuming that
we have a PC refutation of Equations (2.2a)–(2.2c) in degree $d$. Our first
step is to substitute all variables $x_{v,j}$ in this refutation with
polynomials of degree at most $2$ in variables $p_{i,j}$. In the second step,
we argue that if we apply this substitution to the axioms in (2.2a)–(2.2c),
then we can derive the resulting substituted polynomials from Equations
(3.1a)–(3.1c) by PC derivations in low degree. Taken together, this yields a
PC refutation in low degree of the FPHP instance (3.1a)–(3.1c).

To describe the substitution, let us focus on a single gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$. The first step is to
express all equations for this gadget as equations over variables
$x_{i,1},\ldots x_{i,k},x_{i^{\prime},1},\ldots x_{i^{\prime},k}$. Note that
these variables are essentially the same as those from the pigeonhole
principle instance, except that instead of $p_{i,j}$ we use the variable
$x_{i,c}$ where $c$ is the number of the edge pigeon $i$ uses to fly to hole
$j$, but for the sake of exposition we want to keep using the language of
colourings.

Let $w$ and $w^{\prime}$ be the vertices that are supposed to be pre-coloured
with colours $c$ and $c^{\prime}$, respectively. We stress that now we are
considering the graph $G$ which has no pre-coloured vertices, and in
particular all the variables mentioning the vertices $w$ and $w^{\prime}$ are
unassigned. Recall that $w$ and $w^{\prime}$ also appear in the gadget
depicted in Figure 2, where they are identified with some vertices
$\gamma_{t}$ and $\gamma_{t^{\prime}}$ such that $t\equiv c$ and
$t^{\prime}\equiv c^{\prime}\pmod{k}$.

For any pair $(b,b^{\prime})$ of colours different from $(c,c^{\prime})$,
Claim 3.2 guarantees that we can pick some colouring $\chi_{(b,b^{\prime})}$
for the gadget $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ such
that $\chi_{(b,b^{\prime})}(i)=b$,
$\chi_{(b,b^{\prime})}(i^{\prime})=b^{\prime}$, $\chi_{(b,b^{\prime})}(w)=c$
and $\chi_{(b,b^{\prime})}(w^{\prime})=c^{\prime}$. Fix for the rest of this
proof such a colouring $\chi_{(b,b^{\prime})}$ for the gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ for every
$(b,b^{\prime})\neq(c,c^{\prime})$. Then we can write the colour of any vertex
$v$ in $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ other than the
pigeon vertices $i$ and $i^{\prime}$ as a function of $(b,b^{\prime})$. In
more detail, we can express every variable $x_{v,j}$, for
$v\not\in\\{i,i^{\prime}\\}$, as a degree-$2$ polynomial over the variables
$x_{i,1},\ldots x_{i,k},x_{i^{\prime},1},\ldots x_{i^{\prime},k}$ by summing
over the monomials $x_{i,b}x_{i^{\prime},b^{\prime}}$ corresponding to the
choices of colours $(b,b^{\prime})$ for $(i,i^{\prime})$ for which the
colouring $\chi_{(b,b^{\prime})}$ assigns colour $j$ to vertex $v$, or in
symbols

$x_{v,j}\mapsto\sum_{(b,b^{\prime})\neq(c,c^{\prime}),\,\chi_{(b,b^{\prime})}(v)=j}x_{i,b}x_{i^{\prime},b^{\prime}}\enspace.$
(3.2)

Notice that for the vertices $w$ and $w^{\prime}$ the substitutions we obtain
from (3.2) are

$\displaystyle x_{w,c}$ $\displaystyle\ \mapsto\
\sum_{{(b,b^{\prime})\neq(c,c^{\prime})}}x_{i,b}x_{i^{\prime},b^{\prime}}\enspace,$
(3.3a) $\displaystyle x_{w^{\prime},c^{\prime}}$ $\displaystyle\ \mapsto\
\sum_{{(b,b^{\prime})\neq(c,c^{\prime})}}x_{i,b}x_{i^{\prime},b^{\prime}}\enspace,$
(3.3b) $\displaystyle x_{w,b}$ $\displaystyle\ \mapsto\ 0$ (for $c\neq b)$,
(3.3c) $\displaystyle x_{w^{\prime},b^{\prime}}$ $\displaystyle\ \mapsto\ 0$
(for $c^{\prime}\neq b^{\prime}$), (3.3d)

since $w$ always gets colour $c$ and $w^{\prime}$ always gets colour
$c^{\prime}$ in any colouring $\chi_{(b,b^{\prime})}$.

######  Example 3.6.

Let us give a concrete example to make clearer how the substitution in (3.2)
works. Suppose $k=3$ and consider an arbitrary (non-pigeon) vertex $v$ in some
gadget $G_{({i},{i^{\prime}})\not\leftarrow({3},{1})}$. For every pair of
colours $(b,b^{\prime})\in([3]\times[3])\setminus\\{(3,1)\\}$ for
$(i,i^{\prime})$ we have fixed some (legal) colouring of the whole gadget.
Suppose that in these fixed colourings it holds for some vertex $v$ in the
gadget that

  1. 1.

$v$ takes colour $1$ for $(b,b^{\prime})\in\\{(1,2),(2,2),(3,2),(3,3)\\}$,

  2. 2.

$v$ takes colour $2$ for $(b,b^{\prime})\in\\{(1,1)\\}$ and

  3. 3.

$v$ takes colour $3$ for $(b,b^{\prime})\in\\{(1,3),(2,1),(2,3)\\}$.

In this case, the substitutions for the variables $x_{v,j}$ mentioning $v$
become

$\displaystyle x_{v,1}$ $\displaystyle\ \mapsto\
x_{i,1}x_{i^{\prime},2}+x_{i,2}x_{i^{\prime},2}+x_{i,3}x_{i^{\prime},2}+x_{i,3}x_{i^{\prime},3}\enspace,$
(3.4a) $\displaystyle x_{v,2}$ $\displaystyle\ \mapsto\
x_{i,1}x_{i^{\prime},1}\enspace,$ (3.4b) $\displaystyle x_{v,3}$
$\displaystyle\ \mapsto\
x_{i,1}x_{i^{\prime},3}+x_{i,2}x_{i^{\prime},1}+x_{i,2}x_{i^{\prime},3}\enspace.$
(3.4c)

We hope that the substitutions in this example can serve as a guide for
following the rest of the proof.

Let us next discuss how the polynomials obtained from (2.2a)–(2.2c) after the
substitution (3.2) can be derived in PC from (3.1a)–(3.1c). More precisely we
argue that all substituted axioms can be derived from the equations

$\displaystyle\sum^{k}_{b=1}x_{i,b}$ $\displaystyle=1\enspace,$ (3.5a)
$\displaystyle x_{i,b}x_{i,b^{\prime}}$ $\displaystyle=0$ (for $b\neq
b^{\prime}$), (3.5b)
$\displaystyle\sum^{k}_{b^{\prime}=1}x_{i^{\prime},b^{\prime}}$
$\displaystyle=1\enspace,$ (3.5c) $\displaystyle
x_{i^{\prime},b}x_{i^{\prime},b^{\prime}}$ $\displaystyle=0$ (for $b\neq
b^{\prime}$), (3.5d) $\displaystyle x_{i,c}x_{i^{\prime},c^{\prime}}$
$\displaystyle=0\enspace,$ (3.5e)

which are just the same, except for variables renaming, as the pigeon axioms
(3.1a) and (3.1b) for pigeons $i$ and $i^{\prime}$ plus the collision axiom
(3.1c) for the hole which is the common neighbour of $i$ and $i^{\prime}$. In
what follows we will need the equation

$\sum^{k}_{b=1}\sum^{k}_{b^{\prime}=1}x_{i,b}x_{i^{\prime},b^{\prime}}-x_{i,c}x_{i^{\prime},c^{\prime}}-1=0$
(3.6)

which has the degree-$2$ proof

$\sum^{k}_{b=1}x_{i,b}\left(\sum^{k}_{b^{\prime}=1}x_{i^{\prime},b^{\prime}}-1\right)+\left(\sum^{k}_{b=1}x_{i,b}-1\right)-x_{i,c}x_{i^{\prime},c^{\prime}}=0$
(3.7)

from (3.5a)–(3.5e).

We consider first axioms $\sum^{k}_{j=1}x_{v,j}=1$ as in (2.2a) for vertices
$v$ that are not a pigeon vertex $i$ or $i^{\prime}$. It is straightforward to
verify that such an axiom after substitution as in (3.2) becomes an equality
on the form (3.6).333Consider the example of substitution we saw in Example
3.6. The equation $x_{v,1}+x_{v,2}+x_{v,3}=1$ after substitution becomes
$\left(x_{i,1}x_{i^{\prime},2}+x_{i,2}x_{i^{\prime},2}+x_{i,3}x_{i^{\prime},2}+x_{i,3}x_{i^{\prime},3}\right)+\left(x_{i,1}x_{i^{\prime},1}\right)+\left(x_{i,1}x_{i^{\prime},3}+x_{i,2}x_{i^{\prime},1}+x_{i,2}x_{i^{\prime},3}\right)=1$
(3.8) which is equivalent to
$\left(x_{i,1}+x_{i,2}+x_{i,3}\right)\left(x_{i^{\prime},1}+x_{i^{\prime},2}+x_{i^{\prime},3}\right)-x_{i,3}x_{i^{\prime},1}=1\enspace.$
(3.9) If $v$ is a pigeon vertex $i$ or $i^{\prime}$, then no substitution is
made and we simply keep the axiom (3.5a) or (3.5c), respectively.

Next, we consider axioms (2.2b) on the form $x_{v,j}x_{v,j^{\prime}}=0$, where
we assume that $v$ is not a pigeon vertex $i$ or $i^{\prime}$ since in that
case we have one of the axioms (3.5b) and (3.5d). After substitution an axiom
(2.2b) for $v\notin\\{i,i^{\prime}\\}$ becomes a sum of degree-$4$ terms of
the form
$x_{i,b_{1}}x_{i^{\prime},b^{\prime}_{1}}x_{i,b_{2}}x_{i^{\prime},b^{\prime}_{2}}$.
Recall that the substitution associates disjoint sets of pairs
$(b,b^{\prime})$ to the colours for $v$ (see again Example 3.6). Therefore,
for each term
$x_{i,b_{1}}x_{i^{\prime},b^{\prime}_{1}}x_{i,b_{2}}x_{i^{\prime},b^{\prime}_{2}}$
it must be that either $b_{1}\neq b_{2}$ or $b^{\prime}_{1}\neq
b^{\prime}_{2}$ holds, and such a term can be derived from (3.5b) or (3.5d) by
multiplication.

Let us finally consider axioms on the form $x_{u,j}x_{v,j}=0$ for $(u,v)\in
E(G)$ as in (2.2c). There is no edge between $i$ and $i^{\prime}$ in our
constructed graph, so for the size of the intersection between $\\{u,v\\}$ and
$\\{i,i^{\prime}\\}$ it holds that
$0\leq\bigl{\lvert}\\{u,v\\}\cap\\{i,i^{\prime}\\}\bigr{\rvert}\leq 1$.

If $\bigl{\lvert}\\{u,v\\}\cap\\{i,i^{\prime}\\}\bigr{\rvert}=0$, then after
substitution the axiom (2.2c) becomes a sum of degree-$4$ terms of the form
$x_{i,b_{1}}x_{i^{\prime},b^{\prime}_{1}}x_{i,b_{2}}x_{i^{\prime},b^{\prime}_{2}}$.
Consider any such term. If either $b_{1}\neq b_{2}$ or $b^{\prime}_{1}\neq
b^{\prime}_{2}$, then the term can be derived from (3.5b) or (3.5d). We claim
that no term can have $b_{1}=b_{2}$ and $b^{\prime}_{1}=b^{\prime}_{2}$. To
see this, note that this would imply that when performing substitution as in
(3.2) the variables $x_{u,j}$ and $x_{v,j}$ both get expanded to a sum
containing $x_{i,b_{1}}x_{i^{\prime},b^{\prime}_{1}}$. But this would in turn
mean that the colouring $\chi_{(b_{1},b_{1}^{\prime})}$ that we fixed for the
gadget $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ at the start
of the proof assigned colours
$\chi_{(b_{1},b_{1}^{\prime})}(u)=\chi_{(b_{1},b_{1}^{\prime})}(v)$, which is
impossible since there is an edge between $u$ and $v$ and
$\chi_{(b_{1},b_{1}^{\prime})}$ was chosen to be a legal colouring.

The remaining case is when we have intersection size
$\bigl{\lvert}\\{u,v\\}\cap\\{i,i^{\prime}\\}\bigr{\rvert}=1$. Without loss of
generality because of symmetry we can assume that we have an axiom
$x_{u,j}x_{v,j}=0$ for $u\notin\\{i,i^{\prime}\\}$ and $v=i$. The axiom
becomes after substitution a sum of terms of the form
$x_{i,b}x_{i^{\prime},b^{\prime}}x_{i,j}$. If for some term we would have
$b=j$, then $\chi_{(j,b^{\prime})}$ would assign the same colour $j$ to both
$u$ and $i$. This is again impossible since $\chi_{(j,b^{\prime})}$ is a legal
colouring of the gadget by construction. Hence we have $b\neq j$ and it
follows that $x_{i,b}x_{i^{\prime},b^{\prime}}x_{i,j}$ is derivable from
(3.5b).

We are now almost done with the proof of Lemma 3.5. We have defined how to
substitute variables $x_{v,j}$ in (2.2a)–(2.2c) and have shown that the
equations that we obtain after these substitutions can be derived from
Equations (3.1a)–(3.1c) in low degree. The final issue that remains it to get
rid of all vertices $\gamma_{t}$ in the pre-colouring gadget in Figure 2 that
are not members of any injectivity constraint gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$. For such variables
the substitution is simply an assignment: we let $x_{\gamma_{t},b}\mapsto 1$
when $t\equiv b\pmod{k}$ and $x_{\gamma_{t},b}\mapsto 0$ otherwise.444Note
that here the substitution for $x_{\gamma_{t},b}$ where $t\equiv b\pmod{k}$ is
different from the one used for vertices that are members of some gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ in (3.3a) and (3.3b).
For variables $x_{\gamma_{t},b}$ where $t\not\equiv b\pmod{k}$ the
substitution is the same as in (3.3c) and (3.3d), though. This immediately
satisfies all axioms (2.2a) and (2.2b) for these vertices, removing these
axioms from the refutation. It remains to check the axioms (2.2c) for any pair
of connected vertices $\gamma_{t}$ and $\gamma_{t^{\prime}}$. But by
construction, if $\gamma_{t}$ and $\gamma_{t^{\prime}}$ are connected it holds
that $t\not\equiv t^{\prime}\pmod{k}$. Therefore, for every $b\in[k]$ we have
that either $x_{\gamma_{t},b}\mapsto 0$ or $x_{\gamma_{t^{\prime}},b}\mapsto
0$ holds, regardless of whether these two vertices are in some gadget
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ or not.

To summarize what we have done, we started with any arbitrary refutation of
(2.2a)–(2.2c) and substituted all variables with degree-$2$ polynomials over
the variables $x_{i,j}$ for $i\in[n]$. Then we proved that all these
substituted axioms (and therefore the whole refutation) follow from Equations
(3.5a)–(3.5c). It is straightforward to verify that, up to variable renaming,
these axioms are nothing other than the FPHP axioms in (3.1a)–(3.1c). This
concludes the proof of Lemma 3.5. Putting everything together, we can now
state and prove our main theorem.

######  Theorem 3.7.

For any integer $k\geq 3$ there is an efficiently constructible family of
graphs $\\{G_{n}\\}_{n\in\mathbb{N}}$ with $\mathrm{O}(k^{4}n)$ vertices of
degree $\mathrm{O}(k^{2})$ that do not possess $k$-colourings, but for which
the corresponding system of polynomial equations (2.2a)–(2.2c) require degree
$\Omega(n)$, and hence size $\exp(\Omega(n))$, to be refuted in polynomial
calculus.

###### Proof.

We need to build a family of bipartite graphs $\\{B_{n}\\}_{n\in\mathbb{N}}$
with the properties needed to apply Theorem 3.1 and Proposition 3.4. This
would yield a family of graphs $\\{G_{n}\\}_{n\in\mathbb{N}}$ as in the
theorem statement. Indeed any sublinear degree refutation for $k$-colouring of
$G_{n}$ would imply, by Lemma 3.5, a sublinear degree refutation for the
functional pigeonhole principle for $B_{n}$, but this is impossible by a
construction of $B_{n}$ that triggers the lower bound in Theorem 3.1.

For every $k\geq 3$ the starting point of our construction is the paper by
Alon and Capalbo [AC02], which provide universal constants $\alpha,\delta$ and
simple graphs $\\{H_{n}\\}_{n\in\mathbb{N}}$ of degree at most $k$ so that
$H_{n}$ has $n$ vertices and for every set $X$ of vertices in $H_{n}$, the
boundary of $X$ in $V(H_{n})\setminus X$ has size at least $\delta|X|$.
Consider the bipartite graph obtained taking two copies of the vertices of
$H_{n}$, one identified with the left side and one with the right side, and
adding an edge from the left copy of $u$ to the right copy of $v$ for every
edge $\\{u,v\\}\in E(H_{n})$. Then take an arbitrary vertex $\hat{u}\in
V(H_{n})$ and remove the corresponding right copy from the graph. The
resulting graph, that we define to be $B_{n}$, has $n$ vertices on the left
side, $n-1$ vertices on the right side and degree at most $k$ on both sides.
Moreover for every set $I$ of left vertices of size at most $\alpha n$ the
boundary of $I$ consists in the right copies of the corresponding boundary in
$H_{n}$, minus vertex $\hat{u}$. Therefore $B_{n}$ satisfies the properties
needed to apply Theorem 3.1. ∎

##  4 Polynomial-Length Proofs for $k$-Colouring Instances in Cutting Planes

Theorem 3.7 tells us that there are non-$k$-colourable graphs $G_{n}$ for
which it is impossible for polynomial calculus to certify
non-$k$-colourability efficiently. As is clear from our reduction, the
$k$-colouring formulas for these graphs are essentially obfuscated instances
of the functional pigeonhole principle.

It is well-known that cutting planes can easily prove that pigeonhole
principle formulas are unsatisfiable by just counting the number of pigeons
and holes and deduce that the pigeons are too many to fit in the holes
[CCT87]. As we show in this section, the instances of $k$-colouring obtained
via the reduction from FPHP also have short cutting planes refutations. What
these refutations do is essentially to “de-obfuscate” the $k$-colouring
formulas to recover the original functional pigeonhole principle instances,
which can then be efficiently refuted.

We are going to describe our cutting planes refutation as a decision tree such
that at every leaf we have a cutting planes refutation of the formula
restricted by the partial assignment defined by the tree branch reaching that
leaf. These refutations of the restricted versions of the formula can then be
combined to yield a refutation of the original, unrestricted formula as stated
in Lemma 4.1 and Proposition 4.2. The proofs of these statements are fairly
routine, but we include them below for completeness.

We recall that as discussed in Section 2 we will use
$\sum_{i}a_{i}x_{i}\leq\gamma$ as an alias for
$\sum_{i}-a_{i}x_{i}\geq-\gamma$ and $\sum_{i}a_{i}x_{i}=\gamma$ as an alias
for the combination of $\sum_{i}a_{i}x_{i}\leq\gamma$ and
$\sum_{i}a_{i}x_{i}\geq\gamma$. In particular, we will frequently write $x=b$
for some variable $x$ and $b\in\\{0,1\\}$ as a shorthand for the pair of
inequalities $x\leq b$ and $-x\leq-b$.

######  Lemma 4.1.

Let $b\in\\{0,1\\}$ and suppose that there exists a cutting planes derivation
$(B_{1},\ldots,B_{L})$ in length $L$ of the inequality
$\sum_{i}a_{i}x_{i}\leq\gamma$ from the system of inequalities
$\mathcal{S}\cup\\{x=b\\}$. Then for some $K\in\mathbb{N}$ there is a CP
derivation in length $\mathrm{O}(L)$ of the inequality

$(-1)^{1-b}K\cdot(x-b)+\sum_{i}a_{i}x_{i}\leq\gamma$ (4.1)

from $\mathcal{S}$.

###### Proof.

We only consider the case of $b=1$, since the case of $b=0$ is essentially the
same. Observe that $x\leq 1$ is a boolean axiom, and so the only axiom lost
when passing from $\mathcal{S}\cup\\{x=b\\}$ to $\mathcal{S}$ is $-x\leq-1$.
The proof is by forward induction over the derivation. We use the notation
$B_{t}=\sum_{i}a_{i}^{(t)}x_{i}\leq\gamma^{(t)}$ for the linear inequalities
$B_{t}$, $t\in[L]$, in the original derivation. We show how to derive the
inequalities

$K^{(t)}\cdot(x-1)+\sum_{i}a_{i}^{(t)}x_{i}\leq\gamma^{(t)}$ (4.2)

for $t\in[L]$ with a constant number of rule applications per step, assuming
that the preceding inequalities have already been derived. We proceed by cases
depending on which rule was used to derive $B_{t}$ in the original derivation.

If $B_{t}$ is the axiom $-x\leq-1$ we can substitute it with axiom $0\leq 0$,
which can be written as $(x-1)-x\leq-1$. Notice that, technically speaking,
$0\leq 0$ is not an axiom of the cutting planes proof system, but it is
convenient to allows such lines in our derivation and remove them in a final
postprocessing step. If $B_{t}$ is a variable axiom $x\geq 0$ or an initial
axiom $A_{j}\in\mathcal{S}$, then it is already on the form (4.2) with
$K^{(t)}=0$.

If $B_{t}$ is derived as a sum $B_{t}=B_{t_{1}}+B_{t_{2}}$ for some $1\leq
t_{1}<t_{2}<t$, then by the induction hypothesis we have already derived

$K^{(t_{1})}(x-1)+\sum_{i}a_{i}^{(t_{1})}x_{i}\leq\gamma^{(t_{1})}$ (4.3)

and

$K^{(t_{2})}(x-1)+\sum_{i}a_{i}^{(t_{2})}x_{i}\leq\gamma^{(t_{2})}$ (4.4)

and the sum of these two inequalities is already on the form (4.2) with
$K^{(t)}=K^{(t_{1})}+K^{(t_{2})}$.

If $B_{t}$ is derived by multiplication $B_{t}=\alpha B_{t^{\prime}}$ for some
$1\leq t^{\prime}<t$, then then by the induction hypothesis we have already
derived

$K^{(t^{\prime})}(x-1)+\sum_{i}a_{i}^{(t^{\prime})}x_{i}\leq\gamma^{(t^{\prime})}\enspace,$
(4.5)

and so $B_{t}=\alpha B_{t^{\prime}}$ is on the form (4.2) with $K^{(t)}=\alpha
K^{(t^{\prime})}$.

If $B_{t}$ is obtained by the application of the division rule to some
previously derived inequality $B_{t^{\prime}}$, then $B_{t}$ has the form

$\sum_{i}\frac{a_{i}^{(t^{\prime})}}{c}x_{i}\leq\left\lfloor\frac{\gamma^{(t^{\prime})}}{c}\right\rfloor\enspace.$
(4.6)

By the induction hypothesis we have already derived

$K^{(t^{\prime})}(x-1)+\sum_{i}a_{i}^{(t^{\prime})}x_{i}\leq\gamma^{(t^{\prime})}$
(4.7)

and we want to divide this inequality by $c$. In order to do so, however, we
need to ensure that all coefficients in (4.7) are divisible by $c$. Since by
assumption the application of the division rule in (4.6) was legal we have
that $c$ divides all of $a_{1},\ldots,a_{n}$. Choose the smallest $K^{\prime}$
divisible by $c$ such that $K^{\prime}-K^{t^{\prime}}\geq 0$, multiply $x\leq
1$, which we can also write as $x-1\leq 0$, by $K^{\prime}-K^{t^{\prime}}$ and
then add to (4.7) to obtain

$K^{\prime}(x-1)+\sum_{i}a_{i}^{(t^{\prime})}x_{i}\leq\gamma^{(t^{\prime})}\enspace.$
(4.8)

In order to apply division we have to collect all constant terms on the right-
hand side, meaning that we rewrite (4.8) as

$K^{\prime}x+\sum_{i}a_{i}^{(t^{\prime})}x_{i}\leq\gamma^{(t^{\prime})}+K^{\prime}\enspace,$
(4.9)

and division now yields

$\frac{K^{\prime}}{c}x+\sum_{i}\frac{a_{i}^{(t^{\prime})}}{c}x_{i}\leq\left\lfloor\frac{\gamma^{(t^{\prime})}+K^{\prime}}{c}\right\rfloor$
(4.10)

which we can write as

$\frac{K^{\prime}}{c}(x-1)+\sum_{i}\frac{a_{i}^{(t^{\prime})}}{c}x_{i}\leq\left\lfloor\frac{\gamma^{(t^{\prime})}+K^{\prime}}{c}\right\rfloor=\left\lfloor\frac{\gamma^{(t^{\prime})}}{c}\right\rfloor$
(4.11)

since $c$ divides $K^{\prime}$. The inequality (4.11) is on the form (4.2),
and so we are done with our analysis of the division step.

By the induction principle we obtain a derivation in lenght $\mathrm{O}(L)$ of
(4.1), as claimed. As the last step we remove all occurrences of lines $0\leq
0$. It is clear that any addition of such an inequality to another inequality
can simply be ignored. ∎

We next show how Lemma 4.1 can be used to piece together refutations of
restricted versions of a $k$-colouring formula to one refutation of the
unrestricted formula.

######  Proposition 4.2.

Let $G$ be a graph and $k\geq 2$ be a positive integer, and let $\mathcal{S}$
be the set of inequalities (2.13a)–(2.13c) for $G$ and $k$. If for a fixed set
of vertices $u_{1},u_{2},\ldots,u_{\ell}$ in $G$ and every choice of colours
$(c_{1},c_{2},\ldots,c_{\ell})\in[k]^{\ell}$ for these vertices there is a CP
refutation in length at most $L$ of the set of inequalities
$\mathcal{S}\cup\\{x_{u_{1},c_{1}}=1,x_{u_{2},c_{2}}=1,\ldots,x_{u_{\ell},c_{\ell}}=1\\}$,
then there is a CP refutation of $\mathcal{S}$ in length
$k^{\mathrm{O}(\ell)}\cdot L$.

###### Proof.

We prove the claim by induction on $\ell$. If $\ell=0$ then the statement is
vacuous. For $\ell>0$ we assume that we can derive $1\leq 0$ in length at most
$L$ from
$\mathcal{S}\cup\\{x_{u_{1},c_{1}}=1,x_{u_{2},c_{2}}=1,\ldots,x_{u_{\ell},c_{\ell}}=1,x_{u,c}=1\\}$
for a fixed vertex $u$ and every $c\in[k]$.

For each $c\in[k]$ we use Lemma 4.1 to construct a CP derivation of the
inequality $K_{c}(x_{u,c}-1)+1\leq 0$ from
$\mathcal{S}\cup\\{x_{u_{1},c_{1}}=1,x_{u_{2},c_{2}}=1,\ldots,x_{u_{\ell},c_{\ell}}=1\\}$
in length $\kappa L$, where $\kappa$ is a universal constant. By dividing each
such inequality by $K_{c}$ we get $x_{u,c}\leq 0$ for all $c\in[k]$. By
summing all these inequalities with the initial axiom $\sum_{c}x_{u,c}\geq 1$
we obtain $0\geq 1$. The total length of this refutation is $k\kappa L+2k$.
The proposition follows by the induction principle. ∎

We can now state the main result of this section, namely that the hard
$k$-colouring instances for polynomial calculus constructed in Section 3 are
easy for cutting planes.

######  Proposition 4.3.

Let $B$ be a left-regular bipartite graph $B$ with left degree $k$ and bounded
right degree $\mathrm{O}(k)$, and consider the graph $G=G(B)$ in Proposition
3.4. Then if there is no complete matching of the left-hand side of $B$ into
the right-hand side, then the set of inequalities (2.13a)–(2.13c) encoding the
$k$-colouring problem on $G$ has a cutting planes refutation in length
${k}^{\mathrm{O}(k)}\cdot\lvert V(B)\rvert^{\mathrm{O}(1)}$.

###### Proof sketch.

Consider the first $k$ vertices $\gamma_{1},\ldots,\gamma_{k}$ in the pre-
colouring gadget in $G$ as depicted in Figure 2, which form a $k$-clique. For
every partial colouring $(c_{1},c_{2},\ldots,c_{k})\in[k]^{k}$ of this
$k$-clique we build a cutting planes refutation of

$\mathcal{S}\cup\\{x_{\gamma_{1},c_{1}}=1,x_{\gamma_{2},c_{2}}=1,\ldots,x_{\gamma_{k},c_{k}}=1\\}\enspace.$
(4.12)

The result then follows by combining all of these refutations using
Proposition 4.2.

Fix a choice of colours $(c_{1},c_{2},\ldots,c_{k})\in[k]^{k}$. Notice that if
some colour occurs twice in this tuple, then we can derive contradiction in
length $\mathrm{O}(1)$ from (4.12) since one of the edge axioms (2.13c) is
violated. Suppose therefore that $(c_{1},c_{2},\ldots,c_{k})$ is a permutation
of $[k]$. We will construct a CP refutation of (4.12) in length
${k}^{\mathrm{O}(k)}\cdot\lvert V(B)\rvert^{\mathrm{O}(1)}$.

The system of inequalities $\mathcal{S}$ is symmetric which respect to the
permutation of the colour indices, so without loss of generality we focus on
giving a refutation for

$\mathcal{S}\cup\\{x_{\gamma_{1},1}=1,x_{\gamma_{2},2}=1,\ldots,x_{\gamma_{k},k}=1\\}\enspace.$
(4.13)

The equations
$\\{x_{\gamma_{1},1}=1,x_{\gamma_{2},2}=1,\ldots,x_{\gamma_{k},k}=1\\}$ taken
together with $\mathcal{S}$ allow us to efficiently infer
$x_{\gamma_{i},i\bmod{k}}=1$ for all the vertices $\gamma_{i}$, $i\in[M]$, in
the gadget in Figure 2 (where we recall from Section 2 that we identify
colours $0$ and $k$ when convenient). The resulting set of equalities and
inequalities $\mathcal{S}\cup\\{x_{\gamma_{i},i\bmod{k}}=1\mid i\in[M]\\}$ is
essentially an encoding of the $k$-colouring problem for the partially colored
graph $\widehat{G}$ in Lemma 3.3 consisting of the gadgets in Figure 1.
Indeed, since the partial assignment
$\\{x_{\gamma_{1},1}=1,x_{\gamma_{2},2}=1,\ldots,x_{\gamma_{k},k}=1\\}$ forces
the colours of all vertices $\gamma_{i}$, $i\in[M]$, in Figure 2, this gives
us back the pre-coloured vertices in the gadgets in Figure 1.

As argued in (the proof of) Lemma 3.3, $\widehat{G}$ is the union of at most
$\mathrm{O}\bigl{(}k^{2}\lvert V(B)\rvert\bigr{)}$ injectivity constraint
gadgets $G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ that forbid
pigeons $i$ and $i^{\prime}$ taking their $c$th and $c^{\prime}$th edges,
respectively, colliding in some hole $j$. If we introduce the alias $p_{i,j}$
for $x_{i,c}$, where $j$ is the hole to which the $c$th edge from pigeon $i$
leads, then our goal can be described as deriving the pigeonhole axiom
$p_{i,j}+p_{i^{\prime},j}=x_{i,c}+x_{i^{\prime},c^{\prime}}\leq 1$ from the
set of inequalities of the corresponding gadget
$G_{({u},{v})\not\leftarrow({c},{c^{\prime}})}$. We will see shortly how to do
so in length $\mathrm{O}\bigl{(}k^{\mathrm{O}(k)}\bigr{)}$. Once we extract
these pigeonhole inequalities we observe that the collection of these
inequalities together with the inequalities (2.13a) form a cutting plane
encoding

$\displaystyle\sum_{j\in J({i})}p_{i,j}$ $\displaystyle\geq 1$ $i\in I$,
(4.14a) $\displaystyle p_{i,j}+p_{i^{\prime},j}$ $\displaystyle\leq 0$ $i\neq
i^{\prime}\in I$, $j\in J({i})\cap J({i^{\prime}})$. (4.14b)

of the graph pigeonhole principle on the bipartite graph $B$ with left-hand
side $I$ and right-hand side $J$. Such a system of inequalities has a cutting
plane refutation in length $\mathrm{O}\bigl{(}{\lvert V(B)\rvert}^{3}\bigr{)}$
[CCT87].

In order to derive $x_{i,c}+x_{i^{\prime},c^{\prime}}\leq 1$ we consider the
inequalities involving vertices of
$G_{({i},{i^{\prime}})\not\leftarrow({c},{c^{\prime}})}$ plus the equations
$x_{i,c}=1$ and $x_{i,c^{\prime}}=1$. By Claim 3.2 this is an unsatisfiable
system of inequalities of size $\mathrm{O}(k)$. By the refutational
completeness of cutting planes, and using Lemma 4.1 twice, we obtain a
derivation of $K_{1}(x_{i,c}-1)+K_{2}(x_{i^{\prime},c^{\prime}}-1)\leq-1$ in
length $\exp(\mathrm{O}(k))$. Adding multiples of axioms on the form $x-1\leq
0$ we get the inequality $K(x_{i,c}-1)+K(x_{i^{\prime},c^{\prime}}-1)\leq-1$
for some positive integer $K$, and division by $K$ yields
$x_{i,c}+x_{i^{\prime},c^{\prime}}\leq 1$.

We have shown how to derive contradiction is length
${k}^{\mathrm{O}(k)}|V(B)|^{\mathrm{O}(1)}$ for any given colouring of the
vertices $\gamma_{1},\ldots,\gamma_{k}$. We take such refutations for all
${k^{k}}$ possible ways of assigning colours to these vertices and joint them
together using Proposition 4.2 into a refutation of the original, unrestricted
formula. The proposition follows. ∎

##  5 Concluding Remarks

In this work we exhibit explicitly constructible graphs which are
non-$k$-colourable but which require large degree in polynomial calculus to
certify this fact for the canonical encoding of the $k$-colouring problem into
polynomial equations over $\\{0,1\\}$-valued variables. This, in turn, implies
that the size of any polynomial calculus proof of non-$k$-colourability for
these graphs must be exponential measured in the number of vertices.

Our degree lower bound also applies to a slightly different encoding with
primitive $k$th roots of unity used in [DLMM08, DLMM11] to build $k$-colouring
algorithms based on Hilbert’s Nullstellensatz. These algorithms construct
certificates of non-$k$-colourability by solving linear systems of equations
over the coefficients of all monomials up to a certain degree. The current
paper yields explicit instances for which this method needs to consider
monomials up to a very large degree, and therefore has to produce a linear
system of exponential size. This answers an open question raised in, for
example, [DLMM08, DLMO09, DLMM11, LLO16].

This leads to an important observation, however. The degree lower bound
applies to both polynomial encodings discussed above, but the size lower bound
only applies to the encoding using $\\{0,1\\}$-valued variables. It is still
conceivable that proofs of non-$k$-colourability in the roots-of-unity
encoding can be small although they must have large degree. This raises the
following question.

######  Open Problem 1.

Is there a family of non-$3$-colourable graphs such that any polynomial
calculus proof of non-$3$-colourability using the roots of unity encoding must
require large size?

If the answer to the question is positive, then no matter how we choose the
monomials to consider for the linear system construction in [DLMM08, DLMM11],
the size of the system will have to be large.

To further reduce the size of the linear system, the algorithms in [DLMM08,
DLMM11] make use of the symmetries in the graphs. It is a natural question how
much such an approach could help for our non-$k$-colourable instances. It
seems plausible that if we apply our construction to a randomly generated
bipartite graph with appropriate parameters, then the final graph will not
have many symmetries except for the local symmetries inside the gadgets. In
that case our lower bound might apply for the improved version of the
algorithm as well.

The work in [AO18] addresses the proof complexity of refuting constraint
statisfaction problems (CSP) and show that standard reductions between CSPs
preserve hardness, to some extent, and in particular degree. These reductions
are able to translate between various encodings, and indeed they may not
preserve monomial size.

One limitation of our result is that our hard graphs are very specific, and
arguably somewhat artificial. For the weaker resolution proof system an
average-case exponential lower bound has been shown for Erdős–Rényi random
graphs $\mathcal{G}(n,p)$ where $p$ is slightly above the threshold value
$p_{k}(n)$ at which the graph becomes highly likely to be non-$k$-colourable
[BCMM05]. It is natural to ask whether these instances are hard for polynomial
calculus too.

######  Open Problem 2.

Consider a random graph sampled according to $\mathcal{G}(n,p)$ with
$p>p_{k}(n)$, so that the graph is non-$k$-colourable with high probability.
Does polynomial calculus require large degree to certify non-$k$-colourability
of such graphs with high probability?

Some progress on this open problem may come from the recent work of [RT22]
where they show degree lower bound in Nullstellensatz for large classes of
graphs, relying just on the girth size.

In this paper, we also show that the graph colouring instances that are
provably hard for polynomial calculus are very easy for the cutting planes
proof system. It does not seem very likely that graph colouring would be an
easy problem for cutting planes, however, and so it would be interesting to
find explicit candidates for hard instances for cutting planes, even if
proving the actual lower bounds may be very hard. This question is also
interesting for the Lasserre/Sums-of-Squares proof system. Our instances seem
likely to be easy for Lasserre, since they are based on the hardness of the
pigeonhole principle and this combinatorial principle is easy for Lasserre.

######  Open Problem 3.

Find candidates for explicit hard instances of non-$3$-colourability for
cutting planes and for Lasserre/Sums-of-squares proof systems, and then prove
formally that these instances are indeed hard.

A final, intriguing, observation, which is somewhat orthogonal to the rest of
this discussion, is that even though the graph colouring instances in our
paper are easy for cutting planes, results from the _Pseudo-Boolean
Competition 2016_ indicate that they are quite hard in practice for state-of-
the-art pseudo-Boolean solvers [PB16]. This is even more interesting
considering that the cutting planes refutations that we construct have small
rank (i.e., the maximum number of application of the division rules along any
path in the proof graph is small).

## Acknowledgements

We are grateful to Mladen Mikša and Alexander Razborov for stimulating
discussions and helpful feedback during various stages of this project. We
would also like to thank Jan Elffers for running experiments with pseudo-
Boolean solvers on instances obtained from our reduction from functional
pigeonhole principle formulas to graph colouring, demonstrating that these
formulas are hard in practice. Last but not least, a big thanks to the
anonymous CCC reviewers, who helped us catch some typos and bugs that really
should not have been there, and whose suggestions helped improve the
exposition considerably.

Part of this research was done while the first author was at KTH Royal
Institute of Technology funded by the European Research Council (ERC) under
the European Union’s Seventh Framework Programme (FP7/2007–2013) / ERC grant
agreement no. 279611. Later work at Universitat Politècnica de Catalunya for
this project has received funding from the European Research Council (ERC)
under the European Union’s Horizon 2020 research and innovation programme
(grant agreement ERC-2014-CoG 648276 AUTAR). The second author was supported
by the European Research Council under the European Union’s Seventh Framework
Programme (FP7/2007–2013) / ERC grant agreement no. 279611, by the Swedish
Research Council grants 621-2012-5645 and 2016-00782, and by the Independent
Research Fund Denmark grant 9040-00389B.

## References

  * [ABRW02] Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson.  Space complexity in propositional calculus.  SIAM Journal on Computing, 31(4):1184–1211, 2002.  Preliminary version in _STOC ’00_.
  * [AC02] Noga Alon and Michael Capalbo.  Explicit unique-neighbor expanders.  In Proceedings of the 43th Annual IEEE Symposium on Foundations of Computer Science (FOCS ’02), pages 73–79. IEEE, 2002.
  * [AO18] Albert Atserias and Joanna Ochremiak.  Proof complexity meets algebra.  ACM Transactions on Computational Logic, 20(1):1–46, Dec 2018.
  * [AR03] Michael Alekhnovich and Alexander A. Razborov.  Lower bounds for polynomial calculus: Non-binomial case.  Proceedings of the Steklov Institute of Mathematics, 242:18–35, 2003.  Available at http://people.cs.uchicago.edu/~razborov/files/misha.pdf. Preliminary version in _FOCS ’01_.
  * [AT92] Noga Alon and Michael Tarsi.  Colorings and orientations of graphs.  Combinatorica, 12(2):125–134, June 1992.
  * [Bay82] David Allen Bayer.  The Division Algorithm and the Hilbert Scheme.  PhD thesis, Harvard University, Cambridge, MA, USA, June 1982.  Available at https://www.math.columbia.edu/~bayer/papers/Bayer-thesis.pdf.
  * [BC96] Samuel R. Buss and Peter Clote.  Cutting planes, connectivity and threshold logic.  Archive for Mathematical Logic, 35:33–63, 1996.
  * [BCMM05] Paul Beame, Joseph C. Culberson, David G. Mitchell, and Cristopher Moore.  The resolution complexity of random graph $k$-colorability.  Discrete Applied Mathematics, 153(1-3):25–47, December 2005.
  * [BE05] Richard Beigel and David Eppstein.  $3$-coloring in time ${O}(n^{1.3289})$.  Journal of Algorithms, 54(2):168–204, February 2005\.
  * [BGIP01] Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi.  Linear gaps between degrees for the polynomial calculus modulo distinct primes.  Journal of Computer and System Sciences, 62(2):267–289, March 2001.  Preliminary version in _CCC ’99_.
  * [BI10] Eli Ben-Sasson and Russell Impagliazzo.  Random CNF’s are hard for the polynomial calculus.  Computational Complexity, 19:501–519, 2010.  Preliminary version in _FOCS ’99_.
  * [BIK+94] Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák.  Lower bounds on Hilbert’s Nullstellensatz and propositional proofs.  In Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science (FOCS ’94), pages 794–806, November 1994.
  * [Bla37] Archie Blake.  Canonical Expressions in Boolean Algebra.  PhD thesis, University of Chicago, 1937.
  * [BS97] Roberto J. Bayardo Jr. and Robert Schrag.  Using CSP look-back techniques to solve real-world SAT instances.  In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI ’97), pages 203–208, July 1997.
  * [BW01] Eli Ben-Sasson and Avi Wigderson.  Short proofs are narrow—resolution made simple.  Journal of the ACM, 48(2):149–169, March 2001.  Preliminary version in _STOC ’99_.
  * [CCT87] William Cook, Collette Rene Coullard, and György Turán.  On the complexity of cutting-plane proofs.  Discrete Applied Mathematics, 18(1):25–38, November 1987.
  * [CEI96] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo.  Using the Groebner basis algorithm to find proofs of unsatisfiability.  In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC ’96), pages 174–183, May 1996.
  * [Chv73] Vašek Chvátal.  Edmond polytopes and a hierarchy of combinatorial problems.  Discrete Mathematics, 4(1):305–337, 1973.
  * [De 95] Jesús A. De Loera.  Gröbner bases and graph colorings.  Beiträge zur Algebra und Geometrie, 36(1):89–96, January 1995.  Available at https://www.emis.de/journals/BAG/vol.36/no.1/.
  * [DLMM08] Jesús A. De Loera, Jon Lee, Peter N. Malkin, and Susan Margulies.  Hilbert’s Nullstellensatz and an algorithm for proving combinatorial infeasibility.  In Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation (ISSAC ’08), pages 197–206, July 2008\.
  * [DLMM11] Jesús A. De Loera, Jon Lee, Peter N. Malkin, and Susan Margulies.  Computing infeasibility certificates for combinatorial problems through Hilbert’s Nullstellensatz.  Journal of Symbolic Computation, 46(11):1260–1283, November 2011.
  * [DLMO09] Jesús A. De Loera, Jon Lee, Susan Margulies, and Shmuel Onn.  Expressing combinatorial problems by systems of polynomial equations and Hilbert’s Nullstellensatz.  Combinatorics, Probability and Computing, 18:551–582, July 2009.
  * [DMP+15] Jesús A. De Loera, Susan Margulies, Michael Pernpeintner, Eric Riedl, David Rolnick, Gwen Spencer, Despina Stasi, and Jon Swenson.  Graph-coloring ideals: Nullstellensatz certificates, Gröbner bases for chordal graphs, and hardness of Gröbner bases.  In Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation (ISSAC ’15), pages 133–140, July 2015\.
  * [GL10a] Nicola Galesi and Massimo Lauria.  On the automatizability of polynomial calculus.  Theory of Computing Systems, 47:491–506, August 2010\.
  * [GL10b] Nicola Galesi and Massimo Lauria.  Optimality of size-degree trade-offs for polynomial calculus.  ACM Transactions on Computational Logic, 12:4:1–4:22, November 2010.
  * [Gom63] Ralph E. Gomory.  An algorithm for integer solutions of linear programs.  In R.L. Graves and P. Wolfe, editors, Recent Advances in Mathematical Programming, pages 269–302. McGraw-Hill, New York, 1963\.
  * [Hus15] Thore Husfeldt.  Graph colouring algorithms.  In Lowell W. Beineke and Robin J. Wilson, editors, Topics in Chromatic Graph Theory, Encyclopedia of Mathematics and its Applications, chapter 13, pages 277–303. Cambridge University Press, May 2015.
  * [HW08] Christopher J. Hillar and Troels Windfeldt.  Algebraic characterization of uniquely vertex colorable graphs.  Journal of Combinatorial Theory, Series B, 98(2):400–414, March 2008.
  * [IPS99] Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall.  Lower bounds for the polynomial calculus and the Gröbner basis algorithm.  Computational Complexity, 8(2):127–144, 1999.
  * [Lan05] Serge Lang.  Algebra.  Springer New York, 2005.
  * [LLO16] Bo Li, Benjamin Lowenstein, and Mohamed Omar.  Low degree Nullstellensatz certificates for $3$-colorability.  The Electronic Journal of Combinatorics, 23(1), January 2016.
  * [Lov94] László Lovász.  Stable sets and polynomials.  Discrete Mathematics, 124(1–3):137–153, January 1994.
  * [LP10] Daniel Le Berre and Anne Parrain.  The Sat4j library, release 2.2.  Journal on Satisfiability, Boolean Modeling and Computation, 7:59–64, 2010.
  * [Mat74] Yuri V. Matiyasevich.  A criterion for vertex colorability of a graph stated in terms of edge orientations.  Diskretnyi Analiz, 26:65–71, 1974.  English translation of the Russian original. Available at http://logic.pdmi.ras.ru/~yumat/papers/22_paper/.
  * [Mat04] Yuri V. Matiyasevich.  Some algebraic methods for calculating the number of colorings of a graph.  Journal of Mathematical Sciences, 121(3):2401–2408, May 2004.
  * [McD84] Colin McDiarmid.  Colouring random graphs.  Annals of Operations Research, 1(3):183–200, October 1984.
  * [MMZ+01] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.  Chaff: Engineering an efficient SAT solver.  In Proceedings of the 38th Design Automation Conference (DAC ’01), pages 530–535, June 2001.
  * [MN15] Mladen Mikša and Jakob Nordström.  A generalized method for proving polynomial calculus degree lower bounds.  In Proceedings of the 30th Annual Computational Complexity Conference (CCC ’15), volume 33 of Leibniz International Proceedings in Informatics (LIPIcs), pages 467–487, June 2015.
  * [Mnu01] Michal Mnuk.  Representing graph properties by polynomial ideals.  In Proceedings of the 4th International Workshop on Computer Algebra in Scientific Computing (CASC ’01), pages 431–444, September 2001.
  * [MS99] João P. Marques-Silva and Karem A. Sakallah.  GRASP: A search algorithm for propositional satisfiability.  IEEE Transactions on Computers, 48(5):506–521, May 1999\.  Preliminary version in _ICCAD ’96_.
  * [PB16] Pseudo-Boolean competition 2016: Results by benchmark for category no optimisation, small integers, linear constraints (DEC-SMALLINT-LIN).  http://www.cril.univ-artois.fr/PB16/results/globalbybench.php?idev=81&idcat=47, 2016\.
  * [RT22] Julian Romero and Levent Tunçel.  Graphs with large girth and chromatic number are hard for nullstellensatz.  CoRR, abs/2212.05365, 2022.
  * [S4j] Sat4j: The Boolean satisfaction and optimization library in Java.  http://www.sat4j.org/.