AlMoTh 2023

AlMoTh Meeting

Algorithmic Model Theory Meeting 2023

The AlMoTh 2023 meeting will take place at Ruhr-Universität Bochum (RUB) on 2 March and 3 March 2023. The talks will be held in the Open Space area of the Faculty of Computer Science (building MC/VC on RUB campus, Universitätsstr. 140 in Bochum)

Abstracts and registration

In case you want to give a talk, please send title and abstract to almoth2023 at rub.de by 16 February 2023.

Registrations should be sent to almoth2023 at rub.de by 16 February 2023, as well.

Programme

Thursday, 2 March

12:00-13:00 Welcome: Snacks & soup

13:00-14:10 Session: Homomorphisms

In 1967, Lovász proved that two graphs G and H are isomorphic iff they are homomorphism indistinguishable over the the family of all graphs, i.e. for all graphs F the number of homomorphisms from F to G is equal to the number of homomorphisms from F to H. In recent years, many natural equivalence relations comparing graphs like quantum isomorphism, cospectrality, or logical equivalences have been characterised as homomorphism indistinguishability relations over restricted graph classes.

In this talk, I report on recent work with David Roberson which shows that for every t feasibility of the level-t Lasserre semidefinite programming relaxation of the standard integer program for graph isomorphism can be characterised as a homomorphism indistinguishability relation over a novel graph class L_t. By studying graph-theoretic properties of L_t, the power of the Lasserre and Sherali–Adams hierarchy to distinguish graphs can be compared exactly. In addition to these concrete applications, I give an overview of Roberson’s conjecture and explain how homomorphism indistinguishability can be used to separate graph properties.

The task of computing homomorphisms between two finite relational structures $A$ and $B$
is a well-studied question with numerous applications. Since the set $Hom(A, B)$ of all
homomorphisms may be very large having a method of representing it in a succinct way,
especially one which enables us to perform efficient enumeration and counting can be
extremely useful.

One simple yet powerful way of doing this is to decompose $Hom(A, B)$ using union and
Cartesian product. Such data structures, called d-representations, have been introduced
by Olteanu and Závodný in the context of evaluating conjunctive queries. Their results
also imply that if the treewidth of the left-hand side structure A is bounded, then a d-
representation of polynomial size can be found in polynomial time. We show that for
structures of bounded arity this is optimal: if the treewidth is unbounded then there are
instances where the size of any d-representation is superpolynomial. Along the way, we
develop tools for proving lower bounds on the size of d-representations, in particular we
define a notion of reduction suitable for this context and prove an almost tight lower
bound on the size of d-representations of all k-cliques in a graph.

This is joint work with Christoph Berkholz.

 

We introduce the 2-sorted counting logic GC^k that expresses properties of hypergraphs.
This logic has available k „blue“ variables to address edges, an unbounded number of „red“ variables to address vertices of a hypergraph, and atomic formulas E(e,v) to express that vertex v is contained in edge e.
We show that two hypergraphs H, H‘ satisfy the same sentences of the logic GC^k if, and only if, they are homomorphism indistinguishable over the class of hypergraphs of generalised hypertree width at most k.
Here, H, H‘ are called homomorphism indistinguishable over a class C if for every hypergraph G in C the number of homomorphisms from G to H equals the number of homomorphisms from G to H‘.
This result can be viewed as a generalisation (from graphs to hypergraphs) of a result by Dvorak (2010) stating that any two (undirected, simple, finite) graphs H, H‘ are indistinguishable by the (k+1)-variable counting logic C^{k+1} if, and only if, they are homomorphism indistinguishable on the class of graphs of tree width at most k.

14:10-14:20 Short break
 

14:20-15:30 Session: Teaching & Learning

Designing computational reductions is a challenging task for students. In this talk we explore
formal foundations for offering support for this learning task by teaching support systems. Our
approach is to (a) identify typical building blocks of reductions, (b) develop a simple descriptional
language for specifying reductions that allows for combining building blocks in a simple, modular
manner, (c) study the expressive power of such a language to ensure that it is reasonably broad, and
to (d) design suitable algorithms for employing this language in teaching support systems, including
the design of feedback mechanisms.

We analyse the power of graph neural networks (GNNs) in terms of Boolean circuit complexity and descriptive complexity.

We prove that the graph queries that can be computed by a polynomial-size bounded-depth family of GNNs are exactly those definable in the guarded fragment GFO+C of first-order logic with counting with built-in relations. This puts GNNs in the circuit complexity class TC^0. Remarkably, the GNN families may use arbitrary real weights and a wide class of of activation functions that include the standard ReLU, logistic „sigmoid“, and hyperbolic tangent functions. If the GNNs are allowed to use random initialisation and global readout (both standard features of GNNs widely used in practice), they can compute exactly the same queries as bounded depth Boolean circuits with threshold gates, that is, exactly the queries in TC^0.

Moreover, we show that queries computable by a single GNN with piecewise linear activations and rational weights are definable in
GFO+C without built-in relations. Therefore, they are contained in uniform TC^0.

 

