Abstracts

INVITED TALKS

Albert Atserias (Universitat Politècnica de Catalunya)

Title:  Are Average-Case Lower Bounds for Symmetric Boolean Circuits Within Reach?

Abstract: While proving impossibility results for general Boolean circuits is the holly grail of computational complexity theory, the progress in this area is, admittedly, very slow. The same question for restricted models of Boolean circuits has seen much more success: strong and close to optimal lower bounds are known for bounded-depth Boolean circuits with and without modular counting gates, monotone Boolean circuits, symmetric Boolean circuits with and without majority gates, among others. In this talk I will partially survey some of these results, with emphasis on the logic-based methods for symmetric Boolean circuits of various types, and discuss the prospects for proving average-case lower bounds (on Erdos-Renyi random graphs, say) for them.

Anuj Dawar (University of Cambridge)

Title: Seese's conjecture: an update

Abstract: Seese’s conjecture for finite graphs states that monadic second-order logic (MSO) is undecidable on all graph classes of unbounded clique-width. It remains open thirty years after it was first formulated. In this talk, I outline an approach to the conjecture based on classifying classes of unbounded clique-width.

joint work with Abhisekh Sankaran

Sebastian Siebertz (University of Bremen)

Title: Algorithmic meta-theorems

Abstract: Algorithmic meta-theorems provide general explanations when and why certain algorithmic problems can be solved efficiently. They are typically formulated in terms of logic (defining the descriptive complexity of the problems) and structural properties of their inputs. In this talk I will give an overview over the classical meta-theorems for first-order logic (FO) and monadic second-order logic (MSO) as well as recent results for logics with expressive power that lies between these two logics.

Szymon Toruńczyk (University of Warsaw)

Title: On monadically stable and monadically NIP classes of graphs

Abstract: Sparsity theory, initiated by Ossona de Mendez and Nesetril, identifies those classes of sparse graphs that are tractable in various ways (e. g. from the perspective of the model checking problem for first order logic) as exactly the nowhere dense classes. There is an ongoing effort aimed at generalizing sparsity theory to classes of graphs that are not necessarily sparse. It is conjectured that the relevant notion characterising dense graph classes that are tractable, generalising nowhere denseness, is the notion of monadically NIP classes, introduced by Shelah in model theory. I will survey some recent progress in the understanding of those classes, and of the related monadically stable classes. In particular, monadically NIP classes are a common generalization of the notions of nowhere denseness and of twin-width, introduced recently by Bonnet, Thomasse, and coauthors.

REGULAR TALKS

Zdeněk Dvořák (Computer Science Institute, Charles University)

Title: Approximation meta-algorithms for FO properties

Abstract: An important result of Grohe, Kreutzer, and Siebertz shows that all optimization problems expressible in the first-order logic (such as the independence number or domination number) are fixed-parameter tractable (when parameterized by the solution size) in graphs from a monotone graph class if and only if the class is nowhere dense, subject to standard complexity-theoretic assumptions. What about approximation algorithms for these problems? We survey the meta-algorithmic and complexity results on this topic and present some open questions.

Ioannis Eleftheriadis (University of Cambridge)

Title: Monadic NIP in monotone classes of relational structures

Abstract: It is conjectured that the hereditary classes of structures that admit fixed parameter tractable model-checking are precisely those that are (monadically) NIP.  We provide a positive answer to this conjecture in the case of monotone classes of arbitrary relational structures. This is established by showing that (monadic) NIP coincides with having nowhere dense Gaifman class for monotone classes.
 
Joint work with Sam Braunfeld, Anuj Dawar, and Aris Papadopoulos.

Colin Geniet (Univ Lyon, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP)

Title: First-order logic and twin-width in tournaments

Abstract: We characterise classes of tournaments with FPT first-order model checking. In a hereditary class T of tournaments, first-order model checking either is fixed parameter tractable, or is AW[*]-hard. This dichotomy coincides with the fact that T has either bounded or unbounded twin-width, and that the growth of T is either at most exponential or at least factorial, and that T either is monadically NIP or interprets the class of all graphs. Furthermore, these dichotomies are characterised by three infinite families of obstructions: T has bounded twin-width if and only if it excludes one tournament from each family. This generalises results of Bonnet et. al. on ordered graphs. These results are proved by constructing an order < on any tournament T with the property that if the birelation (T,<) has (very) large twin-width, then there is some subtournament T' still with large twin-width inside which the order < is first-order definable. This is enough to reduce the problem to the known case of ordered structures.

