Locally Checkable Graph Properties

Locally Checkable Graph Properties Oliver Bachtler and Tim Bergner Department of Mathematics TU Kaiserslautern Future Research in Combinatorial Optimization, 2021 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information My kingdom should be cubic. BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information My kingdom should be cubic. BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Looks good. BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information This is wrong, notify the king! BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information I also want my kingdom to be bipartite. BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information I also want my kingdom to be bipartite. BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Is this really bipartite? BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Don’t forget your orders! BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Order has been established! BA B A B A AB A B A B O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 17 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct (default), or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 4 / 17 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct (default), or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 4 / 17 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct (default), or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 4 / 17 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 5 / 17 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 5 / 17 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 5 / 17 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 5 / 17 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 5 / 17 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 6 / 17 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 6 / 17 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 6 / 17 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 7 / 17 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 7 / 17 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 7 / 17 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 7 / 17 Examples (taken from Göös, Suomela 2016) O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 8 / 17 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 9 / 17 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 9 / 17 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 9 / 17 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 9 / 17 More Examples: Connectivity Definition (st-Connectivity) In the directed st-connectivity problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 11 / 17 More Examples: Connectivity Definition (st-Connectivity) In the directed st-connectivity problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 11 / 17 More Examples: Connectivity Definition (st-Connectivity) In the directed st-connectivity problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 11 / 17 More Examples: Connectivity Example (st-Connectivity) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-connectivity. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 12 / 17 More Examples: Connectivity Example (st-Connectivity) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-connectivity. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 12 / 17 More Examples: Connectivity Example (st-Connectivity) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-connectivity. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 12 / 17 More Examples: Connectivity Example (st-Connectivity) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-connectivity. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 12 / 17 More Examples: Connectivity Example (st-Connectivity) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-connectivity. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 12 / 17 More Examples: Connectivity Example (Directed st-Connectivity) ▶Use proof to specify a shortest path: prover assigns each vertex on a fixed shortest path a pointer to its successor. ▶The verifier at vchecks that if vhas a pointer, then one of its predecessors points to it (unless v=sor v=t). ▶Accepts exactly the directed graphs where tis reachable from s. ⇒A proof labelling scheme of size log(n)exists for dir. st-connectivity. t s 1 1 1 1 1 0 0 0 1 1 1 s ε ε ε εε s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 13 / 17 More Examples: Connectivity Example (Directed st-Connectivity) ▶Use proof to specify a shortest path: prover assigns each vertex on a fixed shortest path a pointer to its successor. ▶The verifier at vchecks that if vhas a pointer, then one of its predecessors points to it (unless v=sor v=t). ▶Accepts exactly the directed graphs where tis reachable from s. ⇒A proof labelling scheme of size log(n)exists for dir. st-connectivity. t s 1 1 1 1 1 0 0 0 1 1 1 s ε ε ε εε s O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 13 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Directed is Harder Than Undirected Connectivity Goal: we want to prove that Theorem No constant-size proof labelling scheme exists for directed st-connectivity on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 15 / 17 Proof Sketch Goal: iteratively forbid more and more pairs forbidden st O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 16 / 17 Proof Sketch Want: same coloured forward-edges connected by back-edges and forbidden st O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 16 / 17 Proof Sketch How: use the Pigeon Hole Principle st O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 16 / 17 Proof Sketch Result: pair forbidden in all grey areas st O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 16 / 17 Proof Sketch Now: plug in recursively to forbid more pairs st O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 16 / 17 Summary We have: ▶formally defined proof labelling schemes, ▶illustrated these on several examples, and ▶showed that small proofs are insufficient for directed st-connectivity. What now? ▶Show that small proofs do not suffice for more powerful verifiers. ▶Determine the optimal proof sizes for other problems. Contact: [email protected] O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 17 / 17 Summary We have: ▶formally defined proof labelling schemes, ▶illustrated these on several examples, and ▶showed that small proofs are insufficient for directed st-connectivity. What now? ▶Show that small proofs do not suffice for more powerful verifiers. ▶Determine the optimal proof sizes for other problems. Contact: [email protected] O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 17 / 17 References Laurent Feuilloley. Introduction to local certification, 2020. Mika Göös and Jukka Suomela. Locally checkable proofs in distributed computing. Theory of Computing, 12(19):1–33, 2016. A. Korman, S. Kutten, and D. Peleg. Proof labeling schemes. Distributed Computing, 22:215–233, 2010. O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 1 / 2 Almost all Other Examples Example (Universal Proof Labelling Scheme) ▶Assume we can decide for a graph G∈ G whether G∈ F. ▶Use proof to specify the graph: prover assigns the adjacency matrix A and the corresponding row to each vertex. ▶The verifier at vchecks that its neighbourhood is correct and that the graph given by Ais in F. ▶Accepts exactly the graphs in F. ⇒There exists a universal proof labelling scheme of size O(n2). A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 2 / 2 Almost all Other Examples Example (Universal Proof Labelling Scheme) ▶Assume we can decide for a graph G∈ G whether G∈ F. ▶Use proof to specify the graph: prover assigns the adjacency matrix A and the corresponding row to each vertex. ▶The verifier at vchecks that its neighbourhood is correct and that the graph given by Ais in F. ▶Accepts exactly the graphs in F. ⇒There exists a universal proof labelling scheme of size O(n2). A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 O. Bachtler and T. Bergner (TUK) Local Verification FRICO 2021 2 / 2