In this talk, we will take a brief look at recent results on the logical expressiveness of graph neural networks (GNN),
neural network based models that compute functions over graphs.
Furthermore, we will relate these results to common formal verification problems of GNN, with the goal of
deriving new decidability and complexity bounds.

15:30-16:00 Coffee break

16:00-17:10 Session: Logic & Complexity

The fixed-point logic LREC= was developed by Grohe et al. (CSL 2012) in the quest for a logic to capture all problems decidable in logarithmic space.
It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion.
We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-order logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth.
This yields that any pair of graphs separable by the property can be distinguished with the k-dimensional Weisfeiler–Leman algorithm in a logarithmic number of iterations.
In particular, it implies that the algorithm identifies every interval graph and every chordal claw-free graph in logarithmically many iterations,

which is a joint work with Steffen van Bergerem, Martin Grohe, Sandra Kiefer.

We prove unconditionally that superpolynomial circuit lower bounds for NEXP are consistent with the bounded arithmetic V^0_2. The same holds for barely superpolynomial non-deterministic time. Additionally, we prove a magnification result on the hardness of proving circuit lower bounds.

Choiceless Polynomial Time (CPT) is one of the few remaining candidate logics for capturing PTIME. We make progress towards separating CPT from polynomial time by firstly establishing a connection between the expressive power of CPT and the existence of certain symmetric circuit families, and secondly, proving lower bounds against these circuits. We focus on the isomorphism problem of unordered Cai-Fürer-Immerman-graphs (the CFI-query) as a potential candidate for separating CPT from P. Results by Dawar, Richerby and Rossman, and subsequently by Pakusa, Schalthöfer and Selman show that the CFI-query is CPT-definable on linearly ordered and preordered base graphs with small colour classes. We define a class of CPT-algorithms, that we call „CFI-symmetric algorithms“, which generalises all the known ones, and show that such algorithms can only define the CFI-query on a given class of base graphs if there exists a family of symmetric XOR-circuits with certain properties. These properties include that the circuits have the same symmetries as the base graphs, are of polynomial size, and satisfy certain fan-in restrictions. Then we prove that such circuits with slightly strengthened requirements (i.e. stronger symmetry and fan-in and fan-out restrictions) do not exist for the n-dimensional hypercubes as base graphs. This almost separates the CFI-symmetric algorithms from polynomial time – up to the gap that remains between the circuits whose existence we can currently disprove and the circuits whose existence is necessary for the definability of the CFI-query by a CFI-symmetric algorithm.

17:10-17:20 Short break

17:20-18:00 Session: Query evaluation

Probabilistic databases model uncertain data as a probability space over traditional relational databases. Evaluating queries in probabilistic databases hence requires computing confidences for the answers, which is #P-hard even for (some) conjunctive queries.
Therefore, new methods are needed to obtain practical solutions.

We survey the computational complexity of approximately evaluating queries. In particular, we study the data complexity of queries with regard to additive and multiplicative approximation. We adapt algorithms and techniques for proving hardness-of-approximation results from related fields to show that these approximation paradigms give rise to a strict hierarchy under common complexity-theoretic assumptions.

This is work in progress joint with Peter Lindner, Christoph Standke and Martin Grohe

 

It is well-known that all relational algebra queries can be evaluated in parallel constant time on an appropriate PRAM model.
We are interested in the efficiency of algorithms for parallel evaluation, that is, in the number of processors or, asymptotically equivalent, in the work required to evaluate a query. Naive evaluation in the parallel setting results in huge (polynomial) bounds on the work of such algorithms and in presentations of the result sets that can be extremely scattered in memory.
In this talk, we first discuss some obstacles for constant time PRAM query evaluation, and present algorithms for relational operators that are considerably more efficient than the naive approaches.
We will then explore three settings, in which efficient sequential query evaluation algorithms exist: acyclic queries, semi-join algebra queries, and join queries — the latter in the worst-case optimal framework.
Given suitable data structures for the database relations, our algorithms are more work-efficient than naive algorithms. In the case of semi-join queries, the work of our algorithms even matches the running time of the best sequential algorithms in the case of semi-join queries, and for join queries it almost matches the running time of worst-case optimal algorithm.
Based on joint work with Jens Keppeler and Thomas Schwentick

19:00: Dinner in the restaurant „Brauhaus Rietkötter“

Friday, 3 March

from 8:30: Early bird coffee

9:00-10:30 Session: Logic

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 easily be introduced on an atomic level, at the cost of higher complexity.

Guarded logics, on the other hand, are generalisations of modal logic, from which they inherit many desirable model-theoretic properties . Guarded team logics are an attempt to combine the features of both logics.

While the expressiveness of the most prominent (non-guarded) team logics is well understood, there are a number of results that do not directly translate to the guarded case. In this talk, we introduce „hybrid team logics“ as a new intermediary and use it to establish some results among these guarded team logics.

