Brief Announcement: Deciding FO Formulas Efficiently in Congested Networks

We establish that for every first-order logic (FO) formula φ, which captures a vast number of computational problems on graphs, and every graph class G of bounded expansion, there exists a deterministic distributed algorithm that, for any n-node graph G- G with diameter D, determines whether Gφ within O(D+log n) rounds in the standard CONGEST model. Graph classes of bounded expansion encompass many well-known families of sparse graphs, including planar graphs, bounded-genus graphs, bounded-treedepth graphs, bounded-treewidth graphs, bounded-degree graphs, graphs that exclude a fixed graph H as a minor or topological minor, random graphs with constant average degree (a.a.s.), and many network models (e.g., stochastic block models) for some ranges of parameters.Our algorithmic meta-theorem is "tight"in several ways. First, the bound on the number of rounds, up to a logarithmic additive term, is optimal, as even a simple FO formula such as "there are two vertices of degree 3"requires ω(D) rounds in CONGEST even in trees. Second, deciding FO formulas requires significantly more rounds for more general classes of sparse graphs. In particular, we show that even the simple FO formula expressing C6-freeness requires [EQUATION] rounds to be checked in graphs of degeneracy 2 with constant diameter. Finally, our theorem cannot be extended to monadic second order logic (MSO). For instance, we prove that checking non-3-colorability requires [EQUATION] rounds in bounded-degree graphs with logarithmic diameter.Besides establishing the first generic result on the tractability of FO over a large class of sparse graphs, our meta-theorem and the techniques developed to prove it yield several important consequences. We demonstrate how to extend our algorithmic metatheorem to various distributed optimization, counting, and certification problems.