BUKA

Project summary

The combination of methods from logic and graph theory has been extremely successful in the design of algorithms, in complexity theory, and other areas of theoretical computer science. A success story exemplifying the power of this approach is the recent development in the algorithmic structure theory of sparse graphs. In this line of research, structural results stemming from Robertson and Seymour’s graph minor theory, and the more recent sparsity theory of Nešetřil and Ossona de Mendez, were combined with logical methods, yielding a systematic understanding of tractability. An example result in this area states that every graph property definable in first order logic can be decided in linear time on planar graphs. In a landmark result, Grohe, Kreutzer, and Siebertz generalized this to all nowhere dense graph classes. Those are very general classes of sparse graphs, which include the class of planar graphs, classes of bounded maximum degree, and classes excluding a fixed minor. This result completely delimits the tractability frontier for sparse graph classes. However, many classes are tractable, but not sparse. The theory of twin-width, which draws on deep connections between logic and enumerative combinatorics, achieves an analog of the result of Grohe et al. for all ordered graphs. Thus, algorithmic tractability is understood in two contexts: for sparse graphs, and for ordered graphs; very recently, also orderless graph classes (see below).

This project sets out to combine sparsity theory and twin-width theory into a unified theory of structural tractability. One of the main goals is to characterize all hereditary graph classes which are tractable with respect to the model checking problem. This requires developing a systematic understanding of the logical structure underlying algorithmic tractability. The tools that will be applied and developed originate in graph structure theory, finite model theory, and stability theory, one of the most successful areas in logic recently. The expected results will be of foundational nature, and of interest primarily to theoretical computer scientists, graph theorists, and logicians.

More details

The area of the project lies at the interface of structural graph theory, algorithmic and finite model theory, and model theory. 

Its goal is to systematically explore the (fixed-parameter) tractability of the model checking problem for first-order logic for restricted classes of graphs. On the one hand, this topic is closely related to concepts studied in structural graph theory – such as classes of bounded treewidth, cliquewidth, twin-width, or nowhere dense classes – and in combinatorics – such as the Erdős-Hajnal property, χ-boundedness, VC-dimension, regularity, or the Marcus-Tardos theorem.

On the other hand, it is closely related to concepts studied in model theory – such as monadically stable and NIP theories – and in finite model theory – such as locality of first-order logic and query enumeration in database theory. The project will seek efficient algorithms leveraging the structure of the considered graphs or structures.

One of the main goals of the project is to characterize those hereditary graph classes, for which the model checking problem for first-order logic is fixed-parameter tractable. This goal has been achieved in restricted settings:

1. in the setting of monotone graph classes, by the result of Grohe, Kreutzer and Siebertz, building on Sparsity theory of Nešetřil and Ossona de Mendez,

2. in the setting of classes of ordered graphs, by the result of Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé, Toruńczyk, building on twin-width developed by Bonnet, Thomassé, and coauthors,

3. in the setting of edge-stable (or orderless) graph classes, by the result of Dreier, Eleftheriadis, Mählmann, McCarty, Pilipczuk, Toruńczyk, building on ideas from Stability theory developed by Shelah.

Related literature

1. Dreier, Eleftheriadis, Mählmann, McCarty, Pilipczuk, Toruńczyk. First-Order Model Checking on Monadically Stable Graph Classes. 2023, arXiv.

2. Dreier, Mählmann, Siebertz, Toruńczyk. Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes. ICALP 2023.

3. Gajarský, Mählmann, McCarty, Ohlmann, Pilipczuk, Przybyszewski, Siebertz, Sokołowski, Toruńczyk. Flipper Games for Monadically Stable Graph Classes. ICALP 2023.

4. Toruńczyk. Flip-width: Cops and Robber on dense graphs. FOCS 2023.

5. Dreier, Mählmann, Siebertz. First-Order Model Checking on Structurally Sparse Graph Classes. STOC 2023.

6. Gajarský, Pilipczuk, Przybyszewski, Toruńczyk. Twin-Width and Types. ICALP 2022.

7. Bonnet, Dreier, Gajarský, Kreutzer, Mählmann, Simon, Toruńczyk Model Checking on Interpretations of Classes of Bounded Local Cliquewidth. LICS 2022.

8. Braunfeld, Laskowski. Existential characterizations of monadic NIP. 2022, arXiv.

9. Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé, Toruńczyk. Twin-width IV: ordered graphs and matrices. STOC 2022.

10. Bonnet, Kim, Thomassé, Watrigant. Twin-width I: Tractable FO Model Checking. FOCS 2020.

11. Grohe, Kreutzer, Siebertz. Deciding First-Order Properties of Nowhere Dense Graphs. STOC 2014.

People involved

 The currently planned team composition is as follows:

• Szymon Toruńczyk (principal investigator)

• Marcin Pilipczuk (team member)

• Postdoc 1

• Postdoc 2

• PhD student 1

• PhD student 2

Apply to the project here !

Some of our collaborators on topics closely related to the project include:

• Édouard Bonnet

• Jan Dreier

• Ioannis Eleftheriadis

• Jakub Gajarský

• Ugo Giocanti

• Sandra Kiefer

• Stephan Kreutzer

• Nikolas Mählmann 

• Jaroslav Nešetřil

• Joanna Ochremiak

• Pierre Ohlmann

• Patrice Ossona de Mendez

• Rose McCarty

• Michał Pilipczuk (leader of ERC Starting Grant BOBR with which BUKA will collaborate)

• Sebastian Siebertz

• Pierre Simon

• Marek Sokołowski

• Giannos Stamoulis

• Stéphan Thomassé

• Wojciech Przybyszewski