AlMoTh 2024

We present an index structure, called the color-index, to boost the evaluation of acyclic conjunctive queries (ACQs) over binary schemas. 
The color-index is based on the color refinement algorithm, a widely used subroutine for graph isomorphism testing algorithms.
Given a database D, we use a suitable version of the color refinement algorithm to produce a stable coloring of D, an assignment from the active domain of D to a set of colors C_D.
The main ingredient of the color-index is a particular database D_c whose active domain is C_D and whose size is at most |D|.
Using the color-index, we can evaluate any free-connex ACQ Q over D with preprocessing time O(|Q| |D_c|) and constant delay enumeration.
Furthermore, we can also count the number of results of Q over D in time O(|Q| |D_c|).
Given that |D_c| could be much smaller than |D| (even constant-size for some families of databases), the color-index is the first index structure for evaluating free-connex ACQs that allows efficient enumeration and counting with performance strictly smaller than the database size.
This is joint work with Cristian Riveros and Nicole Schweikardt.

The number of walks of length $k$ starting from a given vertex in a graph is expressible, in a certain formal sense, in first-order logic with counting quantifiers with using only two variables. The Immerman-Lander characterization of the color refinement algorithm in terms of this logic suggests walk counting as a tool for testing whether two graphs are isomorphic.
Following this approach, we present the following results.

1. Almost all graphs are canonizable by two matrix-vector multiplications involving the adjacency matrix and the vector of vertex degrees.

2. Almost all Cayley graphs of a cyclic group are canonizable by combining color refinement and vertex individualization.

3. The number of walks of length $k$ between two given vertices is expressible in 3-variable counting logic. It is also well known that this logic captures important spectral invariants of a graph.
We show a tight connection between the spectral invariants and the walk counts, and then use this relationship to compare the strength of the spectral approaches to isomorphism testing and the 2-dimensional Weisfeiler-Leman algorithm.