Joint work with Stéphan Thomassé.

Lars Jaffke (Department of Informatics, University of Bergen)

Title: A logic-based algorithmic meta-theorem for mim-width

Abstract:  We introduce a logic called distance neighborhood logic with acyclicity and connectivity constraints (A&C DN for short) which extends existential MSO1 with predicates for querying neighborhoods of vertex sets and for verifying connectivity and acyclicity of vertex sets in various powers of a graph. Building upon [Bergougnoux and Kanté, ESA 2019; SIDMA 2021], we show that the model checking problem for every fixed A&C DN formula is solvable in n^O(w) time when the input graph is given together with a branch decomposition of mim-width w. Nearly all problems that are known to be solvable in polynomial time given a branch decomposition of constant mim-width can be expressed in this framework. We add several natural problems to this list, including problems asking for diverse sets of solutions. Our model checking algorithm is efficient whenever the given branch decomposition of the input graph has small index in terms of the d-neighborhood equivalence [Bui-Xuan, Telle, and Vatshelle, TCS 2013]. We therefore unify and extend known algorithms for tree-width, clique-width and rank-width. Our algorithm has a single-exponential dependence on these three width measures and asymptotically matches run times of the fastest known algorithms for several problems. This results in algorithms with tight run times under the Exponential Time Hypothesis (ETH) for tree-width and clique-width; the above mentioned run time for mim-width is nearly tight under the ETH for several problems as well. Our results are also tight in terms of the expressive power of the logic: we show that already slight extensions of our logic make the model checking problem para-NP-hard when parameterized by mim-width plus formula length.

Joint work with Benjamin Bergougnoux and Jan Dreier.

Stephan Kreutzer (TU Berlin)

Title: Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

Abstract: We present a fixed-parameter tractable algorithm for first-order model checking on interpretations of graph classes with bounded local cliquewidth. Notably, this includes interpretations of planar graphs, and more generally, of classes of bounded genus. To obtain this result we develop a new tool which works in a very general setting of dependent classes and which we believe can be an important ingredient in achieving similar results in the future

Joint work with Édouard Bonnet, Jan Dreier, Jakub Gajarský, Nikolas Mählmann, Pierre Simon, Szymon Toruńczyk.

Mamadou Kanté (LIMOS, CNRS, Aubière,)

Title: MSOL-definability of decompositions

Abstract: After recalling interest in definability of decompositions, I will show how to define in MSOL branch-decompositions for strongly pigeonhole matroids of bounded linear decomposition-width. Strongly pigeonhole matroids include finitely representable matroids, but also fundamental transversal matroids and 3-connected bi-circular ones. They are characterised by the following property : for each subset X, the number of equivalence classes wrt matroid circuit is bounded by the connectivity of X.

Matthieu Rosenfeld (LIRMM, Univ Montpellier)

Title: Bounding the number of sets defined by a given MSO formula on trees

Abstract: Monadic second-order logic can be used to express many classical notions of sets of vertices of a graph as for instance: dominating sets, induced matchings, perfect codes, independent sets, or irredundant sets. Bounds on the number of sets of any such family of sets are interesting from a combinatorial point of view and have algorithmic applications. Many such bounds on different families of sets over different classes of graphs are already provided in the literature. In particular, Rote recently showed that the number of minimal dominating sets in trees of order n is at most 95^(n/13) and that this bound is asymptotically sharp up to a multiplicative constant. We build on his work to show that what he did with minimal dominating sets can be done with any family of sets definable by a monadic second-order formula.

Peter Rossmanith (RWTH Aachen)

Title: Evaluating Restricted First-Order Counting Properties on Nowhere Dense Classes and Beyond

