Brief Announcement: Deciding FO Formulas Efficiently in Congested Networks

Fomin, FV; Fraigniaud P.; Golovach P.A.; Montealegre P.; Rapaport I.; Todinca I.

Keywords: logic, model checking, distributed computing, sparse graphs, Bounded expansion, Distributed decision, CONGEST model

Abstract

We establish that for every first-order logic (FO) formula phi, 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 is an element of G with diameter D, determines whether G satisfies phi 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 Omega(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 C-6-freeness requires Omega(root n) 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 Omega(n) 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.

Más información

Título según WOS: Brief Announcement: Deciding FO Formulas Efficiently in Congested Networks
Fecha de publicación: 2025
Página de inicio: 310
Página final: 313
Idioma: English
DOI:

10.1145/3732772.3733507

Notas: ISI