AlMoTh 2025

In this talk, we consider the task of representing the set of all homomorphisms between two finite relational structures by tractable circuit classes from knowledge compilation. The idea is that this may allow us to greatly compress the set, while still allowing us to perform various algorithmic tasks---such as counting and enumeration---efficiently. This is a very general problem which can alternatively be viewed as representing the answers to a CSP or as the result of a full conjunctive query on a relational database. Because of this the problem is in general intractable, we are interested in which restrictions of the problem become tractable. In particular, we are interested in left-hand-side restrictions: for which classes of structures A, is it the case that for every A in A and every B, the set of homomorphisms from A to B has a `small' tractable circuit. I will discuss various results related to this problem. The talk is based on ongoing joint work with Christoph Berkholz.

The reconstruction problem for graph embeddings based on homomorphism densities is to determine whether, given a finite sequence of graphs and a corresponding vector of rational numbers, there exists a graph G that realises the vector as homomorphism densities from the given graphs. As far as we know, the decidability of the most general version of this problem remains open. We will show that it is at least as hard as the complexity class NP^(C=P). On the tractable end, we study approximate and restricted variants.

This is a joint work with Martin Grohe, Athena Riazsadri, Nina Runde, and Christoph Standke.
 

Model checking trees generated by order-k Higher-Order Recursion Schemes (HORS) against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong¡¯06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT,such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is k-1-EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via a reduction from a tiling problem.

We prove optimal upper bounds on the Vapnik¨CChervonenkis density of
formulas in the extensions of first-order logic with counting (FOC1) and
with weight aggregation (FOWA1) on nowhere dense classes of (vertex- and
edge-)weighted finite graphs. This lifts a result of Pilipczuk,
Siebertz, and Toru¨½czyk (LICS 2018) from first-order logic on ordinary
finite graphs to substantially more expressive logics on weighted finite
graphs. Moreover, this proves that every FOC1 formula and every FOWA1
formula has bounded Vapnik¨CChervonenkis dimension on nowhere dense
classes of weighted finite graphs; thereby, it lifts a result of Adler
and Adler (Eur. J. Comb.) from first-order logic to FOC1 and FOWA1.
Generalising another result of Pilipczuk, Siebertz, and Toru¨½czyk (LICS
2018), we also provide an explicit upper bound on the ladder index of
FOC1 and FOWA1 formulas on nowhere dense classes. This shows that
nowhere dense classes of weighted finite graphs are FOC1-stable and
FOWA1-stable.

This is joint work with Nicole Schweikardt.

The graph parameter shrub-depth is a dense analog of tree-depth.
We characterize graph classes of bounded shrub-depth by forbidden induced subgraphs.
As an application, we show that on every hereditary class of unbounded shrub-depth, MSO is more expressive than FO.
This confirms a conjecture of [Gajarsk? and Hlin¨§n?; LMCS 2015] who proved that on classes of bounded shrub-depth FO and MSO have the same expressive power.
Combined, the two results fully characterize the hereditary classes on which FO and MSO coincide, answering an open question by [Elberfeld, Grohe, and Tantau; LICS 2012].
Our work is inspired by the notion of stability from model theory.
A graph class C is MSO-stable, if no MSO-formula can define arbitrarily long linear orders in graphs from C.
We show that a hereditary graph class is MSO-stable if and only if it has bounded shrub-depth.
As a key ingredient, we prove that every hereditary class of unbounded shrub-depth FO-interprets the class of all paths.
This improves upon a result of [Ossona de Mendez, Pilipczuk, and Siebertz; Eur. J. Comb. 2025] who showed the same statement for FO-transductions instead of FO-interpretations.

At last year's AlMoTh, Christian Schwarz gave a presentation on the succinctness of modal logic. He showed that modal logic is exponentially more succinct with bi-implication than without it. In this talk our aim is to refine these findings by offering a game-theoretic proof. In order to do so, we look at the formula size game played by Hella and Vilander and adapt it to fit our needs. Then we show that our proof can be extended to work on special classes of Kripke structures, in particular those with transitive and reflexive or symmetric and reflexive accessibility relations. This result is contrasted by the fact that for Kripke structures with a transitive and symmetric accessibility relation, no such succinctness gap exists.

Color Refinement, also known as Naive Vertex Classification, is a
classical method to distinguish graphs by iteratively computing a
coloring of their vertices. While it is mainly used as an imperfect way
to test for isomorphism, the algorithm permeated many other, seemingly
unrelated, areas of computer science. The method is algorithmically
simple, and it has a well-understood distinguishing power: It is
logically characterized by Cai, F¨¹rer and Immerman (1992), who showed
that it distinguishes precisely those graphs that can be distinguished
by a sentence of first-order logic with counting quantifiers and only
two variables. A combinatorial characterization is given by Dvo?¨¢k
(2010), who shows that it distinguishes precisely those graphs that can
be distinguished by the number of homomorphisms from some tree.
In this paper, we introduce Relational Color Refinement (RCR, for
short), a generalization of the Color Refinement method from graphs to
arbitrary relational structures, whose distinguishing power admits the
equivalent combinatorial and logical characterizations as Color
Refinement has on graphs: We show that RCR distinguishes precisely those
structures that can be distinguished by the number of homomorphisms from
an acyclic relational structure. Further, we show that RCR distinguishes
precisely those structures that can be distinguished by a sentence of
the guarded fragment of first-order logic with counting quantifiers.
This is joint work with Nicole Schweikardt.

Finite variable logics play a central role in finite model
theory, serving as a foundational framework for analyzing the complexity
of finite structures. We introduce a restriction to these logics by
limiting the ability of certain variables to be requantified within the
scope of their own quantification. This constraint yields distinct
logical fragments, parameterized by the number of variables that are
either requantifiable or non-requantifiable, thereby providing a more
refined characterization of their expressive power. We explore the
interplay between these restricted logics and various computational
concepts, including games, algorithms, and homomorphism counts,
emphasizing the impact of requantification on the corresponding
counterparts in each domain.
This is based on joint work with Simon Ra?mann and Pascal Schweitzer.

For 50 years, we have been programming with data using the query language / host language paradigm. It¡¯s time to make a change! Rel is a new relational language whose key design goal is to allow both database querying and programming in the large without relying on the currently dominant paradigm in which a query sublanguage is embedded in a host programming language. With the new approach, we can model the semantics of entire enterprise applications relationally, which helps significantly reduce architecture complexity and avoid the well-known impedance mismatch problem. This paradigm shift is enabled by 50 years of database research, making it possible to revisit the sublanguage/host language paradigm, starting from the fundamental principles. We present the vision behind Rel and its main features: those that give it the power to express traditional query language operations, and those that are designed to grow the language and allow programming in the large.

FC-Datalog is a variant of Datalog on strings that allows us to define recursive relations for core spanners. FC-Datalog captures P, and this presents an opportunity for optimization. We propose a series of FC-Datalog fragments with desirable properties in terms of complexity of model checking, expressive power, and efficiency of checking membership in the fragment. This leads to a range of fragments that all capture LOGSPACE, which we further restrict to obtain linear combined complexity.

As a result, we have a framework to tailor fragments for particular applications. We showcase this by simulating deterministic regex in a tailored fragment of FC-Datalog, and demonstrate how this allows us to write programs much more conveniently than other LOGSPACE models. This talk represents an extension to the work I presented at AlMoTh 2024.

FC is a first-order logic that reasons over factors of a finite word using concatenation, and can define non-regular languages like that of all squares (ww). In this talk, we will see that there are regular languages that are not FC-definable. Moreover, I will present a decidable characterization of the FC-definable regular languages in terms of algebra, automata, and regular expressions. The latter of which is natural and concise: Star-free generalized regular expressions extended with the Kleene star of terminal words.
This talk is based on joint work with Nicole Schweikardt and Dominik D. Freydenberger.

A query model for sequence data was introduced in
Kleest-Mei?ner et al. (2022) in the form of subsequence-queries with
wildcards and gap-size constraints (swg-queries, for short). These
queries consist of a pattern over an alphabet of variables and values,
as well as a global window size and a number of local gap-size constraints.

Since then, multiple extensions of the query model were introduced, e.g.
disjunctive swg-queries with intervals or multi-dimensional swg-queries
with generalised gap-size constraints, among others. In this talk, we
provide an overview about the current expressive power of the query
language and discuss a framework for query discovery, i.e. the task of
discovering an swg-query that describes best a given set of event traces.

Algebraic complexity studies families of polynomials in terms of the size of the smallest algebraic circuits representing them.
We study the restriction to symmetric polynomials and symmetric cicuits because it allows to prove strong lower bounds that are out of reach in the general setting: For example, exponential lower bounds on the symmetric circuit complexity of the permanent were shown by Dawar and Wilsenach (2020). In this work, we set out to develop a more general symmetric algebraic complexity theory. Our main result is that a family of symmetric polynomials admits efficient symmetric circuits if and only if they can be written as linear combinations of homomorphism counting polynomials of graphs of bounded treewidth.  We also establish a relationship between the symmetric complexity of subgraph counting and the vertex cover number. Finally, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional complexity dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting.
Joint work with Anuj Dawar and Tim Seppelt.

We study variations of the cops-and-robber-game regarding the following
question: If the cop-player has a winning strategy, do they also have a
winning strategy that is cop- or robber-monotone? We say the respective
variant is cop- or robber-monotone. Here cop-monotonicity denotes that
the cop-player is never allowed to move to a position that they
previously left and robber-monotonicity denotes that the robber-player
can never move to a vertex that was previously occupied by the cops. In
the well-known cops-and-robber-game as defined by Seymour and Thomas
(1993) these notions coincide.

We study a variant of this game, where in each round at most one cop
may be placed and in each play at most q rounds are played, where q is
a parameter of the game. We prove that this game is both cops- and
robber-monotone. As a corollary we obtain a new characterization of
bounded depth treewidth, and we give a positive answer to an open
question by Fluck, Seppelt and Spitzer (2024), thus showing that graph
classes of bounded depth tree-width are homomorphism distinguishing
closed.

Furthermore we study a variant, where the robber player is only allowed
to move, if the cop-player announces that they will move a cop to the
robber-position in the next round. Again we find that these games are
robber-monotone, confirming a conjecture by Richerby and Thilikos
(2011). In the case where the cop-player does not have any information
about the whereabouts of the robber-player, it is known that the number
of cops needed to catch the robber equals the tree width of the graph
plus one. We show that in order to catch the robber using a cop-
monotone strategy one needs path-width plus one may cops, thus this
game variant is not cop-monotone.

This is joint work with Isolde Adler and David Philipps.

Logics with team semantics are logics in which formulae are
not evaluated over individual assignments, but over sets (?teams¡°) of
assignments. This way, concepts like dependence or inclusion can be
introduced on an atomic level and studied with regard to their
expressiveness. In particular, most prominent team logics correspond to
(fragments of) existential second order logic (ESO).

We introduce new function atoms that correspond to the existence of
(total) functions in a team and show that there are several natural
fragments of ESO that can be captured by adding one of these atoms to
established team logics.

Semiring semantics for first-order logic evaluates formulae not just to true or false but to values from a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. Also classical semantics appears as a special case when the Boolean semiring is used, which raises the question to what extent model-theoretic results can be generalized beyond the Boolean semiring and how this relates to the algebraic properties of the underlying semiring. In this talk, we investigate the availability of compactness, which states that a set of sentences is satisfiable if every finite subset is. By defining satisfiability as the existence of non-zero valuations, this implication can be generalized to every absorptive semiring. For the, in Boolean semantics equivalent, formulation via entailment, the situation is different: Based on an order on the semiring, the entailment relation naturally extends to semiring semantics, but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring, the ?ukasiewicz semiring, and the semirings of generalized absorptive polynomials. However, it still holds for finite semirings and (possibly infinite) lattice semirings.