This is joint work with Maksim Zhukovskii, Vikraman Arvind, Frank Fuhlbrück, and Johannes Köbler (ESA'23, WALCOM'24, and STACS'24).

Previous work on Dynamic Complexity has established that there exist dynamic constant-time parallel algorithms for regular tree languages and context-free languages under label or symbol changes. However, these algorithms were not developed with the goal to minimise work (or equivantly, the number of processors). In fact, their inspection yields the work bounds O(n^2) and O(n^7) per change operation, respectively. In this talk, dynamic algorithms for regular tree languages are proposed that generalise the previous algorithms in that they allow unbounded node rank and leaf insertions, while improving the work bound from O(n^2) to O(n^ϵ), for arbitrary ϵ > 0.For context-free languages algorithms with better work bounds (compared with O(n^7)) for restricted classes are proposed: for every ϵ > 0 there are such algorithms for deterministic context-free languages with work bound O(n^(3+ϵ)) and for visibly pushdown languages with work bound O(n^(2+ϵ)).This talk is based on joint work with Jonas Schmidt and Thomas Schwentick.

This talk proposes dynamic parallel algorithms for connectivity and bipartiteness of undirected graphs that require constant time and O(n^(1/2) ·polylog(n)) work on the (arbitrary) CRCW PRAM model. The work of these algorithms almost matches the work of the O(log n) time algorithm for Connectivity by Kopelowitz et al. (2018) on the EREW PRAM model and the time of the sequential algorithm for bipartiteness by Eppstein et al. (1997). In particular, it is shown that the sparsification technique, which has been used in both mentioned papers, can in principle also be used for constant-time algorithms in the CRCW PRAM model, despite the logarithmic depth of sparsification trees. This talk presents joined work with Thomas Schwentick which was published at MFCS 2023.

Is it possible to write significantly smaller formulae, when using more Boolean operators in addition to the De Morgan basis (and, or, not)?
For modal logic, we show that adding bi-implication allows to write exponentially smaller formulae (as opposed to propositional logic). 
Moreover, we provide a complete classification of finite sets of Boolean operators, showing they are either of no help (allow polynomial translations to the De Morgan basis) or can express properties as succinct as modal logic with additional bi-implication.
More precisely, these results are shown for the modal logic T (and therefore for K). We complement this result by showing that the modal logic S5 behaves as propositional logic: no additional Boolean operators make it possible to write significantly smaller formulae.

Given two n-element structures, which can be distinguished by a sentence of first-order logic using only k variables, what can we say about the number of quantifiers required by a separating sentence? We will present various results related to this question. In particular, we show that when we limit the number of variables, there can be an exponential gap between the quantifier depth and the quantifier number needed to separate two structures. As a consequence, we show that the (k+1)-variable fragment of first-order logic is exponentially more succinct than the k-variable fragment.

Ehrenfeucht–Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. In this talk, we investigate the soundness and completeness of this method in the more general context of semiring semantics, which is based on the idea to evaluate logical statements by values of a commutative semiring. This can provide additional information such as evaluation costs, confidence scores or access levels. 

While Ehrenfeucht–Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, we show that this does not generalize to any other semiring: While soundness requires full idempotence of the underlying semiring, it is excluded by completeness. We also discuss soundness and completeness of variants of classical Ehrenfeucht–Fraïssé games based on bijections or counting, which are sound on every semiring and even complete on some important semirings. Finally, we propose a new kind of game, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.

based on joint work with Erich Grädel and Lovro Mrkonjić

A graph class is monadically stable (resp. monadically NIP) if it does not transduce all linear orders (resp. all graphs) using first-order logic.
Originally studied in the 1980s in model theory, those two notions have recently generated interest in structural and algorithmic graph theory where they generalize planarity, tree/clique/twin-width, and nowhere denseness.
Combining tools from logic and combinatorics, we develop a theory for monadically stable and monadically NIP graph classes, that is well suited for their algorithmic treatment.
On the structure side, we present the first purely combinatorial characterizations of monadic stability and monadic NIP by Ramsey theoretic properties dubbed flip-flatness and flip-breakability.
On the non-structure side, we give a characterization by explicitly listing few families of forbidden induced subgraphs.
The two approaches yield new tractability and hardness results for the first-order model checking problem: it is fixed-parameter tractable on every monadically stable graph class and AW[*]-hard on every hereditary graph class that is not monadically NIP.

We prove that isomorphism of tournaments of twin width at most $k$ can be decided in time $k^{O(\log k)}n^{O(1)}$. This implies that the isomorphism problem for classes of tournaments of bounded or moderately growing twin width is in polynomial time. By comparison, there are classes of undirected graphs of bounded twin width that are isomorphism complete, that is, the isomorphism problem for the classes is as hard as the general graph isomorphism problem. Twin width is a graph parameter that has been introduced only recently (Bonnet et al., FOCS 2020), but has received a lot of attention in structural graph theory since then. On directed graphs, it is functionally smaller than clique width. We prove that on tournaments (but not on general directed graphs) it is also functionally smaller than directed tree width (and thus, the same also holds for cut width and directed path width). Hence, our result implies that tournament isomorphism testing is also fixed-parameter tractable when parameterized by any of these parameters.

Our isomorphism algorithm heavily employs group-theoretic techniques. This seems to be necessary: as a second main result, we show that the combinatorial Weisfeiler-Leman algorithm does not decide isomorphism of tournaments of twin width at most 35 if its dimension is $o(\sqrt n)$.

Joint work with Martin Grohe.

We study the expressive power of first-order logic with counting quantifiers, especially the k-variable and quantifier-rank-q fragment C^k_q, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio (2021) proved that two graphs satisfy the same C^k_q-sentences if and only if they are homomorphism indistinguishable over the class T^k_q of graphs admitting a k-pebble forest cover of depth q. Their proof builds on the categorical framework of game comonads developed by Abramsky, Dawar, and Wang (2017). We reprove their result using elementary techniques inspired by Dvořák (2010).
Using these techniques we also give a characterisation of guarded counting logic. Our main focus, however, is to provide a graph theoretic analysis of the graph class T^k_q. This allows us to separate T^k_ from the intersection of the graph class TW^{k−1}, that is graphs of treewidth less or equal k − 1, and TD_q, that is graphs of treedepth at most q if q is sufficiently larger than k. We are able to lift this separation to the semantic separation of the respective homomorphism indistinguishability relations. A part of this separation is to prove that the class TD_q is homomorphism distinguishing closed, which was already conjectured by Roberson (2022).
This is joint work with Tim Seppelt and Gian Luca Spitzer.

Two graphs G and H are homomorphism indistinguishable over a family of graphs \CF if for all F \in \CF the number of homomorphisms from F to G is equal to the number of homomorphism from F to H. Many natural equivalence relations comparing graphs such as (quantum) isomorphism, cospectrality, and logical equivalences can be characterised as homomorphism indistinguishability relations over various graph classes.

For a fixed graph class \CF, the decision problem HomInd(\CF) asks to determine whether two input graphs G and H are homomorphism indistinguishable over \CF. The problem HomInd(\CF) is known to be decidable only for few graph classes \CF. We show that HomInd(\CF) admits a randomised polynomial-time algorithm for every graph class \CF of bounded treewidth which is definable in counting monadic second order-logic CMSO2. Thereby, we give the first general algorithm for deciding homomorphism indistinguishability.

This result extends to a version of HomInd where the graph class \CF is specified via a CMSO2-sentence and a bound k on the treewidth, which are given as input. For fixed k, this problem is randomised fixed-parameter tractable. If k is part of the input then it is coNP- and coW[1]-hard. Addressing a problem posed by Berkholz (2012), we show coNP-hardness by establishing that deciding indistinguishability under the k-dimensional Weisfeiler--Leman algorithm is coNP-hard when k is part of the input.

Property testing (for a property P) asks for a given graph, whether it has property P, or is "structurally far" from having that property. A "testing algorithm" is a probabilistic algorithm that answers this question with high probability correctly, by only looking at small parts of the input.  Testing algorithms are thought of as "extremely efficient", making them relevant in the context of large data sets.

In this talk I will present recent positive and negative results about testability of properties definable in first-order logic and monadic second-order logic on classes of bounded-degree graphs.

This is joint work with Polly Fahey, Frederik Harwath, Noleen Köhler and Pan Peng.

We are interested in the following algorithmic problem: given multiple pairs $ (t_1, t_1^\star),\dots , (t_n, t_n^\star) $ of trees, learn a set of rules to describe (structural) differences common to all these pairs of trees. The learned set of rules shall be able to manipulate each tree $ t_i $ into the tree $ t_i^\star $ in few steps. 
To tackle this problem, we (1) introduce a pattern-based specification language for tree transformations; (2) study the complexity of several variants of the above algorithmic problem and show NP hardness even for very restricted variants, and (3) show how to solve the problem in practice using SAT solvers.

I will present a new lower bound on the iteration number of the Weisfeiler-Leman algorithm.

For every k, there is a class of graphs on which the iteration number of the k-dimensional Weisfeiler-Leman algorithm is Ω(n^k/2), which is the first improvement since Fürers Ω(n) lower bound on graphs. It actually improves over the best known lower bound on k-ary relational structures of n^Ω(k). The construction is based on a new compression technique for Cai-Fürer-Immerman graphs.

The talk is based on joint work with Martin Grohe, Daniel Neuen, and Pascal Schweitzer.

The constraint satisfaction problem (CSP) can be formulated as a homomorphism problem between relational structures: given structure A, for any structure X, whether there exists a homomorphism from X to A. It was conjectured for years that all problems of this kind over finite domains are divided into polynomial time and NP-complete problems, and the conjecture was proved in 2017 separately by Zhuk [1] and Bulatov [2].

Zhuk’s algorithm solves any tractable CSP(A) in polynomial time. For satisfiable instances, the algorithm produces a solution, i.e. a polynomial-size witness of an affirmative answer that one can independently check in polynomial time. That is not the case for unsatisfiable instances.

We use some proof complexity methods (formalization in theories of bounded arithmetic, propositional translations, etc.) to show that the algorithm may be appended to provide an independent proof of the correctness of the algorithm for negative answers too. We present the formalization of the algorithm in the theory of bounded arithmetic W₁ ¹ introduced in [3]. The formalization shows that W₁ ¹ proves the soundness of Zhuk’s algorithm, where by soundness we mean that any rejection of the algorithm is correct. Together with the known relation of the theory to propositional calculus G, it follows that tautologies, expressing the non-existence of a solution for unsatisfiable instances, have short proofs in G.

References
1. Zhuk, D.: A proof of the csp dichotomy conjecture. J. ACM 67(5), 1–78 (2020)
2. Bulatov, A.A.: A dichotomy theorem for nonuniform csps. In: 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pp. 319–330. IEEE, Berkeley, CA, USA (2017)
3. Skelley, A.: A Third-Order Bounded Arithmetic Theory for PSPACE. In Computer Science Logic, pp. 340–354. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)

