research-article

Locally checkable proofs

Authors:

Jukka SuomelaAuthors Info & Claims

PODC '11: Proceedings of the 30th annual ACM SIGACT-SIGOPS symposium on Principles of distributed computing

Pages 159 - 168

https://doi.org/10.1145/1993806.1993829

Published: 06 June 2011 Publication History

Abstract

This work studies decision problems 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-colouring 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 work we classify graph problems 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 proof complexities form a natural hierarchy of complexity classes: for many classical graph problems, the proof complexity is either 0, (1), (log n), or poly(n) bits per node. Among the most difficult graph properties are symmetric graphs, which require ©(n²) bits per node, and non-3-colourable graphs, which require ©(n²/log n) bits per node - any pure graph property admits a trivial proof of size O(n²).

References

[1]

Miklos Ajtai and Ronald Fagin. Reachability is harder for directed than for undirected finite graphs. The Journal of Symbolic Logic, 55(1):113--150, 1990.

[2]

Dana Angluin. Local and global properties in networks of processors. In Proc. 12th Symposium on Theory of Computing (STOC 1980), pages 82--93. ACM Press, 1980.

Digital Library

[3]

Lowell W. Beineke. Characterizations of derived graphs. Journal of Combinatorial Theory, 9(2):129--135, 1970.

[4]

John A. Bondy and Miklós Simonovits. Cycles of even length in graphs. Journal of Combinatorial Theory, Series B, 16(2):97--105, 1974.

[5]

http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/Reinhard Diestel. Graph Theory. Springer, 3rd edition, 2005.

[6]

Paul Erdos and Alfréd Rényi. Asymmetric graphs. Acta Mathematica Hungarica, 14:295--315, 1963.

[7]

Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In R. Karp, editor, Complexity of Computation, volume 7, pages 43--73. 1974.

[8]

Pierre Fraigniaud. Distributed computational complexities: are you Volvo-addicted or NASCAR-obsessed? In Proc. 29th Symposium on Principles of Distributed Computing (PODC 2010), pages 171--172. ACM Press, 2010.

Digital Library

[9]

Pierre Fraigniaud, Cyril Gavoille, David Ilcinkas, and Andrzej Pelc. Distributed computing with advice: Information sensitivity of graph coloring. In Proc. 34th International Colloquium on Automata, Languages and Programming (ICALP 2007), volume 4596 of LNCS, pages 231--242. Springer, 2007.

Digital Library

[10]

Pierre Fraigniaud, Amos Korman, and David Peleg. Local distributed decision, 2010. Manuscript, arXiv:1011.2152 {cs.DC}.

[11]

Cyril Gavoille and David Peleg. Compact and localized distributed data structures. Distributed Computing, 16(2-3):111--120, 2003.

Digital Library

[12]

http://www.iki.fi/jukka.suomela/lcpMika Göös and Jukka Suomela. Locally checkable proofs. http://www.iki.fi/jukka.suomela/lcp, 2011. Manuscript.

[13]

Neil Immerman. Descriptive Complexity. Springer, 1999.

[14]

Amos Korman and Shay Kutten. On distributed verification. In Proc. 8th International Conference on Distributed Computing and Networking (ICDCN 2006), volume 4308 of LNCS, pages 100--114. Springer, 2006.

Digital Library

[15]

Amos Korman and Shay Kutten. Distributed verification of minimum spanning trees. Distributed Computing, 20(4):253--266, 2007.

Digital Library

[16]

Amos Korman, Shay Kutten, and David Peleg. Proof labeling schemes. In Proc. 24th Symposium on Principles of Distributed Computing (PODC 2005), pages 9--18. ACM Press, 2005.

Digital Library

[17]

Amos Korman, David Peleg, and Yoav Rodeh. Constructing labeling schemes through universal matrices. Algorithmica, 57(4):641--652, 2010.

Digital Library

[18]

Moni Naor and Larry Stockmeyer. What can be computed locally? SIAM Journal on Computing, 24(6):1259--1277, 1995.

Digital Library

[19]

David Peleg. Distributed Computing -- A Locality-Sensitive Approach. SIAM, 2000.

Digital Library

[20]

Thomas Schwentick. Graph connectivity and monadic NP. In Proc. 35th Symposium on Foundations of Computer Science (FOCS 1994), pages 614--622. IEEE, 1994.

Digital Library

[21]

Thomas Schwentick and Klaus Barthelmann. Local normal forms for first-order logic with applications to games and automata. Discrete Mathematics and Theoretical Computer Science, 3:109--124, 1999.

Digital Library

[22]

http://oeis.orgN. J. A. Sloane. The on-line encyclopedia of integer sequences. http://oeis.org, 2010.

[23]

http://www.iki.fi/jukka.suomela/local-surveyJukka Suomela. Survey of local algorithms. http://www.iki.fi/jukka.suomela/local-survey, 2011. Manuscript submitted for publication.

Cited By

