LogAlg 2023

  9:30 - 11:00 Tutorial of Jan Dreier

11:00 - 11:30 Coffee break

11:30 - 12:30 Contributed talks:

• Samuel Braunfeld, Characterizations of monadic NIP

• Nikolas Mählmann, Flip-Breakability: Combinatorial Characterizations of Monadically NIP Graph Classes

• Szymon Toruńczyk, Flip-width: Cops and Robber on Dense Graphs

12:30 - 14:00 Lunch break

14:00 - 15:00 Invited talk of Martin Grohe

15:00 - 15:30 Coffee break

15:30 - 16:30 Open problem session

19:00 - 22:00 Workshop dinner (Kuźnia Smaku)

  9:30 - 11:00 Tutorial of Mikołaj Bojańczyk

11:00 - 11:30 Coffee break

11:30 - 12:30 Contributed talks:

• Tomáš Jakl, Game comonads - a new kid in the finite model theory playground

• Sang-il Oum, Survey on vertex-minor obstructions and related parameters of graphs

• Wojciech Przybyszewski, Canonical decompositions in bounded treedepth and bounded shrubdepth graphs

12:30 - 14:00 Lunch break

14:00 - 15:00 Contributed talks:

• Giannos Stamoulis, Elementary first-order model checking for sparse graphs

• Daniel Mock, Solving a family of multivariate optimization and decision problems on classes of bounded expansion

• Robert Ganian, Approximate Evaluation of Quantitative Second Order Queries

15:00 - 15:30 Coffee break

15:30 - 16:30 Contributed talks:

• Sandra Kiefer, A Study of Weisfeiler–Leman Colorings on Planar Graphs

• Moritz Lichter, Symmetric Choice and the Quest for a Logic Capturing Polynomial Time

• Tim Seppelt, Homomorphism Tensors and Graph Isomorphism Relaxations

  9:30 - 10:30 Invited talk of Dimitrios Thilikos

10:30 - 11:00 Coffee break

11:00 - 12:20 Contributed talks:

• Eun Jung Kim, Directed flow-augmentation and boolean CSPs

• Ugo Giocanti, Structure of quasi-transitive graphs avoiding a minor

• Colin Geniet, Factoring permutations of bounded twin-width

• Viktor Zamaraev, Implicit Representations of Graphs and Randomized Communication

12:20 End of workshop

An MSO transduction is a transformation, which transforms some structure (e.g. a tree or graph) into some other structure. The notion is strong enough to capture interesting transformations (such as computing a spanning tree, or even a treewidth decomposition), but limited enough to be subject to automata techniques. In this tutorial, I will describe MSO transductions, and explained how they can be used to give a uniform picture of connections between automata and logic.

Animated Slides

Monadically stable graph classes are a central milestone in the quest towards a unified theory of graph classes with fpt first-oder model-checking. They generalize nowhere dense graph classes and transductions thereof, but are incomparable to classes of bounded twin-with. In this tutorial, we give an overview of the latest developments surrounding monadically stable graph classes. In particular, we discuss the very recent fpt model-checking algorithm for these classes, and the combinatorial tools and techniques leading up to it.

Slides

Graph neural networks (GNNs) are deep learning models for graph data that play a key role in machine learning on graphs. A GNN describes a distributed algorithm carrying out local computations at the vertices of the input graph. Typically, the parameters governing this algorithm are acquired through a data-driven learning process. 

After introducing the basic model, in this talk we will focus on the expressiveness of GNNs: which functions on graphs or their vertices can be computed by GNNs? An intriguing and nontrivial facet of this inquiry is that GNNs are “analog” computation models operating on and with real numbers. Nevertheless, we can give precise characterisations of the expressiveness of GNNs in terms of Boolean circuits and logic, that is, computation models of classical (descriptive) complexity theory.

Slides