We consider the parameterized complexity of the problem to decide whether a given natural number n satisfies a given bounded arithmetical formula; the parameter is the size of the formula. This parameterization naturally focusses attention on instances where n is large compared to the formula. We show unconditionally that this problem does not belong to the parameterized analogue of AC0. From this we derive that certain natural upper bounds on the complexity of our parameterized problem imply certain separations of classical complexity classes. This connection is obtained via an analysis of a parameterized halting problem. Some of these upper bounds follow assuming that bounded induction proves the MRDP theorem in a certain weak sense.

The Ideal Proof System or IPS (Grochow, Pitassi 2018) is a powerful circuit-based algebraic proof system for proving the unsatisfiability of polynomial equation systems.
We propose and study a natural restriction sym-IPS where the circuits are required to be symmetric under symmetries of the input equations. 
Variants of the resulting system efficiently simulate other well-known symmetry-invariant formalisms such as fixed-point logic with counting and Choiceless Polynomial Time, specifically with respect to the graph isomorphism problem.
We also study the power of sym-IPS on typical proof complexity benchmarks, identifying the pigeonhole principle as a potential candidate for exponential lower bounds. A surprising connection to the symmetric complexity of the permanent (Dawar, Wilsenach 2020) appears and can potentially be exploited for a lower bound. Joint work with Anuj Dawar, Erich Grädel and Leon Kullman.

We present a linear preprocessing and output linear delay enumeration algorithm for MSO-queries over trees that are compressed in the well-established grammar-based framework.
Time bounds are measured with respect to the size of the compressed representation of the tree.
Our result extends previous work on the enumeration of MSO-queries over uncompressed trees and on the enumeration of document spanners over compressed text documents.

Document Spanners query text documents analogously to how one queries a relational database. Despite considerable research on document spanners, little is known about the expressive power of a particular class known as generalized core spanners.
 
For first-order logic, one of the fundamental tools for inexpressibility are Ehrenfeucht-Fraïssé Games. To use Ehrenfeucht-Fraïssé games in order to yield inexpressibility results for generalized core spanners, we need a suitable logic. For this task, we use FC; a finite-model variant of the theory of concatenation.
 
Using Ehrenfeucht-Fraïssé games, we obtain general inexpressibility lemmas for the logic FC. Applying these lemmas give inexpressibility results for FC that we lift to generalized core spanners. In particular, we give several queries that cannot be selected by generalized core spanners.

Datalog is a recursive query language for relational databases. We propose a novel adaptation of Datalog for querying text, where earlier attempts resulted in an undecidable model checking problem. Based on FC, a logic for document spanners that combines finite model theory and the theory of concatenation, we use FC-Datalog, a recursive query language for text that has been shown to capture the complexity class P.

In this talk, we discuss fragments of FC-Datalog with fast evaluation. Similarly to classical Datalog for relational databases, we first introduce Linear FC-Datalog, a fragment that captures NLOGSPACE. We then show that deterministic Linear FC-Datalog captures LOGSPACE, although deciding if a program is deterministic is NP-hard.

As such, we introduce another fragment One Letter Lookahead (OLLA) Linear FC-Datalog, where deterministic OLLA (DOLLA) Linear FC-Datalog also captures LOGSPACE, but where determinism can be checked in polynomial time.

Isolde Adler, Universität Bamberg
Eric Alsmann, Universität Kassel
Bednarczyk Bartosz, TU Dresden/ University of Wroclaw
Owen Bell, Loughborough University
Christoph Berkholz, TU Ilmenau
Sophie Brinke, RWTH Aachen
Florian Bruse, Universität Kassel
Martin Dietzfelbinger, TU Ilmenau
Kord Eickmeyer, TU Darmstadt
Eva Fluck, RWTH Aachen
Azza Gaysin, Universität Passau
Erich Grädel, RWTH Aachen
Dorian Gutschenreiter, HU Berlin
Louis Härtel, RWTH Aachen
Christopher Hugenroth, TU Ilmenau
Vincent Klimmer, TU Ilmenau
Chris Köcher, Max Planck Institute for Software Systems
Dietrich Kuske, TU Ilmenau
Cecilia Lange, HU Berlin
Martin Lange, Universität Kassel
Charlotte Lenz, HU Berlin
Moritz Lichter, RWTH Aachen
Nikolas Mählmann, Universität Bremen
Maximilian Merz, TU Ilmenau
Matthäus Micun, TU Ilmenau
Lovro Mrkonjić, RWTH Aachen
Moritz Müller, Universität Passau
Matthias Naaf, RWTH Aachen
Daniel Neuen, Universität Bremen
Matthias Niewerth, Universität Bayreuth
Tomáš Novotný, RWTH Aachen
Benedikt Pago, University of Cambridge
Sebastian Pfau, TU Ilmenau
Cristian Riveros, PUC & IMFD Chile
Marco Sälzer, Universität Kassel
Benjamin Scheidt, HU Berlin
Florian Schmalstieg, Ruhr-Universität Bochum
Marko Schmellenkamp, Ruhr-Universität Bochum
Markus Schmid, HU Berlin
Jonas Schmidt, TU Dortmund
Christian Schwarz, TU Ilmenau
Nicole Schweikardt, HU Berlin
Tim Seppelt, RWTH Aachen
Christoph Standke, RWTH Aachen
Joseph Stimpson, Universität Bamberg
Sam Thompson, Loughborough University
Jennifer Todtenhoefer, TU Dortmund
Marius Tritschler, TU Darmstadt
Felix Tschirbs, Ruhr-Universität Bochum
Steffen van Bergerem, HU Berlin
Fabian Vehlken, Ruhr-Universität Bochum
Oleg Verbitsky, HU Berlin
Harry Vinall-Smeeth, TU Ilmenau
Nils Vortmeier, Ruhr-Universität Bochum
Max Wehmeier, HU Berlin
Hermann Wilhelm, TU Ilmenau
Thomas Zeume, Ruhr-Universität Bochum

• Ilmenau has its own train connection Ilmenau, main station    To the journey planner

Continue from Ilmenau main station

• in the direction of the campus of the Technical University, approx. 25 min. on foot route description via Google maps

or

• take the city line A (direction Technical University) to the Mensa, then approx. 3 min. on foot in each case (timetable for bus)

• via the A71 Erfurt-lmenau or A71 Schweinfurt-Ilmenau motorways

• the campus is located on the B88, at the end of Ilmenau, in the direction of Rudolstadt

• Visitor car parks are available, (please call in advance for an access code at +49 (0) 3677 69 2655)

• Contingent reservation Hotel Mara, bis 31.01.2024,
  Overnight stay with breakfast and car park 89,00 €, Keyword: AlMoTh 2024

• adress:
  mara Hotel
  Krohnestraße 5, 98693 Ilmenau
  phone: +49 3677 4680390

• Contingent reservation Hotel Tanne until 01.02.2024,
  Overnight stay with breakfast € 84.00, keyword: AlMoTh 2024

• adress:
  Hotel Tanne
  Lindenstraße 38, 98639 Ilmenau
  phone: +49 3677 6590