During the talk I will present a novel logic called the forward guarded fragment (FGF) that combines ideas of forward and guarded quantification.
The presented logic extends the Description Logic ALC with higher-arity relations in a tamed way: both the knowledge base satisfiability problem and conjunctive query entailment problem are ExpTime-complete, thus having the same complexity as plain ALC. We provide a few intuitions behind these results and discuss an ongoing work towards understanding the model-theory and extensions of FGF.

Semiring semantics generalises the evaluation of first-order formulae by truth values to the evaluation in a commutative semiring. Following the hierarchy from the Boolean semiring over min-max and lattice semirings to absorptive semirings and beyond, we seek to understand the relationship between the algebraic properties and classical model-theoretic results.

In this talk, we investigate to what extent the classical locality theorems due to Hanf and Gaifman generalise to semiring semantics. We prove that Hanf’s theorem generalises to all semirings in which both operations are idempotent, but otherwise fails in many semirings. Regarding Gaifman normal forms, we show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring, and also fails for sentences in certain semirings. Our main result, however, shows that Gaifman normal forms exist in all min-max semirings.

This is joint work with Clotilde Bizière and Erich Grädel.

We consider real Presburger arithmetic — the first-order theory
of the structure of the reals with addition, order, and congruences — and
the extension of first-order logic by threshold and modulo counting quantifiers.
When restricting ourselves to two types of variables, ranging over the
integers and the interval $[0,1)$ respectively, we can show that every formula
is equivalent to a quantifier-free formula whose integer constants are at most
triply exponential in the length of the input formula. Based on this observation,
we can draft a decision procedure that runs in doubly exponential space.
During the process, we introduce quantifiers that range over pairs of variables
and show that they can be reduced to combinations of unary ones; this construction
can be generalised to quantifiers of higher arity.
We also show that real arithmetic, the theory of the reals with addition and
order only, is decidable in exponential space.

10:30-11:00: Coffee break
 

11:00-12:05: Session: Graphs & Sparseness

It is well known that for any given FO sentence, the probability that a randomly chosen relational structure satisfies the sentence converges to 0 or 1 as the structures get larger. This is easily seen to be false if instead of arbitrary relational structures one randomly chooses a string (i.e. a linear order with additional unary predicates), but there is a decidable characterisation of those MSO-sentences for which this probabiliy tends to 0 or 1. We review this result and show how it can be generalised from strings to finite trees. We also review similar characterisations for infinite words.

We give new decomposition theorems for classes of graphs that can be transduced in first-order logic from classes of sparse graphs – more precisely, from classes of bounded expansion and from nowhere dense classes. In both cases, the decomposition takes the form of a single colored rooted tree of bounded depth where, in addition, there can be links between nodes that are not related in the tree. The constraint is that the structure formed by the tree and the links has to be sparse. Using the decomposition theorem for transductions of nowhere dense classes, we show that they admit low-shrubdepth covers of size O(n^ε), where n is the vertex count and ε>0 is any fixed real. This solves an open problem posed by Gajarský et al. (ACM TOCL ’20) and also by Briański et al. (SIDMA ’21).

The k-dimensional Weisfeiler-Leman algorithm (k-WL) iteratively refines a coloring of k-tuples of a graph or relational structure until the refinement process stabilizes. The iteration number of k-WL to distinguish two structures corresponds to the quantifier depth of a sentence in k+1 variable counting logic needed to distinguish the structures. Hence, bounds on the iteration number immediately yield bounds on the quantifier depth.
In this talk, I give an overview on existing and new results bounding the iteration number of k-WL. In particular, I present joint work with Martin Grohe and Daniel Neuen improving the best known lower bound for k-WL on k-ary structures from n^(Ω(k/log k)) to n^(Ω(k)) and establishing the first non-trivial upper bound of O(n^(k-1) log n) for k-WL for every k.

12:05 Option for joint lunch at Q-West (on campus)

AlMoTh Dinner

We will meet for a joint dinner on Thursday, 2 March 2023 at the following place:

Brauhaus Rietkötter
Große Beckstrasse 7
44787 Bochum

Reaching us

Directions to the meeting venue from the tram station „Bochum Ruhr-Universität“ (U35) can be found on this map.
A (towards the end different) path is depicted here: https://informatik.rub.de/weg-zu-mc/

If you travel by car: the parking decks P12 and P13 (Max-Imdahl-Straße, see map above or via Google maps) are located next to the MC building and offer plenty of free parking spots.

Lunch

In addition to the Mensa, you can find

  • the „Q-West“, a café and restaurant on the RUB campus, a few minutes walk from the MC/VC building.
  • the „Rote Bete“, a vegan restaurant on the RUB campus, close to the Mensa

Hotels

Hotel ibis Bochum Zentrum
(approx. 12 minutes with public transport plus 5 minutes walk to the Faculty of Computer Science buildung)

Universitätsstraße 3, 44789 Bochum

Mercure Hotel Bochum City
(approx. 14 minutes with public transport plus 5 minutes walk to the Faculty of Computer Science building)

Massenbergstr. 19-21, 44787 Bochum
phone:  +49 234 9690