The Graph Minors series of Robertson and Seymour, apart from its seminal importance in modern combinatorics, offered a wealth of graph algorithmic techniques. These techniques where mainly developed for the derivation of a cubic-time algorithm for the disjoint paths problem (for fixed number of terminals) and have been extensively used for the design of parametrized graph algorithms. We present a series of meta-algorithmic results that attempt to abstract away these algorithmic techniques and make them automatically applicable to wide families of problems. For this we present distinct certain extensions of First Order Logic. Every problem expressible in such a logic admits a parametrized algorithm on classes of graphs excluding some graph as a (topological) minor.

Slides

The model-theoretic notions of monadic stability and the more general monadic NIP seem to provide the right generalization of the structural and algorithmic properties of nowhere dense graph classes beyond sparse classes. Model-theoretic/combinatorial characterizations of infinite monadically stable structures have long been known, and have recently helped spur spectacular finitary results leading to the tractability of first-order model-checking. We discuss analogous characterizations for infinite monadically NIP structures.

Joint work with Chris Laskowski.

Slides

Courcelle's theorem and its adaptations to cliquewidth have shaped the field of exact parameterized algorithms and are widely considered the archetype of algorithmic meta-theorems. In the past decade, there has been growing interest in developing parameterized approximation algorithms for problems which are not captured by Courcelle's theorem and, in particular, are considered not fixed-parameter tractable under the associated widths.

We develop a generalization of Courcelle's theorem that yields efficient approximation schemes for any problem that can be captured by an expanded logic we call Blocked CMSO, capable of making logical statements about the sizes of set variables via so-called weight comparisons. The logic controls weight comparisons via the quantifier-alternation depth of the involved variables, allowing full comparisons for zero-alternation variables and limited comparisons for one-alternation variables. The developed framework threads the very needle of tractability: on one hand it can describe a broad range of approximable problems, while on the other hand the restrictions of our logic cannot be relaxed under well-established complexity assumptions.

Slides

An infinite graph is quasi-transitive if the action of its automorphism group on its vertex set has finitely many orbits. Roughly speaking, this means that the graph has a lot of symmetries. Starting with the work of Maschke (1896), a lot of work have been done on the structure of planar Cayley graphs, and more generally of planar quasi-transitive graphs. On the opposite, only few research has been done about the more general class of minor-excluded quasi-transitive graphs. In this talk, I will present a structure theorem for such graphs, which is reminiscent of the Robertson-Seymour Graph Minor Structure Theorem. The proof of our result is mainly based on a combination of the work of Thomassen (1992) together with an extensive study of Grohe (2016) on the properties of separations of order 3 in finite graphs. Our proof involves some technical notions from structural graph theory and I will spend some time to present some of the key concepts involved and especially how they must be adapted to take into account the symmetries of the studied graph. Eventually I will explain how such a result can be used to prove the so called domino problem conjecture for minor-excluded groups, extending previous results from Berger (1966) and Aubrun, Barbieri and Moutot (2019). I will also spend time to present other applications both at the group and at the graph level.

This is a joint work with Louis Esperet and Clément Legrand-Duchesne.

Slides

We show that any permutation of twin-width k can be factorised into the composition of f(k) separable (i.e. twin-width 0) permutations. A corollary is that all classes of structures with bounded twin-width are first-order transductions from one fixed base class.

This factorisation is based on a general decomposition result for structures of bounded twin-width, previously introduced to prove their polynomial χ-boundedness.

This is joint work with Édouard Bonnet, Romain Bourneuf, and Stéphan Thomassé.

Slides

In the past few years the game comonads programme has attempted to bring new perspectives to finite model theory. It builds on an unexpected connection between category theory and model comparison games. In this talk I briefly overview the progress we have made in the last few years and present some unexpected connections that we helped to uncover between finite model theory, algebraic topology and the theory of monads.

Slides

The Weisfeiler–Leman (WL) algorithm is a combinatorial procedure that computes colourings on graphs, which can often be used to detect their (non-)isomorphism. Particularly the 1- and 2-dimensional versions have received much attention. Despite this, the power of the 2-dimensional algorithm is not well understood.

Knowing the expressive power of a certain dimension of the algorithm usually amounts to understanding the computed colourings. In this talk, I investigate the colourings computed by the 2-dimensional WL algorithm on planar graphs and show a classification result for them. 

This is joint work with Daniel Neuen.