Balliu AHirvonen JMelnyk DOlivetti DRybicki JSuomela J(2022)Local MendingStructural Information and Communication Complexity10.1007/978-3-031-09993-9_1(1-20)Online publication date: 25-Jun-2022
https://doi.org/10.1007/978-3-031-09993-9_1
Shimi A(2019)The Splendors and Miseries of RoundsACM SIGACT News10.1145/3364626.336463550:3(35-50)Online publication date: 24-Sep-2019
https://dl.acm.org/doi/10.1145/3364626.3364635
Arfaoui HFraigniaud PIlcinkas DMathieu FPelc A(2019)Deciding and verifying network properties locally with few output bitsDistributed Computing10.1007/s00446-019-00355-1Online publication date: 13-Jun-2019
https://doi.org/10.1007/s00446-019-00355-1
Show More Cited By

Index Terms

Locally checkable proofs

Recommendations

Quasipolynomial size proofs of the propositional pigeonhole principle

Cook and Reckhow proved in 1979 that the propositional pigeonhole principle has polynomial size extended Frege proofs. Buss proved in 1987 that it also has polynomial size Frege proofs; these Frege proofs used a completely different proof method based ...
Non-automatizability of bounded-depth frege proofs

In this paper, we show how to extend the argument due to Bonet, Pitassi and Raz to show that bounded-depth Frege proofs do not have feasible interpolation, assuming that factoring of Blum integers or computing the Diffie-Hellman function is sufficiently ...
Verifying proofs in constant depth

In this paper we initiate the study of proof systems where verification of proofs proceeds by NC⁰ circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PODC '11: Proceedings of the 30th annual ACM SIGACT-SIGOPS symposium on Principles of distributed computing

June 2011

406 pages

ISBN:9781450307192

DOI:10.1145/1993806

General Chair:
Cyril Gavoille
LaBRI, University of Bordeaux, France
,
Program Chair:
Pierre Fraigniaud
CNRS and University of Paris Diderot, France

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PODC '11

Sponsor:

PODC '11: ACM Symposium on Principles of Distributed Computing

June 6 - 8, 2011

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
270
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)2

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Balliu AHirvonen JMelnyk DOlivetti DRybicki JSuomela J(2022)Local MendingStructural Information and Communication Complexity10.1007/978-3-031-09993-9_1(1-20)Online publication date: 25-Jun-2022
https://doi.org/10.1007/978-3-031-09993-9_1
Shimi A(2019)The Splendors and Miseries of RoundsACM SIGACT News10.1145/3364626.336463550:3(35-50)Online publication date: 24-Sep-2019
https://dl.acm.org/doi/10.1145/3364626.3364635
Arfaoui HFraigniaud PIlcinkas DMathieu FPelc A(2019)Deciding and verifying network properties locally with few output bitsDistributed Computing10.1007/s00446-019-00355-1Online publication date: 13-Jun-2019
https://doi.org/10.1007/s00446-019-00355-1
Cygan MKratsch SNederlof J(2018)Fast Hamiltonicity Checking Via Bases of Perfect MatchingsJournal of the ACM10.1145/314822765:3(1-46)Online publication date: 13-Mar-2018
https://dl.acm.org/doi/10.1145/3148227
Foerster KRichter OSeidel JWattenhofer R(2017)Local Checkability in Dynamic NetworksProceedings of the 18th International Conference on Distributed Computing and Networking10.1145/3007748.3007779(1-10)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1145/3007748.3007779
Fraigniaud PPelc A(2017)Decidability classes for mobile agents computingJournal of Parallel and Distributed Computing10.1016/j.jpdc.2017.04.003109:C(117-128)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1016/j.jpdc.2017.04.003
Ostrovsky RPerry MRosenbaum W(2017)Space-Time Tradeoffs for Distributed VerificationStructural Information and Communication Complexity10.1007/978-3-319-72050-0_4(53-70)Online publication date: 30-Dec-2017
https://doi.org/10.1007/978-3-319-72050-0_4
Patt-Shamir BPerry M(2017)Proof-Labeling Schemes: Broadcast, Unicast and in BetweenStabilization, Safety, and Security of Distributed Systems10.1007/978-3-319-69084-1_1(1-17)Online publication date: 7-Oct-2017
https://doi.org/10.1007/978-3-319-69084-1_1
Björklund AKaski PGiakkoupis G(2016)How Proofs are Prepared at CamelotProceedings of the 2016 ACM Symposium on Principles of Distributed Computing10.1145/2933057.2933101(391-400)Online publication date: 25-Jul-2016
https://dl.acm.org/doi/10.1145/2933057.2933101
Baruch MOstrovsky RRosenbaum WGiakkoupis G(2016)Brief AnnouncementProceedings of the 2016 ACM Symposium on Principles of Distributed Computing10.1145/2933057.2933071(357-359)Online publication date: 25-Jul-2016
https://dl.acm.org/doi/10.1145/2933057.2933071
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten