Authors Mika G{\"o}{\"o}s, Jukka Suomela,
License CC-BY-3.0
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33
www.theoryofcomputing.org
Locally Checkable Proofs
in Distributed Computing
Mika Göös Jukka Suomela
Received August 20, 2012; Revised November 3, 2016; Published November 29, 2016
Abstract: We study decision problems related to graph properties from the perspective of
nondeterministic distributed algorithms. For a yes-instance there must exist a proof that can
be verified with a distributed algorithm: all nodes must accept a valid proof, and at least one
node must reject an invalid proof. We focus on locally checkable proofs that can be verified
with a constant-time distributed algorithm. For example, it is easy to prove that a graph is
bipartite: the locally checkable proof gives a 2-coloring of the graph, which only takes 1 bit
per node. However, it is more difficult to prove that a graph is not bipartite—it turns out that
any locally checkable proof requires Ω(log n) bits per node.
In this paper we classify graph properties according to their local proof complexity, i. e.,
how many bits per node are needed in a locally checkable proof. We establish tight or near-
tight results for classical graph properties such as the chromatic number. We show that the
local proof complexities form a natural hierarchy of complexity classes: for many classical
graph properties, the local proof complexity is either 0, Θ(1), Θ(log n), or poly(n) bits per
node. Among the most difficult graph properties are proving that a graph is symmetric (has
a non-trivial automorphism), which requires Ω(n2 ) bits per node, and proving that a graph
is not 3-colorable, which requires Ω(n2 / log n) bits per node. Any property of connected
graphs admits a trivial proof with O(n2 ) bits per node.
ACM Classification: C.2.4, F.1.3
AMS Classification: 68M14, 68Q15, 68Q25, 68Q85, 03F20
Key words and phrases: nondeterminism, distributed computing, locality, graphs
A preliminary version of this paper appeared in the Proceedings of the 30th ACM Symposium on Principles of Distributed
Computing (PODC 2011) [13].
© 2016 Mika Göös and Jukka Suomela
c b Licensed under a Creative Commons Attribution License (CC-BY) DOI: 10.4086/toc.2016.v012a019
M IKA G Ö ÖS AND J UKKA S UOMELA
1 Introduction
This paper studies decision problems related to graph properties from the perspective of distributed graph
algorithms. In distributed graph algorithms, the nodes of an unknown communication network (modeled
as a graph) work together in order to solve graph problems related to the structure of the communication
graph itself. As argued by Fraigniaud in his PODC 2010 keynote talk [10], the appropriate model for
distributed yes–no verification is the following:
• For a yes-instance, all nodes must output 1.
• For a no-instance, at least one node must output 0.
Intuitively, if we have an acceptable input, all nodes will be happy, and if we have an invalid input, at
least one node has to raise the alarm.
Our focus is on distributed verification that is made locally, by using a constant-time distributed
algorithm [21, 29]. Throughout this paper, we follow the convention that the running time of a distributed
algorithm equals the number of synchronous communication rounds. In particular, in a local algorithm
all nodes stop after O(1) communication rounds and announce their outputs. Equivalently, each node
makes its yes–no decision based on its constant-radius neighborhood in the communication graph.
Recall that a graph property is a family of graphs that is closed under isomorphism. We say that a
graph property P is locally checkable if it can be checked by a local algorithm. That is, there exists a
local algorithm, called verifier, that accepts all yes-instances G ∈ P and rejects all no-instances G ∈
/ P.
Examples. An easy example of a locally checkable property is determining if a given connected graph is
Eulerian: it is sufficient that each node outputs 1 if its degree is even, and 0 otherwise.
Another example is checking if a given graph is a line graph. If the nodes have unique identifiers, a
constant-time verifier can check that the graph does not contain any of the nine forbidden subgraphs in
Beineke’s [5] characterization of line graphs.
However, local checkability as such does not seem to lead to an interesting complexity theory—for
many well-studied graph properties, it is often easy to show that they are not locally checkable. The key
insight of Korman et al. [15, 16, 18, 19] is to study locally checkable proofs.
1.1 Locally checkable proofs
To illustrate the idea of locally checkable proofs, we start with a canonical example. Consider the problem
of checking if a given graph is bipartite. This is not a locally checkable property—indeed, if we consider
odd vs. even cycles, we can see that any verifier that solves the problem must have the running time Ω(n).
However, if we want to convince a local algorithm that the graph is indeed bipartite, we can augment
the graph with a locally checkable proof. It is sufficient to give 1 bit of proof per node: if the graph is
bipartite, we can give a 2-coloring of the graph as the proof, and a local verifier can check that the proof
is correct. Conversely, if the graph is not bipartite, no matter what proof bits we choose, at least one node
will detect that the proof is invalid. Hence we say the property of bipartiteness is in the class LCP(1): for
any bipartite graph, there is a locally checkable proof of size 1 bit per node. Precise definitions are given
in Section 2.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 2
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
The concept of locally checkable proofs is related to locally checkable properties as the familiar
complexity class NP is related to the class P. If a problem is in NP, then yes-instances have a concise
proof that can be verified in P. Similarly, if the problem is in LCP( f ), then yes-instances have a concise
proof with at most f (n) bits per node and the proof itself is checkable with a local algorithm. Equivalently,
we can interpret locally checkable proofs as nondeterministic local algorithms: in the algorithm, each
node can nondeterministically guess f (n) bits.
1.2 Contributions
The main contributions of this paper are the following:
1. We define the class LCP( f ) that consists of graph properties that admit locally checkable proofs of
size f (n) bits per node. This model is related to those studied by Korman et al. [15, 16, 18, 19] and
Fraigniaud et al. [11], but strictly stronger than both; see Section 3.
2. We catalog graph properties according to their local proof complexities, and we show that the
LCP( f ) classes form a natural hierarchy of decision problems. In particular, there are natural graph
properties that separate the following levels of the hierarchy: LCP(0), LCP(O(1)), LCP(O(log n)),
and LCP(poly(n)).
We refer to Tables 1 and 2 for a summary. Table 1 catalogs the complexity of verifying graph
properties (given a graph G, prove that G ∈ P), while Table 2 catalogs the complexity of verifying
solutions to graph problems (given a graph G and a solution X to graph problem P, prove that the
solution is correct).
3. We argue that LogLCP = LCP(O(log n)) is a particularly good candidate for a complexity class of
independent interest. The class is robust to variations in the exact definition of the LCP hierarchy.
Many graph properties are contained in LogLCP and not contained in LCP(o(log n)).
4. We present proof techniques that can be used to derive tight and near-tight lower bounds for the
local proof complexity. We show how to apply tools from other fields of computer science and
mathematics: results in extremal graph theory, fooling set arguments from the field of communica-
tion complexity, and gadgets that are typical in NP-hardness proofs. Here we mention, in particular,
our tight proof-size lower bound of Ω(log n) for non-bipartiteness and related graph properties, and
a near-tight lower bound of Ω(n2 / log n) for non-3-colorability.
2 Definitions and examples
To begin, we fix a family F of input graphs. For example, F might just be the set of all graphs (undirected,
unless otherwise noted), or perhaps F is the set of all connected graphs, i. e., we can work under a promise.
For a graph G ∈ F, we write V (G) for the set of nodes, E(G) for the set of edges, and n(G) = |V (G)|
for the number of nodes in G. If graph G is clear from the context, we simply use the symbols V , E,
and n. As is standard in distributed computing, we assume that the nodes of any G ∈ F are uniquely
identified with O(log n)-bit natural numbers (“identifiers”), that is, V (G) ⊆ {1, 2, . . . , poly(n(G))}. (As
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 3
M IKA G Ö ÖS AND J UKKA S UOMELA
Class Proof size s Graph property P Graph family F References
LCP(0) 0 Eulerian graphs connected §1
0 line graphs general §1
LCP(O(1)) Θ(1) s–t reachability undirected § 4.1
Θ(1) s–t unreachability undirected § 4.1
Θ(1) s–t unreachability directed § 4.1
Θ(1) s–t connectivity = k planar § 4.2
Θ(1) bipartite graphs general § 4.3
Θ(1) even n(G) cycles
LCP(O(log k)) O(log k) s–t connectivity = k general § 4.2
O(log k) chromatic number ≤ k general §2
LogLCP O(log n) any coLCP(0) property connected § 7.3
O(log n) any monadic Σ11 property connected § 7.5
Θ(log n) odd n(G) cycles §5
Θ(log n) chromatic number > 2 connected §5
LCP(poly(n)) Θ(n) fixed-point-free symmetry trees § 6.2
Θ(n2 ) symmetric graphs connected § 6.1
Ω(n2 / log n) chromatic number > 3 connected § 6.3
O(n2 ) any property connected §6
Table 1: The local proof complexity of verifying graph property P, when we are promised that the input
graph is in graph family F. Constant k is a natural number. In reachability problems, nodes s and t are
labeled; otherwise the graphs are unlabeled.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 4
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
Class Proof size s Graph problem P Graph family F References
LCP(0) 0 maximal matching general
0 any LCL problem general § 3, [21]
0 any LD problem connected § 3, [11]
LCP(O(1)) Θ(1) maximum matching bipartite § 4.3
LCP(O(logW )) O(logW ) max-weight matching bipartite § 4.3
LogLCP O(log n) any coLCP(0) problem connected § 7.3
Θ(log n) leader election connected § 5, [18]
Θ(log n) spanning tree connected § 5, [18]
Θ(log n) maximum matching cycles §5
Θ(log n) Hamiltonian cycle connected §5
LCP(∞) unlimited any NLD problem connected § 3, [11]
unlimited any NLD#n problem connected § 3, [11]
Table 2: The local proof complexity of verifying a solution to graph problem P, when we are promised
that the input graph is in graph family F. Here W is the maximum weight of an edge.
an exception, we study anonymous models without unique identifiers in Sections 7.1–7.2.) Depending on
the problem that we study, nodes and edges may also be associated with weights, colors, labels, etc.; if
this is the case, we say that the graph is labeled, and otherwise it is unlabeled.
2.1 Proofs, verifiers and locality
Proofs. A proof P for G is a function P : V (G) → {0, 1}? that associates a binary string with each node
of G. The size |P| of a proof P is the maximum number of bits in any string P(v), over all v ∈ V (G). We
write ε for an empty proof of size 0.
Verifiers. A verifier A is a function that maps each triple (G, P, v) to a binary output 0 or 1. Here G ∈ F
is a graph, P : V (G) → {0, 1}? is a proof, and v ∈ V (G) is a node of G. Intuitively, A(G, P, v) is the output
of node v if we run the distributed algorithm A in graph G and each node u ∈ V (G) is provided with
input P(u).
Remark 2.1. The issue of whether or not A is computable (or polynomial-time bounded) is usually
immaterial to our considerations. For simplicity, we do not impose any such resource constraints on A;
our focus will be on studying the limitations of verifiers arising from locality—as defined next.
Local verifiers. For a natural number r ∈ N and a node v ∈ V (G), let V [v, r] ⊆ V (G) be the ball of radius
r about v, i. e., set of nodes that are within distance r from v (the shortest path from v to any node in V [v, r]
has at most r edges). Let G[v, r] be the subgraph of G induced by V [v, r], and let P[v, r] : V [v, r] → {0, 1}?
be the restriction of a proof P : V (G) → {0, 1}? to V [v, r].
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 5
M IKA G Ö ÖS AND J UKKA S UOMELA
A verifier A is a local verifier if there exists a constant r ∈ N such that
A(G, P, v) = A(G[v, r], P[v, r], v) for all G, P, v .
That is, the output of a node v only depends on the input in its radius-r neighborhood. Constant r is the
local horizon of A. (Alternatively, if we consider Peleg’s [25] LOCAL model, a local verifier can be
defined as a constant-time distributed algorithm: a local verifier with horizon r can be implemented as a
distributed message-passing algorithm that completes in r synchronous communication rounds.)
2.2 Locally checkable proofs
A graph property P ⊆ F is a subset of graphs that is closed under isomorphism. Examples of graph
properties include Hamiltonian graphs, Eulerian graphs, bipartite graphs, connected graphs, line graphs,
trees, and cycles.
Definition 2.2. A graph property P ⊆ F admits locally checkable proofs of size s : N → N on family F if
there is a local verifier A that satisfies the following properties.
(i) Completeness: If G ∈ P then there exists a proof P : V (G) → {0, 1}? with |P| ≤ s(n(G)) such that
A(G, P, v) = 1 for each node v ∈ V (G).
(ii) Soundness: If G ∈ F \ P then for every proof P : V (G) → {0, 1}? there is at least one node v ∈ V (G)
with A(G, P, v) = 0.
That is, yes-instances have a valid proof that is accepted by all nodes, while no-instances are always
rejected by at least one node. If f is a function that associates a valid proof P = f (G) with each G ∈ P,
we say that the pair ( f , A) is a proof labeling scheme.
If a property P admits locally checkable proofs of size s, we write P ∈ LCP(s). We use coLCP(s) to
denote the class of graph properties whose complement is in LCP(s); that is, if F \ P ∈ LCP(s), we write
P ∈ coLCP(s). The class LogLCP consists of properties that are in LCP(s) for s = O(log n); we will see
in Section 5 that LogLCP admits many alternative characterizations, which makes it a particularly robust
class.
Examples. As we observed in Section 1, Eulerian graphs and line graphs can be verified without a proof,
and hence they are in LCP(0). As further observed in Section 1.1, bipartite graphs are not in LCP(0) but
they are contained in LCP(1), as they can be verified with one bit of input per node. More generally, if a
graph has chromatic number at most k, we can prove it with dlog ke bits per node: simply give a proper
k-coloring as the proof.
2.3 Extension: solutions to graph problems
If we consider labeled graphs, we can also define graph properties such as independent sets (“nodes with
label 1 form an independent set”) or spanning trees (“edges with label 1 induce a spanning tree”). That
is, we can interpret the labeling as a solution to a graph problem, and we can extend the definitions of
locally checkable proofs to verify solutions of graph problems.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 6
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
Formally, a graph problem P associates any graph G ∈ F with a set P(G) of solutions; each solution
is a labeled version of graph G. Contrary to the setting of graph properties, there are two natural variants
to verifying solutions of graph problem P:
• Strong proof labeling scheme ( f , A): for any graph G ∈ F, for any solution X ∈ P(G), there is a
locally checkable proof f (X) that is accepted by A, and any incorrect labeling X ∈
/ P(G) is rejected
by A.
• Weak proof labeling scheme ( f , A): for any graph G ∈ F, there is at least one solution X ∈ P(G)
such that there is a locally checkable proof f (X) that is accepted by A, and any incorrect labeling
X∈/ P(G) is rejected by A.
Put differently, in a strong proof labeling scheme, an adversary can choose both the input and the solution,
and we must come up with a locally checkable proof. However, in a weak proof labeling scheme, an
adversary chooses the input but we can choose a solution. These two notions are different even for natural
verification tasks.
Example 2.3 (Separating Strong from Weak). Consider the task of verifying whether a set of vertices
C ⊆ V (G) is a 2-approximation of a minimum vertex cover. It is straightforward to prove that without
proof bits, no strong proof labeling scheme exists for this task, i. e., the approximation ratio achieved
by an arbitrary C cannot be determined locally. On the other hand, on bounded-degree graphs there is a
constant-time local algorithm [4] that always outputs a set C∗ ⊆ V (G) that is a 2-approximation of the
minimum vertex cover—it is this C = C∗ that we can verify without proof bits in the weak sense.
In contrast to the above example, for the remaining problems studied in this paper, the local proof
complexities of strong and weak proof labeling schemes are within a constant factor of each other. All
proof labeling schemes that we will exhibit are of the strong variety whereas our lower-bound results
preclude not only the existence of strong proof labeling schemes for various problems, but also the
existence of weak proof labeling schemes.
3 Comparison with other models
Determinism. Our definition of the LCP hierarchy is an extension of locally checkable labelings (LCL)
introduced by Naor and Stockmeyer [21] in their seminal work. Naor and Stockmeyer focus on bounded-
degree graphs and constant-size labels, but if we generalize the class LCL in a straightforward manner,
we arrive at the class LCP(0).
Our classes LCP( f ) with f > 0 thus extend the classical LCL concept by providing f (n) bits of
additional information per node. We have chosen the terminology “LCP” to emphasize this connection,
admitting that it is a departure from some of the other terminology available in the literature, as outlined
next.
Nondeterminism. Our model is not the first, nor the last attempt at introducing nondeterminism in the
setting of local decision problems. Indeed, similar extensions have appeared in prior and independent
work. Two specific competing models are
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 7
M IKA G Ö ÖS AND J UKKA S UOMELA
• proof labeling schemes of Korman et al. [15, 16, 18, 19], and
• nondeterministic local decision of Fraigniaud et al. [11].
Our LCP model is the strongest among the trio: positive results in the other models imply positive results
in our model; this makes our lower-bound results widely applicable. In short, while an LCP verifier
algorithm is limited only by locality, the verifiers in the other two models have additional restrictions.
3.1 Proof labeling schemes
The proof labeling scheme model of Korman et al. [15, 16, 18, 19] is inspired by the classical notion of
labeling schemes (see Gavoille and Peleg [12] for a survey). In this model,
(i) the verifier has run-time of 1 communication round, and
(ii) a node cannot see the identifiers nor the input labels of its neighboring nodes.
That is, the output of a single node must be determined on the basis of its own identifier, own input label,
own proof label and the proof labels of the neighboring nodes. Thus, an upper bound on the local proof
complexity in this model provides an extremely efficient local checking procedure.
Because of these restrictions, verifiers in the proof labeling scheme model are sometimes rather
weak. For example, there are simple LCL problems that cannot be solved without proof labels in this
model: one example is the agreement problem of checking whether all nodes in a connected graph are
assigned the same input label [18, Lemma 2.3]; another example is checking whether the input graph is
triangle-free. Hence the notion of proof labeling schemes is not a straightforward generalization of the
LCL model—something our LCP model strives to be.
However, we note that in some cases the gap between the models can be bridged at the cost of an
additive proof-size overhead of Θ(log n)—or however many bits of local data (node identifiers, input
labels) are hidden by the restrictions (i)–(ii). This means, for instance, that the two models admit roughly
the same analysis at the LCP(poly(n)) level (Section 6).
In comparison with prior work related to proof labeling schemes, the main challenges of the present
paper can be summarized as follows:
1. Logarithmic lower bounds from prior work do not apply directly. It is harder to fool an LCP
verifier that sees all the information available in its constant-radius neighborhood (in particular,
O(log n)-bit identifiers). Therefore we need stronger techniques to prove Ω(log n) proof-size lower
bounds in Section 5.
2. Superlogarithmic lower bounds would apply, but few such bounds are known for graph properties.
It seems that the main focus in the prior work has been on problems related to labeled graphs. We
can reuse ideas from prior work in Sections 6.1–6.2 in the context of symmetric graphs, but we are
not aware of any prior work related to non-3-colorability that we could apply in Section 6.3.
For logarithmic lower bounds, our novel idea is to invoke an extremal result of Bondy and Simonovits [6]
in the context of a “gluing” argument. For superlogarithmic lower bounds, the novel idea is to apply the
disjointness problem to construct a difficult graph problem, while prior work has focused on constructions
that are based on equality.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 8
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
3.2 Nondeterministic local decision
Independently of our work, Fraigniaud et al. [11] have also studied nondeterminism (along with random-
ness) in the context of distributed decision problems. Here, the major difference to our model is that
the local proofs P : V (G) → {0, 1}? are not allowed to depend on the identifier assignment on G. This
implies, for example, that many leader election problems are not solvable at all in their model, no matter
how large P is (cf. Section 7.1).
To connect the results of Fraigniaud et al. to our work, let us define LCP0 ( f ) similarly to LCP( f ) but
restricted to computable properties of connected graphs. With this notation, the class LD of local decision
problems defined by Fraigniaud et al. is equal to LCP0 (0). The nondeterministic variants of LD are called
NLD and NLD#n ; in the latter class each node knows the total number of nodes in the graph. It turns out
that our class LCP0 (∞) is equal to NLD#n : both classes contain all computable properties of connected
graphs. Hence using the separation results of Fraigniaud et al. we have
LCP0 (0) = LD ( NLD ( NLD#n = LCP0 (∞) .
While Fraigniaud et al. place one class between the extreme ends of LCP0 (0) and LCP0 (∞), our work
introduces an entire hierarchy of LCP( f ) classes.
4 Problems in LCP(O(1))
As a warm-up, this section gives examples of graph properties and graph problems that admit locally
checkable proofs of size O(1) but for which there is no locally checkable proof of size 0. We will see that
many fundamental problems related to graph connectivity are in this class.
4.1 Reachability
To ask meaningful questions about connectivity in the LCP model, we require that two nodes s and t are
always distinguished in the input graph G; that is, we have the promise that there is exactly one node
with label s and exactly one node with label t. It is easy to see that in LCP(0) we cannot check whether
there is a path from s to t in G. However, many questions related to reachability and connectivity are in
LCP(O(1)).
Let us first consider the s–t reachability problem in an undirected graph G, i. e., proving that there is a
path from s to t. This problem admits a locally checkable proof of size 1: we find a shortest path from s to
t in G, define that U ⊆ V consists of all nodes on the shortest path, and set P(v) = 1 iff v ∈ U. A verifier
can locally check that: (i) s,t ∈ U; (ii) s and t have unique neighbors in U; and (iii) every u ∈ U \ {s,t}
has exactly two neighbors in U [14, p. 130].
Interestingly, the above method breaks down in directed graphs because of back-edges. In graphs
of maximum degree ∆, one can still give an easy upper bound of O(log ∆) by using edge pointers in the
proof labeling to describe a path from s to t, but it is an open problem whether directed s–t reachability is
in LCP(O(1)) for general graphs (see also Ajtai and Fagin [1]).
However, it is easy to show that the complement of the above problem, s–t unreachability, is in
LCP(O(1)) both for undirected and directed graphs. We find a partition S ∪ T of V such that s ∈ S, t ∈ T ,
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 9
M IKA G Ö ÖS AND J UKKA S UOMELA
and there is no (directed) edge from S to T . Such a partition can be encoded with 1 bit per node, and it
can be verified locally.
4.2 Connectivity
As a natural generalization of reachability, we can study the s–t connectivity of undirected graphs;
throughout this text, we focus on the vertex connectivity. By extending the techniques of Korman et
al. [18] we can show that graphs with s–t connectivity equal to k admit locally checkable proofs of size
O(log k). Here we assume that k is given as input to all nodes (or, equivalently, that k is a global constant).
If and only if the vertex connectivity is exactly k, then by Menger’s theorem [7, p. 62] we can find
(i) a partition S ∪ C ∪ T of V such that s ∈ S, t ∈ T , and |C| = k, and (ii) k vertex-disjoint s–t paths
p1 , p2 , . . . , pk such that |C ∩ pi | = 1. Without loss of generality, we can assume that each pi is locally
minimal in the sense that it cannot be made shorter without colliding with the other paths p j , j 6= i.
The proof label P(v) encodes whether v ∈ S, v ∈ C, or v ∈ T . Moreover, in the proof label P(v) of a
vertex v ∈ pi \ {s,t}, we include the path index i (in binary) and also the distance of v from s modulo 3:
this allows us to store the orientation on the path pi . The local verifier can verify that:
1. Nodes s and t have exactly k neighbors labeled with path indices 1, 2, . . . , k.
2. Each v ∈ pi \ {s,t} has exactly one predecessor and one successor along pi .
3. We have s ∈ S, t ∈ T , and there is no edge between S and T .
4. Each v ∈ C is on a path pi , its predecessor along pi is in S and its successor is in T .
If the above checks go through, the structure encoded by the proof P contains exactly k disjoint s–t paths.
It may contain some oriented cycles inside S or inside T as well, but this is sufficient to convince the
verifier that the connectivity of s and t is at least k. Moreover, if a path crosses C, its color changes from
S to T ; its color cannot change back to S, and it cannot disappear without reaching t. Hence the above
checks are also sufficient to convince the verifier that the size of the s–t separator C is at most k. In
summary, s–t-connectivity has to be equal to k.
Finally, we note that the sole source for the O(log k) label size was the need to store the path indices.
However, on planar graphs, only 3 path indices suffice to tell adjacent paths from one another; an
adaptation of the above method gives a constant size proof in the case of planar graphs.
4.3 Bipartite matching
While maximal matchings can be verified without any proofs, verifying maximum-cardinality matchings
requires some auxiliary information. In this section we study bipartite graphs; later in Section 5.4 we will
show that the methods below break down on non-bipartite graphs.
Maximum matching. To construct a constant-size proof P for maximum matchings on a bipartite
graph G we can use König’s theorem [7, p. 35], which states that, on bipartite graphs, the maximum
size of a matching equals the minimum size of a vertex cover. Indeed, take any minimum vertex cover
C ⊆ V (G), and set P(v) = 1 iff v ∈ C. For any matching M ⊆ E(G), we then have, by König’s theorem,
that M is of maximum size if and only if |C| = |M|. To check this condition locally, we simply verify
that M is a valid matching, the set C encoded in the proof forms a vertex cover, and each edge of M has
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 10
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
exactly one endpoint in C. This proves that maximum matchings in bipartite graphs are in LCP(1), as the
size of P is 1.
Maximum-weight matching. Generalizing the above example, we can use linear programming duality
to prove that in an edge-weighted bipartite graph G, a subset of edges M ⊆ E(G) is a maximum-weight
matching. Associate a variable xe ≥ 0 with each edge e ∈ E, and a dual variable yv ≥ 0 with each node
v ∈ V . Let we ∈ N be the weight of edge e, and let A be the vertex-edge incidence matrix of graph G.
Recall (e. g., [24, §13.2]) that matrix A and its transpose A> are totally unimodular, and hence there are
integral vectors x and y that maximize ∑e we xe subject to Ax ≤ 1 (primal LP) and minimize ∑v yv subject
to A> y ≥ w (dual LP). Each maximum-weight matching M corresponds to an optimal integral solution x
of the primal LP, and we can use an optimal dual solution y as a proof; for each node v ∈ V , the proof
consists of a binary encoding of the value yv . To verify the proof, it is sufficient to check that x and y
satisfy the complementary slackness conditions. If the weights are integers from 0, 1, . . . ,W , then we can
find an optimal dual solution such that yv ∈ {0, 1, . . . ,W } for each node v. Hence the size of the proof is
O(logW ) bits.
5 Problems in LogLCP
In this section we give examples of graph properties and graph problems that admit locally checkable
proofs of size O(log n) but for which there is no locally checkable proof of size o(log n). That is, these
problems are in LogLCP but not in any lower level of the LCP hierarchy. We begin with positive results
that directly build on prior work—a key ingredient is the observation that spanning trees in connected
graphs are in LogLCP. After that, we give our new lower-bound results.
5.1 Positive results
A spanning tree is not locally checkable, but Korman et al. [18] show that any spanning tree T can be
equipped with a proof of size O(log n) that, for each vertex v, consists of (i) the identity of a particular
vertex a, the root, and (ii) the distance from v to a in T . Such a proof can be locally verified by checking
that the root-distance at a is 0, and that for each vertex v (i) all neighbors of v agree on the identity of
the root, and (ii) the root-distance decreases at exactly one neighbor of v in T and increases at other
neighbors.
A spanning tree equipped with a locally checkable proof is a versatile tool. For example, consider
the leader election problem: there has to be exactly one node that is labeled as the leader. In connected
graphs, we can verify any solution to the leader election problem by constructing a spanning tree that is
rooted at the leader.
Spanning trees can be also used to prove that the graph is acyclic: we simply show that each
component is a tree. Hamiltonian cycles and Hamiltonian paths can be verified by using the same
technique: a Hamiltonian path can be interpreted as a spanning tree.
With spanning trees, we can also gather global information about the input graph. For instance, every
node can be convinced of the value of n(G) on a connected graph G with the aid of a spanning tree with
node counters along the paths towards the root: the leaves have counter value 1, and a non-leaf carries the
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 11
M IKA G Ö ÖS AND J UKKA S UOMELA
sum of the counter values of its children plus 1. Hence graph properties such as having an odd number of
nodes are also in LogLCP.
In LogLCP, we can also show that the chromatic number of a connected graph is larger than 2 (i. e.,
the graph is not bipartite). To construct a proof, first find an odd cycle in the graph—such a cycle exists if
and only if the graph is non-bipartite. Then select one of the nodes of the cycle as the leader a. Construct
a spanning tree rooted at a; this way the verifier can check that there exists exactly one leader. Then
propagate a node counter along the cycle, starting and ending at a; this way the leader node can be
convinced that it is indeed part of an odd cycle.
5.2 Negative results: overview
We will now prove the following theorem.
Theorem 5.1. The following graph properties and graph problems do not admit locally checkable proofs
of size o(log n): graphs with odd number of nodes, non-bipartite graphs, spanning trees, and leader
election.
Hence these are examples of problems whose containment in LogLCP is tight: their local proof
complexity is exactly Θ(log n).
Proof sketch. The negative results build on the same basic idea. We will consider graph properties on
cycles. We will assume that there is a proof labeling scheme ( f , A) with o(log n)-bit proofs. We will take
several yes-instances—each of them is a short cycle—and inspect the encoding produced by f . Then we
will show that some of the yes-instances are necessarily compatible with each other in the following sense:
we can take several short cycles and glue them together to form a longer cycle; the unique identifiers
and the proof labels are inherited from the short cycles, and each node of the long cycle will be locally
indistinguishable from a node of a short cycle. Hence the verifier will accept the long cycle, as it has to
accept all short cycles.
However, even though the short cycles are yes-instances, the long cycle will be a no-instance. For
example, in the case of non-bipartiteness, each short cycle has an odd number of nodes, but the long
cycle is composed of an even number of short cycles, and is therefore a no-instance. In the case of leader
election, each short cycle has one leader node, while the long cycle will contain multiple leaders, and is
therefore an invalid solution. Similar ideas can be applied to many other lower bounds.
Subtleties. The only combinatorial hurdle in carrying out the above strategy is in making sure that
there are enough proof-labeled neighborhoods among the yes-instances accepted by A that they can
be reassembled into the long no-instance. To this end we invoke an extremal result of Bondy and
Simonovits [6] on a certain bipartite compatibility graph. (By contrast, recall that in the model of Korman
et al. [18] such gluing operations were made easy by the limited vision of a local verifier—we did not
have to worry about node identifiers.)
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 12
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
5.3 The proof
Let F be a family of graphs that contains (at least) all cycles. In each graph G ∈ F, we may have a
constant number of bits of auxiliary information per node (colors, labels, etc.). Let P ⊆ F be a graph
property. Assume that ( f , A) is a proof labeling scheme for property P that uses o(log n)-bit proofs. Fix
an integer constant k ≥ 2. Let n be a sufficiently large positive integer. We will assume that n-cycles
(with appropriate auxiliary information) are in P.
Our plan is to show that we can always find k yes-instances, each of which is an n-cycle, and we can
glue them together to form a kn-cycle that inherits the proof labels (and auxiliary information, if any)
from the yes-instances. Verifier A will accept each n-cycle, and therefore it will also accept the kn-cycle.
For an example, refer to Figures 1 and 2.
Partitioning the space of identifiers. First, split n = nA + nB , where nA = bn/2c and nB = dn/2e.
Fix any partition of the set of identifiers {1, . . . , n2 } into 2n subsets a1 , . . . , an , b1 , . . . , bn so that each
a ∈ A := {a1 , . . . , an } is of size nA , and each b ∈ B := {b1 , . . . , bn } is of size nB . We denote by a[i] (resp.,
b[i]) the i-th identifier in a (resp., b) in the natural order.
For example, if n = 10, we have nA = nB = 5. We can choose the partition a1 = {1, 2, . . . , 5},
a2 = {6, 7, . . . , 10}, . . . , b10 = {96, 97, . . . , 100}. In this case a2 [1] = 6, b10 [2] = 97, etc.
Family of yes-instances. Next, we define a family of yes-instances C(a, b) indexed by pairs (a, b) ∈
A × B. Define C(a, b) to be the n-cycle that contains the nodes a in increasing order followed by the
nodes b in decreasing order, completing the cycle. That is, a[1] and b[1] are adjacent, as are a[nA ] and
b[nB ]; see Figure 1a. Note that V (C(a, b)) and V (C(a0 , b0 )) are disjoint if a 6= a0 and b 6= b0 .
Augment each C(a, b) with auxiliary information such that C(a, b) is in P, if necessary; let Lab (v) ∈
{0, 1}? be the bit string associated with node v ∈ V (C(a, b)). For example, if we are interested in the
leader election problem, label exactly one node in each C(a, b) as the leader: select a node u ∈ V (C(a, b))
and set Lab (u) = 1 and Lab (v) = 0 for all v 6= u. We can consider either the best-case or the worst-case
choice of the leader, thus covering both weak and strong proof labeling schemes.
Recording proof bits. Now we make use of the assumption that property P admits o(log n)-bit proofs.
Apply f to C(a, b) to construct a locally checkable proof Pab of size o(log n). For each node v ∈ V (C(a, b)),
0 (v) = (L (v), P (v)). Finally, define
let Pab ab ab
0 0 0 0 0 0
c(a, b) = Pab (a[2r + 1]), Pab (a[2r]), . . . , Pab (a[1]), Pab (b[1]), Pab (b[2]), . . . , Pab (b[2r + 1]) .
That is, c(a, b) consists of all auxiliary information and all proof bits that are available within distance
2r + 1 from the node a[1] or b[1] in C(a, b); see Figure 1a. By assumption, we have o(r log n) bits of
information in c(a, b).
Finding compatible cycles. Now let Kn,n = (A ∪ B, E) be the complete bipartite graph with E =
{{a, b} : a ∈ A, b ∈ B}. We define an edge coloring of Kn,n as follows: the color of the edge {a, b} ∈ E is
c(a, b). For a sufficiently large n, the number of bits of information in c(a, b) is smaller than log(n)/3,
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 13
M IKA G Ö ÖS AND J UKKA S UOMELA
(a) a[1] b[1] (b) edge colour
c(a, b) b
a[2] b[2] a
c(a, b)
a[3] b[3]
C(a, b)
a[4] b[4] a’ b’
c(a’, b’)
a[5] b[5]
(c)
a[1] b[1] a’[1] b’[1]
a[2] b[2] a’[2] b’[2]
a[3] C b[3] a’[3] b’[3]
a[4] b[4] a’[4] b’[4]
a[5] b[5] a’[5] b’[5]
a[1] b[1] a’[1] b’[1]
a[2] b[2] a’[2] b’[2]
c(a, b) c(a’, b’)
a[3] b[3] a’[3] b’[3]
C(a, b) C(a’, b’)
a[4] b[4] a’[4] b’[4]
a[5] b[5] a’[5] b’[5]
Figure 1: An illustration of the Ω(log n) lower-bound construction; here n = 10, r = 1, and k = 2.
(a) Construction of the cycle C(a, b). We consider the leader election problem in this example; hence
precisely one node is highlighted to indicate the leader node. (b) A monochromatic 2k-cycle a, b, a0 , b0 in
Kn,n . (c) Constructing the kn-cycle C by gluing together two compatible n-cycles, C(a, b) and C(a0 , b0 ).
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 14
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
√
and the number of distinct colors in Kn,n is therefore smaller than 3 n. Hence there is a subset of edges
√
H ⊆ E such that |H| > |E|/ 3 n = n5/3 and all edges of H have the same color.
Now we can apply the result due to Bondy and Simonovits [6]: for any k ≥ 2 and for a suffi-
ciently large n, the subgraph (A ∪ B, H) necessarily contains a 2k-cycle. Let the nodes of the cycle be
a1 , b1 , a2 , b2 , . . . , ak , bk in this order, such that ai ∈ A and bi ∈ B for each i. As all edges of the cycle have
the same color, we have
c(a1 , b1 ) = c(a2 , b2 ) = · · · = c(ak , bk ) = c(a1 , bk ) = c(a2 , b1 ) = · · · = c(ak , bk−1 ) .
For convenience, define b0 = bk and ak+1 = a1 .
Gluing. Next, we glue together the n-cycles C(a1 , b1 ),C(a2 , b2 ), . . . ,C(ak , bk ) to construct a kn-cycle
C. That is, we take the node-disjoint graphs C(ai , bi ), remove the edges {ai [1], bi [1]} for each i, and add
{bi−1 [1], ai [1]} for each i > 1. For each node v ∈ V (C), we inherit the auxiliary information L(v) and the
proof bits P(v) from the cycles C(ai , bi ). The gluing process is illustrated in Figure 1c for the case k = 2.
We have two compatible n-cycles, C(a, b) and C(a0 , b0 ), and we connect a[1] to b0 [1] and a0 [1] to b[1].
Analysis. It remains to argue that the computation of A on C with the labels L and proof P is accepting.
To see this, pick a vertex v ∈ V (C). Then there is an i such that v ∈ V (C(ai , bi )). If v is far from ai [1] and
bi [1], then the local neighborhood of v looks identical in C and C(ai , bi ); as C(ai , bi ) is a yes-instance, v
accepts the input. If v is near bi [1], then the local neighborhood of v looks identical in C and C(ai+1 , bi ),
which is another yes-instance. Similarly, if v is near ai [1], then its local neighborhood looks identical in
C and C(ai , bi−1 ), which is also a yes-instance (see Figure 2 for an illustration). In all cases, v accepts
the input. Thus the kn-cycle C is accepted by all nodes. If C ∈ / P, we have a contradiction, and we can
conclude that the graph property P does not admit locally checkable proofs of size o(log n).
5.4 Implications
Now we can give concrete examples of graph properties and graph problems P for which C ∈
/ P, provided
that we choose the parameters k and n properly:
• Non-bipartite graphs: We can select an odd n and k = 2.
• Leader election: It is sufficient to choose k = 2. Then each C(a, b) contains exactly one node
labeled as a leader and C contains two nodes.
• Spanning trees: Again, we can choose k = 2. The spanning tree in each C(a, b) contains all edges
of E(C(a, b)) except one, i. e., it is a spanning path. The solution encoded in C consists of two
disjoint paths, and is therefore not a spanning tree.
We can also apply the same construction to counting problems: to give a simple example, if we choose an
odd n and an even k, then n(C(a, b)) is odd while n(C) is even.
We can also prove lower bounds for optimization problems. Consider, for example, the problem of
finding a maximum matching in a cycle. If n is odd, then each C(a, b) has necessarily one unmatched
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 15
M IKA G Ö ÖS AND J UKKA S UOMELA
a’[1] b[1] a[1] b’[1]
a’[2] b[2] a[2] b’[2]
c(a’, b) c(a, b’)
a’[3] b[3] a[3] b’[3]
C(a’, b) C(a, b’)
a’[4] b[4] a[4] b’[4]
a’[5] b[5] a[5] b’[5]
a[1] b[1] a’[1] b’[1]
a[2] b[2] a’[2] b’[2]
a[3] C b[3] a’[3] b’[3]
a[4] b[4] a’[4] b’[4]
a[5] b[5] a’[5] b’[5]
a[1] b[1] a’[1] b’[1]
a[2] b[2] a’[2] b’[2]
c(a, b) c(a’, b’)
a[3] b[3] a’[3] b’[3]
C(a, b) C(a’, b’)
a[4] b[4] a’[4] b’[4]
a[5] b[5] a’[5] b’[5]
Figure 2: Cycle C was constructed by gluing together two compatible n-cycles, C(a, b) and C(a0 , b0 ). The
grey arrows indicate pairs of nodes that have identical local neighborhoods: some parts of C look locally
identical to C(a, b) or C(a0 , b0 ), while other parts look locally identical to C(a, b0 ) or C(a0 , b).
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 16
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
node. The solution inherited from C(a, b) to C has therefore k unmatched nodes, and cannot be optimal.
Hence all of these problems require proofs of size Ω(log n) and the lower bound is tight. This concludes
the proof of Theorem 5.1.
6 Problems in LCP(poly(n))
In the previous sections, we have seen problems that admit locally checkable proofs of size O(log(n)).
Now we turn our attention to the problems that require much larger proofs. If the nodes can have arbitrary
labels (e. g., weights), it is easy to come up with artificial problems that require arbitrarily large proofs.
However, in this section we will focus on finding natural examples of graph properties that are related to
unlabeled graphs: we do not have any additional information besides the structure of the graph G and the
unique node identifiers.
In connected graphs, any property of unlabeled graphs admits locally checkable proofs of size O(n2 ).
We can encode the structure of G and the unique node identifiers in O(n2 ) bits; the nodes can verify that
their neighbors agree on the structure of G and that their local neighborhoods match those in G. Finally,
the nodes can solve the problem by brute force.
In this section, we will show that there are natural graph properties that require Ω(n2 )-bit proofs.
Such problems are the most difficult problems from the LCP perspective—we can only save a constant
factor in comparison with the brute-force solution.
6.1 Symmetric graphs
In this section, we fix F to be the family of connected graphs. We say that a graph G is symmetric if it has
a non-trivial automorphism, that is, there is an automorphism g : V → V that is not the identity function;
otherwise it is asymmetric.
Theorem 6.1. Symmetricity of connected graphs requires locally checkable proofs of size Ω(n2 ).
Proof. To reach a contradiction, assume that there exists a proof labeling scheme ( f , A) with o(n2 )-bit
proofs. To facilitate the proof, we will use canonical forms of graphs. We associate a canonical form C(G)
with any graph G. Graphs G and C(G) are isomorphic; moreover, whenever G and H are isomorphic,
their canonical forms C(G) and C(H) are equal. We assume that the node identifiers of a canonical form
are V (C(G)) = {1, 2, . . . , n(G)}. We also define a graph with shifted identifiers as follows: for an integer
i, graph C(G, i) has V (C(G, i)) = {i + 1, i + 2, . . . , i + n(G)} as the set of node identifiers. Moreover, we
assume that g : v 7→ i + v is an isomorphism from C(G) to C(G, i). In particular, C(G, 0) = C(G).
Now we are ready to give the lower-bound construction. Given two connected graphs G1 and G2
with n(G1 ) = n(G2 ) = k, we construct a graph G = G1 } G2 with V (G) = {1, 2, . . . , 3k} as follows: G
consists of a copy of C(G1 , k), a copy of C(G2 , 2k), and the path (k + 1, 1, 2, . . . , k, 2k + 1). That is, G
consists of a path that joins graphs that are isomorphic to G1 and G2 .
Assume that G1 and G2 are asymmetric. If G1 and G2 are isomorphic, then G = G1 } G2 is symmetric:
there is a non-trivial automorphism that maps 1 7→ k and k + 1 7→ 2k + 1 and so on. Conversely, if G
admits a non-trivial automorphism ϕ, then, by the construction of G, we must have that ϕ swaps G1 and
G2 . This way, ϕ induces an isomorphism of G1 and G2 .
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 17
M IKA G Ö ÖS AND J UKKA S UOMELA
Let Fk be a family containing a representative from each isomorphism class of asymmetric connected
graphs with k nodes. For any G1 ∈ Fk , the local verifier A has to accept G1 } G1 , as it is symmetric.
Since almost all graphs are connected [7, Cor. 11.3.3] and asymmetric [8], we have
k
|Fk | = (1 − o(1))2(2) /k! and log |Fk | = Θ(k2 ) .
Now assume that k ≥ 2r + 1, where r is the local horizon of A. Consider the proof labels of the nodes
in U = {1, 2, . . . , 2r + 1}. There are only o(rn2 ) proof bits in U. As r = O(1) and n = 3k, we have only
o(k2 ) proof bits in U; for sufficiently large k this is less than log |Fk |. Hence we must have two different
graphs G1 , G2 ∈ Fk such that the labeling scheme assigns the same proof bits to the nodes 1, 2, . . . , 2r + 1
in both G1 } G1 and G2 } G2 .
Now we can construct the asymmetric graph G = G1 } G2 . For the nodes k + 1, k + 2, . . . , 2k we
inherit the proof labels from f (G1 } G1 ), and for the nodes 2r + 2, 2r + 3, . . . , k, 2k + 1, 2k + 2, . . . , 3k we
inherit the proof labels from f (G2 } G2 ). For the nodes 1, 2, . . . , 2r + 1 we use the common labeling of
f (G1 } G1 ) and f (G2 } G2 ). Now the radius-r neighborhood of any node in G looks identical to the
neighborhood of a node in G1 } G1 or G2 } G2 . Hence all nodes will accept the input even though G is
not symmetric, a contradiction.
Remark 6.2. The basic idea of the above proof is similar to Korman et al. [18, Corollary 2.4]. However,
Korman et al.’s construction gives a problem related to graphs that are labeled with unique identifiers; it
is not a graph property in the usual sense (closed under re-assigning the identifiers).
6.2 Fixed-point-free symmetry on trees
In this section, we fix F to be the family of connected trees. Here, any graph property P ⊆ F admits a
locally checkable proof of size O(n): for each node v of the tree G ∈ P, we encode the structure of G and
an index that identifies which node of G is v; the structure of a tree can be encoded in Θ(n) bits, and the
index requires Θ(log n) bits.
Now we will show that there are properties of unlabeled trees that require Θ(n)-bit proofs. We will use
the following (artificial) problem as an example. We say that a graph G has a fixed-point-free symmetry if
there is an automorphism that fixes no nodes, i. e., there is an automorphism g : V (G) → V (G) such that
g(v) 6= v for all v ∈ V (G).
Theorem 6.3. Trees with a fixed-point-free symmetry require locally checkable proofs of size Θ(n).
The proof is analogous to the case of symmetric graphs. The only difference is that we let Fk consist
of rooted trees with k nodes; if G1 , G2 ∈ Fk and k is even, then G1 } G2 has a fixed-point-free symmetry
if and only if G1 = G2 . We have log |Fk | = Θ(k) [28, Seq. A000081]; hence a proof of size o(n) bits
leads to a contradiction.
6.3 Non-3-colorability
Now we turn our attention to the classical problem of graph coloring. In Section 5 we have already seen
that in the case of 2-colorability, the complement of the problem is strictly more difficult: to show that
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 18
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
a graph can be colored with 2 colors a Θ(1)-bit proof is sufficient, but to show that a graph cannot be
colored with 2 colors we need Θ(log n)-bit proofs.
In the case of 3-colorings, the difference between the problem and its complement is even more
dramatic. Again, constant-size proofs are enough to show that a graph can be colored with 3 colors, as
we can give a 3-coloring as a proof. However, to prove that a graph cannot be colored with 3 colors, we
need very large proofs, with polynomially many bits per node.
Theorem 6.4. Non-3-colorability requires locally checkable proofs of size Ω(n2 / log n).
Let F be the family of connected graphs, and let P ⊆ F consist of graphs that have chromatic number
larger than 3. We will show that property P does not admit locally checkable proofs of size o(n2 / log n).
Recall that any property of unlabeled graphs admits proofs of size O(n2 ); hence the result is almost tight,
and shows that non-3-colorability does not have a proof labeling scheme that is substantially better than
the brute-force approach.
Proof overview. The template for our lower-bound proof will be the disjointness problem in two-party
communication complexity: two players, Alice and Bob, are given sets A and B, respectively, and
they need to communicate to find out whether A ∩ B = ∅. It is well-known that this problem has high
communication complexity even in the nondeterministic setting where the players seek to prove that
A ∩ B = ∅; see Example 1.23 and Lemma 2.4 in Kushilevitz and Nisan [20]. Recall also that proving
A ∩ B 6= ∅ is easy: simply guess an element in A ∩ B.
Our lower bound graph G = GA,B will have two subgraphs GA and GB that are owned by Alice
and Bob, respectively. These subgraphs are connected by some Θ(log n) wires, that, intuitively, allow
nondeterministic communication between the players (via the proof labels). The subgraphs GA and GB
are constructed in such a way that if we are given any partial 3-coloring c of G defined only on the wires
of G, then c can be extended to 3-coloring of GA (resp., GB ) if and only if c encodes, in a certain way,
an element in A (resp., B). This means that GA,B will be 3-colorable iff A ∩ B 6= ∅—or in other words
GA,B will be non-3-colorable iff A ∩ B = ∅. A communication complexity argument then implies that the
wires must carry large proof labels.
Properties of GA . Let k be a positive integer. Define I = {0, 1, . . . , 2k − 1}. Given a set A ⊆ I × I, we
construct a graph GA , with the following properties:
(i) The total number of nodes in GA is Θ(2k ).
(ii) The set of nodes V (GA ) contains the following nodes: T , F, N, x0 , x1 , . . . , xk−1 , and y0 , y1 , . . . , yk−1 .
Moreover, proper 3-colorings of GA have the following properties:
(iii) The nodes T , F, and N have three different colors. The nodes with the same color as T are said to
be true, those with the same color as F are false, and others are neutral.
(iv) Each of xi and yi has to be true or false. Hence we can interpret the coloring of the nodes xi as a
binary encoding of an integer x ∈ I; similarly the coloring of the nodes yi is a binary encoding of
an integer y ∈ I.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 19
M IKA G Ö ÖS AND J UKKA S UOMELA
(v) In any 3-coloring, we must have (x, y) ∈ A. Conversely, we can find a proper 3-coloring that
encodes any (x, y) ∈ A.
An explicit construction of GA follows. In the subsequent analysis the details of the construction are not
used outside of the above properties (i)–(v).
Gadgets. We begin with the basic building blocks of GA . In graph GA , nodes T , F, and N form a
triangle, ensuring that in any 3-coloring these nodes have different colors.
N
T
F
Recall that the nodes with the same color as T are said to be true, those with the same color as F are
false, and others are neutral. Nodes T , F, and N are extensively used in the construction of the following
gadgets.
A Boolean gadget has two terminals; see Figure 3. In a proper 3-coloring, exactly one terminal is
true and the other terminal is false; conversely, any such assignment is a proper 3-coloring.
A color changer has one input node and one output node; see Figure 4. In any proper 3-coloring,
a true input implies a true output while a neutral input implies a false output (and a false input is not
possible); conversely, any such assignment can be realized as a proper 3-coloring.
A disjunction gadget has a number of output nodes; see Figure 5. In any proper 3-coloring, at least
one output node is true and all other output nodes are neutral; conversely, any such assignment can be
realized as a proper 3-coloring. The construction uses Boolean gadgets.
Finally, we construct a binary decoder as illustrated in Figure 6. There are k input nodes, labeled
with x0 , x1 , . . . , xk−1 , and 2k output nodes, labeled with 0, 1, . . . , 2k − 1, i. e., with a number in I. In any
3-coloring, each input node is either true or false, while each output node is either true or neutral. The
color assignment of the input nodes can be interpreted as a binary encoding of a number i ∈ I, and the
decoder guarantees that only the output node with label i is true. Conversely, any such assignment can be
realized as a proper 3-coloring. In the construction of the binary decoder, a disjunction gadget ensures
that at least one output node is true, while the edges between inputs and outputs ensure that if an output
node is true, its index matches the truth assignment of the input nodes. Now we have all basic ingredients
for constructing graph GA .
Construction of GA . The high-level structure of graph GA is shown in Figure 7. There are 2k + 3
terminals: T , F, N, x0 , x1 , . . . , xk−1 , and y0 , y1 , . . . , yk−1 . There are also non-terminal nodes ai , bi , and ci
for i ∈ I.
The construction contains two binary decoders: one mapping inputs x j to outputs ai , and the other
mapping inputs yi to outputs c j . Moreover, there are 2k color changers, each of them mapping input ai to
output bi . Finally, we have an edge {bi , c j } if and only if (i, j) ∈ / A.
Now in any proper 3-coloring, nodes x j and y j have to be either true or false; we can interpret the
coloring of nodes x j as the binary encoding of a number x ∈ I, and the coloring of nodes y j as the binary
encoding of a number y ∈ I. By construction, we have
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 20
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
(a) = N (b) = =
Figure 3: (a) Boolean gadget: one terminal is true, one terminal is false. (b) Proper 3-colorings.
input
(a) = F N (b) = =
output
Figure 4: (a) Color changer: true 7→ true but neutral 7→ false. (b) Proper 3-colorings.
outputs
F F
(a) (b)
T T
Figure 5: (a) Disjunction gadget with four output nodes. (b) An example of a proper 3-coloring.
(i) ai is true iff i = x; otherwise ai is neutral,
(ii) bi is true iff i = x; otherwise bi is false,
(iii) ci is true iff i = y; otherwise ci is neutral.
In particular, both bx and cy are true, and therefore we must have (x, y) ∈ A. Conversely, for any pair of
integers (x, y) ∈ A, we can construct a proper 3-coloring of GA such the coloring of x j forms the binary
encoding of x and the coloring of y j forms the binary encoding of y.
Construction of G = GA,B . We have now completed the construction of GA for any given set A ⊆ I × I.
In what follows, we denote by G0A an isomorphic copy of GA ; we use the primed symbols T 0 , F 0 , N 0 , xi0 ,
and y0i to refer to the terminal nodes of G0A .
We will need one more gadget: a wire that propagates colors; see Figure 8. A wire w consists of 9r
nodes, labeled w(i, j) for i = 1, 2, . . . , 3r and j = 1, 2, 3. For each i, the nodes w(i, 1), w(i, 2), and w(i, 3)
form a triangle. For each i < 3r and j 6= j0 , the nodes w(i, j) and w(i + 1, j0 ) are connected with an edge.
It follows that in any 3-coloring of a wire, the nodes w(i, 1), w(i, 2) and w(i, 3) must have different colors,
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 21
M IKA G Ö ÖS AND J UKKA S UOMELA
0 1 7
(a) Disjunction
x0
x1
x2
0 2 7
(b)
x0
x1
x2
Figure 6: (a) A binary decoder for k = 3. (b) An example: x = 2.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 22
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
N Graph GA N
T T
(k = 3)
F F
x0 x0
Binary decoder
x1 x1
x2 a0 a1 ax a7 x2 0 2 7
b0 b1 edge if (x,y) ∉ A no edge
c0 c1 cy c7 0 3 7
y0 y0
y1 y1
Binary decoder
y2 y2
(a) (b)
Figure 7: (a) The high-level structure of graph GA . (b) An example: (x, y) = (2, 3) ∈ A.
and w(i, j) must have the same color as w(i + 1, j).
Given two sets A, B ⊆ I × I, we construct a graph G = GA,B that consists of subgraphs GA and G0B that
are connected to each other by 2k + 1 wires; see Figure 9. The wires ensure that GA and G0B agree on the
coloring of the terminals.
In more detail, we label the 2k + 1 wires with wT , wx1 , wx2 , . . . , wxk , and wy1 , wy2 , . . . , wyk . The endpoints
of the wires are identified with the nodes of the subgraphs GA and G0B as follows:
w(1, 1) = N and w(3r, 1) = N 0 for each wire w,
0
wT (1, 2) = T and wT (3r, 2) = T ,
wxi (1, 2) = xi and wxi (3r, 2) = xi0 for each i = 0, 1, . . . , k − 1,
wyi (1, 2) = yi and wyi (3r, 2) = y0i for each i = 0, 1, . . . , k − 1.
Analysis. We make the following observations of G:
(i) The total number of nodes in G is n = Θ(2k ).
(ii) Let W ⊆ V (G) consist of the nodes that are not in GA or G0B ; these are internal nodes of the wires.
The number of nodes in W is Θ(rk) = Θ(r log n).
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 23
M IKA G Ö ÖS AND J UKKA S UOMELA
N N’ N N’
a a’ a a’
= =
N N’ N N’
… …
a a’ a a’
(a) (b)
Figure 8: (a) A wire between terminals a and a0 . (b) An example of a proper 3-coloring.
GA,B (k = 3)
GA N N’ G’B
wire
T T’
F F’
x0 x’0
x1 x’1
x2 x’2
y0 y’0
y1 y’1
y2 y’2
Figure 9: Graph GA,B consists of graphs GA and G0B that are connected by 2k + 1 wires.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 24
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
(iii) The shortest path from a node of GA to a node of G0B has length at least 3r − 1. In particular, for
sufficiently large r, the local neighborhood of any node is a subset of W ∪V (GA ) or a subset of
W ∪V (G0B ).
Moreover, 3-colorings of G have the following properties:
(iv) Nodes N and N 0 have the same color, nodes T and T 0 have the same color, and nodes F and F 0
have the same color. Hence the concepts of true, false, and neutral nodes are well-defined in G.
(v) Nodes xi and xi0 have the same color for each i, and nodes yi and y0i have the same color for each
i. In particular, both GA and G0B agree on the encoding of the same pair (x, y), and we must have
(x, y) ∈ A ∩ B.
It follows that GA,B has a 3-coloring if and only if A ∩ B 6= 0./
Let A ⊆ I × I and let Ā be its complement. Now A ∩ Ā = 0/ and GA,Ā does not have a 3-coloring; hence
it is in P. If we had locally checkable proofs of size o(n2 / log n), the total number of proof bits in W
would be o(rn2 ); on the other hand, there are Θ(n2 ) elements in I × I. Hence for sufficiently large n there
are two different sets A, B ⊆ I × I such that we have the same proof bits in W for both GA,Ā and GB,B̄ .
Now we are ready to apply a fooling set argument. As A 6= B, we have A ∩ B̄ 6= 0/ or Ā ∩ B 6= 0/ (or
both). Without loss of generality, assume that A ∩ B̄ 6= 0. / Hence GA,B̄ admits a 3-coloring, and it is
therefore not in P. But we can construct a proof as follows: the proof bits of GA are inherited from the
proof of GA,Ā , the proof bits of G0B̄ are inherited from the proof of GB,B̄ , and the proof bits of wires are
the same as in GA,Ā and GB,B̄ . Hence each node of GA,B̄ has a local neighborhood that looks identical to a
node of GA,Ā or GB,B̄ . As GA,Ā and GB,B̄ are yes-instances, all nodes will accept GA,B̄ , a contradiction.
This completes the proof of Theorem 6.4 that non-3-colorability requires proofs of size Ω(n2 / log n).
For comparison, proofs of size O(n2 ) are trivially sufficient.
7 Structural properties
In the previous sections we have discussed concrete examples of graph properties and their local proof
complexities. By contrast, the focus of this final section is on the structural properties of the LCP
hierarchy: We study the sensitivity of our LCP model to the definitional choices made in Section 2. In
a similar vein, we will seek alternative characterizations of the class LogLCP. Finally, we give some
observations relating our LCP classes to other complexity classes.
7.1 Port numbering algorithms
Throughout this paper, we have used the assumption that the local verifier can access the unique identifiers
of the nodes (in accordance with Peleg’s [25] LOCAL model). Furthermore, we have assumed that the
proof can depend on the identifier assignment (recall that this convention is not followed by Fraigniaud et
al. [11]). In this section we ask what one can locally prove in a setting where node identifiers are not
available.
The standard model for computing on networks without unique identifiers is the port numbering
model (PN) of Angluin [3]. In the PN model the nodes are considered anonymous; they do not have
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 25
M IKA G Ö ÖS AND J UKKA S UOMELA
unique identifiers. There is only a port numbering available in the network, i. e., a node of degree d
can refer to its neighbors by integers 1, 2, . . . , d. We refer to Angluin [3] and Suomela [29] for a formal
definition of the PN model.
Recall that if ϕ : V (H) → V (G) is a covering map (i. e., an onto graph homomorphism that for each
v ∈ V (H) maps the neighbors of v in H bijectively onto the neighbors of ϕ(v) in G), then H is said to be
a lift of G [2, 3]. For example, any kn-cycle is a lift of an n-cycle. Furthermore, we say that a property
P ⊆ F is closed under lifts if G ∈ P implies H ∈ P for every lift H ∈ F of G.
A fundamental limitation of a PN algorithm A is that it is fooled by a lift ϕ : V (H) → V (G) in the
following sense [3, 29]: for every local input P : V (G) → {0, 1}? we have that
A(H, P ◦ ϕ, v) = A(G, P, ϕ(v)) for all v ∈ V (H)
for suitable port numberings of H and G. Thus—regardless of the size of P—this directly implies that any
property that can be locally checked using a PN verifier must be closed under lifts: if each node outputs 1
on (G, P), then each node outputs 1 on (H, P ◦ ϕ). In fact, the converse holds on connected graphs:
Theorem 7.1. Suppose that P ⊆ F is a property of connected graphs that is closed under lifts. Then P
admits locally checkable proofs of size O(n2 ) that can be verified using a PN algorithm.
Proof. On input a connected graph H ∈ F, the PN verifier for P expects the proof label P(v) of a
node v ∈ V (H) to encode a pair (G, ϕ(v)), where G is a connected graph (without port numbers) having
identifiers V (G) = {1, . . . , n(G)}, and ϕ(v) ∈ V (G) is a distinguished node. Naturally, an honest O(n2 )-bit
proof will have P(v) = (H, v) for all v.
We let the PN verifier perform the following checks at a node v ∈ V (H). First, we check that all the
neighbors of v hold the same encoding of G in their proof labels. This ensures that all nodes agree on the
encoding of G since the input graph is connected. Then v checks that degH (v) = degG (ϕ(v)) and that
{ϕ(u) : u is a neighbor of v in H } = {u : u is a neighbor of ϕ(v) in G } .
These checks guarantee that the map ϕ : V (H) → V (G) is a covering map. Finally, the PN verifier accepts
iff G ∈ P. The soundness of the checking procedure now follows from the assumption that P is closed
under lifts.
7.2 Alternative characterizations of LogLCP
A LogLCP proof can address individual vertices by their O(log n) identifiers. Consequently—and in
contrast to the discussion above—LogLCP contains properties that are not closed under lifts (e. g., non-
bipartiteness). Next, we show how a little additional input structure can enable a PN verifier to check
properties in LogLCP. This shows that the class LogLCP is robust in the sense that we can change our
underlying model of distributed computation and yet arrive at exactly the same class of graph properties.
We note that the model (3) below is related to the class NLD#n considered by Fraigniaud et al. [11].
Theorem 7.2. On connected graphs G, the class LogLCP coincides with properties that can be locally
verified with O(log n) bits in each of the following models:
1. PN with unique identifiers, i. e., the model used to define LogLCP in Section 2.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 26
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
2. PN with an elected leader in G.
3. PN with each node being given n(G) as input.
Proof. We show that the above models are equivalent by describing how to pass from one model to
another with only an additive O(log n) overhead in proof size.
(1 ⇒ 2 & 3): Using spanning tree methods [18] we already saw in Section 5 that (on a connected
graph) proving the presence of a unique leader and verifying the number of nodes is in LogLCP.
(2 & 3 ⇒ 1): Consider the following attempt at encoding a spanning tree T of G in the PN model: the
O(log n) proof encodes T together with the root-distances. The problem with this encoding is that since
we cannot talk about the identifier of the anonymous root of T , we cannot verify that such an encoding
describes a spanning tree rather than a spanning forest. However, we can overcome this tree/forest
problem by employing either one of the assumptions (2) or (3): Under (2) we can require that the unique
elected leader in G is the root of the spanning tree. Under (3) we can equip T with node counters along
the paths towards the root and thus verify that all n(G) nodes are contained in the same tree. Hence, in
either of the models (2) or (3) we can build and verify a spanning tree T of G.
Using T we can generate unique identifiers for the nodes of G as follows (cf. ancestor labeling
schemes [12]): Do a depth-first traversal on T starting at the root and record in the proof label of a node v
its discovery time x(v) and finishing time y(v); the identifier of a node v is then an encoding of the pair
(x(v), y(v)). We note that the pairs (x(v), y(v)) can be locally checked to be consistent with a depth-first
traversal on T —it follows that the node identifiers are globally unique.
Remark 7.3. Fraigniaud et al. [11] describe how a randomized local verifier can check—in a certain
probabilistic sense—whether a graph contains at most one leader. This technique provides yet another
means to check for the uniqueness of a rooted spanning tree.
7.3 Complementing in LCP(0)
We will now show that coLCP(0) ⊆ LogLCP on connected graphs. The key idea is that we can employ
spanning trees to reverse the decision made by an LCP(0) verifier.
Let F be the family of connected graphs, let P ⊆ F be a graph property in LCP(0), and let P̄ = F \ P
be the complement of P. We will show that P̄ admits a locally checkable proof of size O(log n) in graph
family F.
Let A be a local verifier that checks P; we will use A to design a proof labeling scheme for P̄. For
any yes-instance G ∈ P̄, we construct a locally checkable proof P of size O(log n) as follows: Select
a root node a with A(G, ε, a) = 0, i. e., a is a node that rejects the input G. Then choose an arbitrary
spanning tree T rooted at a. Let P consist of an encoding of (T, a) and a proof of its correctness.
The proof is checked by a local verifier Ā as follows. First, Ā verifies that T is valid spanning tree
rooted at a; in particular, there is a finite path from any v ∈ V (G) to a. Second, at the root node a, verifier
Ā simulates A and checks that A(G, ε, a) = 0.
By construction, a valid proof is accepted by Ā. Let us now show that we cannot fool Ā. Consider a
no-instance G ∈ / P̄ and any proof P. We have one of the following cases:
1. P is not an encoding of a rooted spanning tree. At least one node detects this and the input is
rejected by Ā.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 27
M IKA G Ö ÖS AND J UKKA S UOMELA
2. P is an encoding of a spanning tree T rooted at a. However, G ∈ P and therefore A(G, ε, a) = 1.
Hence Ā outputs 0 at the root node a.
We conclude that for each G ∈ P̄ there is a proof P that is accepted by Ā, and for each G ∈
/ P̄ any proof P
is rejected by Ā. Hence P̄ is in LogLCP.
7.4 Containment in NP and NP/poly
Comparing classes such as LogLCP and NP is not straightforward. To define the LCP hierarchy, we have
used the LOCAL model, which allows unlimited local computation. Hence if we have unbounded node
degrees in G (or unbounded amount of additional information per node in the form of colors or weights),
we can easily come up with artificial problems that are in LCP(0) but not in NP.
However, the situation becomes much more interesting if we study bounded-degree graphs; moreover,
we will consider properties of unlabeled graphs, i. e., there is no additional information besides the node
identifiers and the topology of the graph.
In this restricted case, we can still show that there are problems in LogLCP that are not contained
in NP. Once again, we can resort to spanning tree methods: without loss of generality, we can assume
that a LogLCP verifier has access to n = n(G) in any connected graph G. Hence the verifier can solve
arbitrarily hard problems concerning the integer n, including those that are not in NP (which exist by the
hierarchy theorems [23, §7.2]).
However, if P ∈ LogLCP is a graph property related to unlabeled bounded-degree graphs, we can
show that P is in NP/poly, i. e., NP with a polynomial-size non-uniform advice. In a bounded-degree
graph, the number of nodes inside the local horizon is bounded by a constant, and hence a LogLCP
verifier A uses only O(log n) bits of input in total. Thus verifier A can be encoded as a lookup table of
size 2O(log n) , which is polynomial in n. We can provide the entire lookup table as the advice string S to an
NP/poly machine M. Then M merely guesses the O(n log n)-bit proof P : V (G) → {0, 1}? , and uses the
advice string S to verify the guess.
7.5 Connections to descriptive complexity
A central result in descriptive complexity theory and one that began the field is Fagin’s [9], [14, Ch. 7]
characterization of the class NP as graph properties expressible by existential second-order formulas
(Σ11 )—this is the extension of first-order logic that allows existential quantification over relation symbols
X1 , X2 , . . . (of any arity). Some NP-complete graph properties (e. g., 3-colorability) are even expressible
by monadic Σ11 formulas that only quantify over unary relation symbols [1, 26]. In this section, we
make observations of a connection between the LogLCP class and the class of graph properties that are
expressible by monadic Σ11 formulas.
In the study of first-order expressibility, locality is a thematic subject; this is illustrated by Hanf’s
theorem and the work of Gaifman [14, Ch. 6]. Building on this work, Schwentick and Barthelmann [27]
have shown that on connected graphs, every monadic Σ11 formula is equivalent to a formula of the form
ϑ = ∃X1 ∃X2 . . . ∃Xk ∃x∀y : ϕ(X1 , . . . , Xk , x, y) ,
where ϕ is first-order (using relation symbols X1 , . . . , Xk ) and local around y. Here, a formula ϕ is local
around y if there is a constant r so that for all graphs G and all interpretations of X1 , X2 , . . . , Xk , x, y it
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 28
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
can be determined whether G satisfies φ (X1 , X2 , . . . , Xk , x, y) on the basis of the r-radius neighborhood
of y in G. (More formally, the quantifications in ϕ are always of the form ∃z : (dist(z, y) ≤ r ∧ ψ) or
∀z : (dist(z, y) ≤ r → ψ), where “dist(z, y) ≤ r” simply stands for “the distance between z and y is at
most r”.)
Let us consider the family F of connected graphs. If and only if a graph G ∈ F has property ϑ , there
are unary relations A1 , A2 , . . . , Ak and a node a ∈ V such that G satisfies ∀y : ϕ(A1 , A2 , . . . , Ak , a, y). For
each node v and each relation Ai , encoding Ai (v) takes 1 bit. To prove the existence of the node a, we
can use a spanning tree rooted at a; a locally checkable spanning tree requires O(log n) bits per node
(recall Section 5). To check the proof, the verifier A first checks the spanning tree, and then evaluates
ϕ(A1 , A2 , . . . , Ak , a, y) for each node y. As ϕ is local around y, the verifier A is a local algorithm. Hence
in connected graphs, any monadic Σ11 graph property P admits locally checkable proofs of size O(log n),
i. e., P ∈ LogLCP.
8 Open problems
We conclude by summarizing some open problems raised by our paper. While the local proof complexity
as a function of the number of nodes n is now fairly well understood, we left a small gap in the case of
non-3-colorability, which is probably a proof artifact.
1. Prove that non-3-colorability is not in LCP(o(n2 )).
There are also many open questions related to the local proof complexity as a function of the maximum
degree ∆:
2. In Section 4.1 we saw that directed s–t reachability admits locally checkable proofs of size O(log ∆).
Is there a proof labeling scheme with O(1)-bit proofs?
3. Eulerian tours admit a straightforward proof of size O(∆ log n), and the lower-bound techniques
of Section 5 imply a lower bound of Ω(log n). Is there a proof labeling scheme with O(log n)-bit
proofs?
If we increase the local horizon of a verifier, can we decrease the proof size? Korman et al. [17] show
how this can be done when verifying minimum weight spanning trees. Do such trade-offs exist for all
properties in LCP(O(1)), or not:
4. Do we have LCP(k) ( LCP(k + 1) for all constants k ∈ N?
The analogous question has been answered affirmatively for monadic Σ11 expressibility [22].
Perhaps our most nagging question is one that involves another structural property of the class
LCP(O(1)). Recall that in Section 7.4 it was straightforward to see that LogLCP * NP. The analogous
question for LCP(O(1)) is the following:
5. If P ⊆ F is a graph property in LCP(O(1)) related to connected, unlabeled, bounded-degree graphs,
do we necessarily have P ∈ NP?
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 29
M IKA G Ö ÖS AND J UKKA S UOMELA
It should be noted that in case F is closed under disjoint unions of graphs, a single component C ⊂ G in
a graph G ∈ F can have node identifiers that are not bounded by a polynomial in n(C). In this case, a
modification of the Ramsey argument of Naor and Stockmeyer [21, §3] applies to get rid of the identifier
dependencies and proves P ∈ NP.
Acknowledgments
We thank the anonymous reviewers for their helpful comments and suggestions. This work was supported
in part by the Academy of Finland, Grants 132380 and 252018, the Finnish Cultural Foundation, and the
Research Funds of the University of Helsinki. Most of this work was conducted while the authors were
affiliated with the University of Helsinki.
References
[1] M IKLÓS A JTAI AND RONALD FAGIN: Reachability is harder for directed than for undirected finite
graphs. J. Symbolic Logic, 55(1):113–150, 1990. Preliminary version in FOCS’88. JSTOR. 9, 28
[2] A LON A MIT, NATHAN L INIAL , J I ŘÍ M ATOUŠEK , AND E YAL ROZENMAN: Random lifts of graphs.
In Proc. 12th Ann. ACM-SIAM Symp. on Discrete Algorithms (SODA’01), pp. 883–894. ACM Press,
2001. Abstract based on papers in Combinatorica ’02, Combinatorics, Probability and Computing
’06, Random Struct. Algorithms ’02, and Combinatorica ’05. [ACM:365801] 26
[3] DANA A NGLUIN: Local and global properties in networks of processors. In Proc. 12th STOC, pp.
82–93. ACM Press, 1980. [doi:10.1145/800141.804655] 25, 26
[4] M ATTI Å STRAND AND J UKKA S UOMELA: Fast distributed approximation algorithms for
vertex cover and set cover in anonymous networks. In Proc. 22nd Ann. ACM Symp. on
Parallelism in Algorithms and Architectures (SPAA’10), pp. 294–302. ACM Press, 2010.
[doi:10.1145/1810479.1810533] 7
[5] L OWELL W. B EINEKE: Characterizations of derived graphs. J. Combinatorial Theory, 9(2):129–
135, 1970. [doi:10.1016/S0021-9800(70)80019-9] 2
[6] J OHN A. B ONDY AND M IKLÓS S IMONOVITS: Cycles of even length in graphs. J. Combin. Theory
Ser. B, 16(2):97–105, 1974. [doi:10.1016/0095-8956(74)90052-5] 8, 12, 15
[7] R EINHARD D IESTEL: Graph Theory. Springer, Berlin, Germany, 3rd edition, 2005. Official
website. 10, 18
[8] PAUL E RD ŐS AND A LFRÉD R ÉNYI: Asymmetric graphs. Acta Mathematica Hungarica, 14(3-
4):295–315, 1963. [doi:10.1007/BF01895716] 18
[9] RONALD FAGIN: Generalized first-order spectra and polynomial-time recognizable sets. In R. M.
K ARP, editor, Complexity of Computation, volume 7, pp. 43–73. ams, 1974. Available at author’s
home page. 28
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 30
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
[10] P IERRE F RAIGNIAUD: Distributed computational complexities: are you Volvo-addicted or
NASCAR-obsessed? In Proc. 29th Ann. ACM Symp. on Principles of Distributed Computing
(PODC’10), pp. 171–172. ACM Press, 2010. [doi:10.1145/1835698.1835700] 2
[11] P IERRE F RAIGNIAUD , A MOS KORMAN , AND DAVID P ELEG: Local distributed decision. In Proc.
52nd FOCS, pp. 708–717. IEEE Comp. Soc. Press, 2011. To appear in J. ACM. J. ACM version
available at author’s home page. [doi:10.1109/FOCS.2011.17] 3, 5, 8, 9, 25, 26, 27
[12] C YRIL G AVOILLE AND DAVID P ELEG: Compact and localized distributed data structures. Dis-
tributed Computing, 16(2-3):111–120, 2003. [doi:10.1007/s00446-002-0073-5] 8, 27
[13] M IKA G ÖÖS AND J UKKA S UOMELA: Locally checkable proofs. In Proc. 30th Ann. ACM
Symp. on Principles of Distributed Computing (PODC’11), pp. 159–168. ACM Press, 2011.
[doi:10.1145/1993806.1993829] 1
[14] N EIL I MMERMAN: Descriptive Complexity. Graduate Texts in Computer Science. Springer, Berlin,
Germany, 1999. 9, 28
[15] A MOS KORMAN AND S HAY K UTTEN: On distributed verification. In Proc. 8th Internat.
Conf. on Distributed Computing and Networking (ICDN’06), pp. 100–114. Springer, 2006.
[doi:10.1007/11947950_12] 2, 3, 8
[16] A MOS KORMAN AND S HAY K UTTEN: Distributed verification of minimum spanning trees. Dis-
tributed Computing, 20(4):253–266, 2007. Preliminary version in PODC’06. [doi:10.1007/s00446-
007-0025-1] 2, 3, 8
[17] A MOS KORMAN , S HAY K UTTEN , AND T OSHIMITSU M ASUZAWA: Fast and compact self stabi-
lizing verification, computation, and fault detection of an MST. In Proc. 24th Ann. ACM Symp.
on Principles of Distributed Computing (PODC’05), pp. 311–320, 2011. To appear in Distributed
Computing. [doi:10.1145/1993806.1993866] 29
[18] A MOS KORMAN , S HAY K UTTEN , AND DAVID P ELEG: Proof labeling schemes. Distributed
Computing, 22(4):215–233, 2010. Preliminary version in PODC’05. [doi:10.1007/s00446-010-
0095-3] 2, 3, 5, 8, 10, 11, 12, 18, 27
[19] A MOS KORMAN , DAVID P ELEG , AND YOAV RODEH: Constructing labeling schemes through
universal matrices. Algorithmica, 57(4):641–652, 2010. Preliminary version in ISAAC’06.
[doi:10.1007/s00453-008-9226-7] 2, 3, 8
[20] E YAL K USHILEVITZ AND N OAM N ISAN: Communication Complexity. Cambridge Univ. Press,
Cambridge, UK, 1997. [ACM:264772] 19
[21] M ONI NAOR AND L ARRY J. S TOCKMEYER: What can be computed locally? SIAM J. Comput.,
24(6):1259–1277, 1995. Preliminary version in STOC’93. [doi:10.1137/S0097539793254571] 2, 5,
7, 30
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 31
M IKA G Ö ÖS AND J UKKA S UOMELA
[22] M ARTIN OTTO: A note on the number of monadic quantifiers in monadic Σ11 . Inform. Process. Lett.,
53(6):337–339, 1995. [doi:10.1016/0020-0190(94)00219-O] 29
[23] C HRISTOS H. PAPADIMITRIOU: Computational Complexity. Addison-Wesley Publishing Company,
1994. 28
[24] C HRISTOS H. PAPADIMITRIOU AND K ENNETH S TEIGLITZ: Combinatorial Optimization: Al-
gorithms and Complexity. Dover Publications, Inc., Mineola, NY, USA, 1998. [ACM:31027]
11
[25] DAVID P ELEG: Distributed Computing: A Locality-Sensitive Approach. Volume 5 of SIAM
Monographs on Discrete Mathematics and Applications. SIAM, 2000. [ACM:355459] 6, 25
[26] T HOMAS S CHWENTICK: On winning Ehrenfeucht games and monadic NP. Ann. Pure Appl. Logic,
79(1):61–92, 1996. Preliminary version in FOCS’94. [doi:10.1016/0168-0072(95)00030-5] 28
[27] T HOMAS S CHWENTICK AND K LAUS BARTHELMANN: Local normal forms for first-order logic
with applications to games and automata. Discrete Mathematics and Theoretical Computer Science,
3(3):109–124, 1999. Preliminary version in STACS’98. DMTCS. 28
[28] N EIL J. A. S LOANE: The On-Line Encyclopedia of Integer Sequences, 2010. http://oeis.org.
18
[29] J UKKA S UOMELA: Survey of local algorithms. ACM Computing Surveys, 45(2):24, 2013.
[doi:10.1145/2431211.2431223] 2, 26
AUTHORS
Mika Göös
Postdoctoral fellow
Harvard University
Cambridge, MA
mika seas harvard edu
http://www.cs.utoronto.ca/~mgoos/
Jukka Suomela
Assistant professor
Helsinki Institute for Information Technology HIIT
Department of Computer Science
Aalto University, Finland
jukka suomela aalto fi
http://users.ics.aalto.fi/suomela/
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 32
L OCALLY C HECKABLE P ROOFS IN D ISTRIBUTED C OMPUTING
ABOUT THE AUTHORS
M IKA G ÖÖS is a postdoctoral fellow at the Theory of Computing group at Harvard. He
obtained his Ph. D. from the University of Toronto (2016) under the supervision of
Toniann Pitassi. He also holds a M. S. from University of Oxford (2011) and a B. S. from
Aalto University (2010). His research interests revolve around computational complexity
theory.
J UKKA S UOMELA is an assistant professor in the Department of Computer Science at Aalto
University. He received his Ph. D. from the University of Helsinki in 2009, and the
title of Docent in Computer Science in 2012. Suomela’s research group conducts basic
research related to the theoretical foundations of distributed computing, with particular
emphasis on the concept of locality in the context of distributed graph algorithms.
T HEORY OF C OMPUTING, Volume 12 (19), 2016, pp. 1–33 33