Slides

Let Γ be a fixed, finite Boolean constraint language. In MinSAT(Γ), the input is a formula 𝓕 over Γ and an integer k, and the task is to find an assignment α: V(𝓕) -> {0,1} that satisfies all but at most k constraints of 𝓕, or determine that no such assignment exists. With appropriately chosen Γ, MinSAT(Γ) captures classic (parameterized) problems such as st-Min Cut, Edge Bipartization, Almost 2-Sat on the tractable side. On the intractable side, for certain constraint languages Γ the problem MinSAT(Γ) is known not to allow a constant-factor fpt-approximation. Toward completing the full FPT/W[1]-hardness classification of MinSAT(Γ), two problems were known to be a roadblock, namely l-chain SAT and Coupled Min-Cut. 

A recently developed method of directed flow-augmentation (Kim et al., STOC 2022) resolved the above two roadblocks positively, establishing them as being fixed-parameter tractable even for the weighted variants. Furthermore, now a complete dichotomy theorem for MinSAT(Γ) parameterized by the number of unsatisfied constraints is settled, and the directed flow-augmentation turns out to be precisely what was the last missing piece.

In this talk, we give a brief overview on how the key remaining cases for MinSAT(Γ) are modeled as (directed) cut problems, and the applications of directed flow-augmentation to obtain fpt-algorithms for tractable cases. The talk is based on a series of joint work with Stefan Kratsch, Marcin Pilipczuk, Magnus Wahlström.

Slides

One central open question in finite model theory is the question whether there is a logic capturing polynomial time. Since fixed-point logic with counting was shown to be too weak to capture polynomial time, stronger logics were proposed. Two current approaches are on the one hand the usage of hereditarily finite sets in the logic Choiceless Polynomial Time (CPT) and on the other hand symmetric choice - a restricted choice-mechanism for choosing an arbitrary element out of a definable orbit. To guarantee polynomial-time evaluation, these orbits have to be witnessed by definable automorphisms.

In this talk, I will present recent results regarding symmetric choice. I will show how witnessed symmetric choice can be combined with CPT. The resulting logic has the interesting property that a definable isomorphism test implies a definable canonization, which for other logics is not known to be the case. However, to investigate the power of symmetric choice, CPT is the wrong logic to consider since we do not know CPT-undefinable polynomial-time properties. Hence, I will consider fixed-point logic with counting and witnessed symmetric choice. It turns out that this logic fails to capture polynomial time, too, and that ensuring the closure under interpretations is necessary.

Slides

Intuitively, a class of graphs is monadically NIP if one cannot encode, using first-order logic, the class of all graphs into it. Generalizing nowhere denseness, monadic stability, and bounded twin-width, monadic NIP is conjectured to be the exact tractability limit for the first-order model checking problem on hereditary graph classes. Working towards this conjecture, we provide the first two combinatorial characterizations of monadically NIP graph classes. On the structure side, we characterize monadic NIP by a property called flip-breakability. Flip-breakability is an elegant generalization of uniform quasi-wideness and flip-flatness, which characterize nowhere dense and monadically stable classes and played a key role in their respective model checking algorithms. Natural restrictions of flip-breakability additionally characterize bounded cliquewidth and bounded treewidth. On the non-structure side, we characterize monadic NIP by explicitly listing few families of forbidden induced subgraphs. This allows us to resolve one half of the motivating conjecture and show that the first-order model checking problem is AW[*]-hard on every hereditary graph class that is not monadically NIP. 

This is joint work with Jan Dreier and Szymon Toruńczyk.

Slides