Abstract: It is known that first-order logic with some counting extensions can be efficiently evaluated on graph classes with bounded expansion, where depth-$r$ minors have constant density.  More precisely, the formulas are $\exists x_1\ldots x_k \#y\,\phi(x_1,\ldots,x_k, y)>N$, where $\phi$ is an FO-formula. If $\phi$ is quantifier-free, we can extend this result to \emph{nowhere dense} graph classes with an almost linear FPT run time.  Lifting this result further to slightly more general graph classes, namely almost nowhere dense classes, where the size of depth-$r$ clique minors is subpolynomial, is impossible unless $\rm FPT=W[1]$.  On the other hand, in almost nowhere dense classes we can approximate such counting formulas with a small additive error.
In particular, it follows that partial covering problems, such as partial dominating set, have fixed parameter algorithms on nowhere dense graph classes with almost linear running time.

Joint work with Jan Dreier and Daniel Mock.

Ignasi Sau (LIRMM, Univ Montpellier, CNRS)

Title: Compound Logics for Modification Problems

Abstract: We introduce a novel model-theoretic framework inspired from graph modification and based on the interplay between model theory and algorithmic graph minors. The core of our framework is a new compound logic operating with two types of sentences, expressing graph modification: the modulator sentence, defining some property of the modified part of the graph, and the target sentence, defining some property of the resulting graph. In our framework, modulator sentences are in counting monadic second-order logic (CMSOL) and have models of bounded treewidth, while target sentences express first-order logic (FOL) properties along with minor-exclusion. Our logic captures problems that are not definable in first-order logic and, moreover, may have instances of unbounded treewidth. Also, it permits the modeling of wide families of problems involving vertex/edge removals, alternative modulator measures (such as elimination distance or G-treewidth), multistage modifications, and various cut problems. Our main result is that, for this compound logic, model-checking can be done in quadratic time. All derived algorithms are constructive and this, as a byproduct, extends the constructibility horizon of the algorithmic applications of the Graph Minors theorem of Robertson and Seymour. The proposed logic can be seen as a general framework to capitalize on the potential of the irrelevant vertex technique. It gives a way to deal with problem instances of unbounded treewidth, for which Courcelle's theorem does not apply. The proof of our meta-theorem combines novel combinatorial results related to the Flat Wall theorem along with elements of the proof of Courcelle's theorem and Gaifman's theorem. We finally prove extensions where the target property is expressible in FOL+DP, i.e., the enhancement of FOL with disjoint-paths predicates.

Joint work with Fedor V. Fomin, Petr A. Golovach, Giannos Stamoulis, Dimitrios M. Thilikos

Giannos Stamoulis (LIRMM, Univ Montpellier)

Title: Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classe

Abstract: The disjoint paths logic, FOL+DP, is an extension of First Order Logic (FOL) with the extra atomic predicate dpk(x_1, y_1, . . . , x_k, y_k), expressing the existence of internally vertex- disjoint paths between x_i and y_i, for i ∈ {1, . . . , k}. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every minor- closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate s-sdpk(x_1, y_1, . . . , x_k, y_k), demanding that the disjoint paths are within distance bigger than some fixed value s. Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.

Joint work with Petr A. Golovach and Dimitrios M. Thilikos

Stefan Szeider (Algorithms and Complexity Group, Faculty of Informatics, TU Wien)

Title: From Twin-Width to Propositional Logic and Back 

Abstract: The width measure twin-width was recently introduced by Bonnet et al. (FOCS 2020), who showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this talk, we discuss two connections between twin-width and propositional logic. First, we show that a generalization of the propositional satisfiability problem, obtaining the weighted sum of all satisfying assignments to a formula in CNF that set at most k variables to true, is fixed-parameter tractable. As the parameter, we take the certified signed twin-width of the input formula and the bound k. Second, we propose an efficient encoding of the recognition problem for graphs of bounded twin-width to the propositional satisfiability problem (SAT). This encoding allows us to utilize the power of today's SAT solvers to identify the exact twin-width of several graphs whose twin-width was unknown. The SAT encoding relies on a characterization of twin-width based on elimination sequences. We modify the encoding to deal with the above-mentioned signed twin-width. 

Joint work with Robert Ganian, Filip Pokrývka, and André Schidler.