For some time, it is known that the model checking problem for first-order formulas is fixed-parameter tractable on nowhere dense graph classes, so we shall ask in which direction there is space for improvements. One of the possible directions is to go beyond first-order formulas: Augmenting first-order logic with general counting quantifiers increases the expressiveness by far, but makes the model checking problem hard even on graphs of bounded tree-depth. The picture is different if we allow only ``simple'' -- but arbitrarily nested -- counting terms of the form #y phi(x_1,...,x_k,y)>N. Even then, only approximate model-checking is possible on graph classes of bounded expansion. Here, the largest known logic fragment, on which exact model-checking is still fpt, consists of formulas of the form Exists x_1 ... Exists x_k [#y phi(x_1,...,x_k,y)>N], where phi(x_1,...,x_k,y) is a first-order formula without counting terms. An example of a problem that can be expressed in this way is partial dominating set: Are there k vertices that dominate at least a given number of vertices in the graph? The complexity of the same problem is open if you replace at least with exactly. Likewise, the complexity of ``are there k vertices that dominate at least half of the blue and half of the red vertices?'' is also open. We answer both questions by providing an fpt algorithm that solves the model-checking problem for formulas of the more general form psi = Exists x_1 ... Exists x_k P(#y phi_1(x_1,...,x_k,y), ..., #y phi_l(x_1,...,x_k,y)), where P is an arbitrary polynomially computable predicate on numbers. The running time is f(|psi|) n^{l+1} polylog(n) on graph classes of bounded expansion. Under SETH, this running time is tight up to almost linear factor.

Slides

I will give an overview on the current status on vertex-minor obstructions and related graph parameters such as rank-width, linear rank-width, rank-depth, clique-width, shrub-depth.

In this talk I'll show how tools originating from model theory can be used for defining canonical decompositions for classes of graphs definable in a combinatorial way. In particular, how one can compute canonical decompositions for finite graphs of bounded treedepth by proving theorems for infinite ones. Using the result about canonical decompositions I'll show that for any fixed graph class C of bounded treedepth, there is an O(n^2)-time algorithm that given two n-vertex graphs from C, checks whether there are isomorphic. This reproves a result of Bouland, Dawar and Kopczyński.

Slides

In order to determine the complexity of graph isomorphism, the expressiveness of various polynomial-time relaxations of graph isomorphism has been studied in the last decades. Prominent examples are the Sherali–Adams and Lasserre hierarchies from linear and semidefinite programming. Only recently, it has emerged that these relaxations can be characterised as homomorphism indistinguishability relations. This means that there exists a graph class 𝓕 such that two graphs G and H fail to be distinguished by the relaxation if and only if they admit the same number of homomorphisms from every graph F ∊ 𝓕.

In this talk, I will show that such characterisations can be obtained using a close connection between combinatorics (labelled graphs) and algebra (homomorphism tensors). Furthermore, I will discuss new insights that homomorphism indistinguishability offers into the expressiveness of graph isomorphism relaxations.

Slides 

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023].

In this talk, we present a recent generalization of these results and almost completely characterize subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number d such that for every r, some tree of depth d and size bounded by an elementary function of r is avoided as an (≤ r)-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size.

Based on joint work with Jakub Gajarský, Michał Pilipczuk, Marek Sokołowski, and Szymon Toruńczyk.

Slides

I will discuss a new family of graph parameters, dubbed flip-width. Those are defined in terms of a pursuit-evasion game, which is played on graphs which are possibly dense. The ensuing notion of classes of bounded flip-width generalizes notions such as bounded expansion and bounded twin-width, and coincides with them when restricted to weakly sparse graph classes, and to classes of ordered graphs, respectively. Finally, the more general classes of almost bounded flip-width include all nowhere dense classes, and are likely to coincide with monadically dependent classes.

Slides

Animated Slides

A local representation of a graph G=(V,E) is an assignment l from V to {0,1}* of labels to the vertices such that adjacency between any two vertices x,y in V can be decided only from the corresponding labels l(x) and l(y). A fundamental question is: which hereditary classes admit local representations with labels of order optimal size (also known as implicit representations)? In particular, until recently one of the central questions in the area was the Implicit Graph Conjecture (IGC) positing that any factorial hereditary class (i.e., a class in which the number of n-vertex labeled graphs is exponential in n log n) admits an implicit representation, i.e. a local representation with labels of size O(log n). In this talk we will present a connection between local representations of graphs and randomized communication that was developed to make progress towards the IGC and led to the refutation of the conjecture by Hatami and Hatami. This is joint work with Nathan Harms and Sebastian Wild.

Slides