Instituts-Logo Logik in der Informatik
Prof. Dr. Nicole Schweikardt

AlMoTh 2018

Algorithmic Model Theory Meeting 2018

announced talks (in alphabetic order)

Christoph Berkholz (HU-Berlin)
The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs

We relate different approaches for proving the unsatisfiability of a system of real polynomial equations over Boolean variables. On the one hand, there are the static proof systems Sherali-Adams and sum-of-squares (a.k.a. Lasserre), which are based on linear and semi-definite programming relaxations. On the other hand, we consider polynomial calculus, which is a dynamic algebraic proof system that models Gröbner basis computations.

Our first result is that sum-of-squares simulates polynomial calculus: any polynomial calculus refutation of degree d can be transformed into a sum-of-squares refutation of degree 2d and only polynomial increase in size. In contrast, our second result shows that this is not the case for Sherali-Adams: there are systems of polynomial equations that have polynomial calculus refutations of degree 3 and polynomial size, but require Sherali-Adams refutations of degree sqrt(n)/log(n) and exponential size.

A preprint is available at

Julian Bitterlich (TU Darmstadt)
finite f-inverse covers do exist

It is shown that each finite inverse monoid admits a finite /F/-inverse cover. This solves a problem that has been formulated in 1991 by Henckell and Rhodes. The main ingredient in the proof is a reformulation of a result by Otto concerning acyclic groupoids that was used to establish a characterisation theorem for GF in finite model theory.

Yijia Chen (Fudan University)
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [Chen and Flum, 2012]. Among others, if p-Halt is in para-AC^0, the parameterized version of the circuit complexity class AC^0, then AC^0, or equivalently, (+,\times)-invariant FO, has a logic. Although it is widely believed that p-Halt\notin para-AC^0, we show that the problem is hard to settle by establishing a connection to the question in classical complexity of whether NE\not\subseteq LINH. Here, LINH denotes the linear time hierarchy.

On the other hand, we suggest an approach toward proving NE\not\subseteq LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson-Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE\not\subseteq LINH. Interestingly, central to this result is a para-AC^0 lower bound for the parameterized model-checking problem for FO on arithmetical structures.

This is joint work with Mortiz Mueller (Barcelona) and Keita Yokoyama (JAIST).

Erich Grädel (RWTH Aachen)
Provenance Analysis Beyond First-Order Logic

In database theory, provenance analysis via interpretations in commutative semiring is a successful method for providing detailed information about why a query answer holds, and aboutthe cost, the confidence, the required access level, or the number of proof trees for a query answer. However, for a long time provenance analysis was largely restricted to positive query languages, such as positive relational algebra, (unions of) conjunctive queries and, to a lesser extent, datalog.

In my talk at AlMoTh 2017 I presented an approach, developed in joint work with Val Tannen, to extend provenance analysis to logics with negation, in particular to full first-order logic, by means of semirings with a duality between provenance tokens for positive and negative facts, and a factorisation of the free semiring N[X] with respect to the ideal generated by this duality. This approach is closely related to a provenance analysis for finite reachability games, giving much more detailed information than just who wins the game.

In this talk I shall discuss the extension of this approach to stronger logics and to infinite games.

Jens Keppeler (HU-Berlin)
Answering UCQs under updates

We investigate the query evaluation problem for fixed queries over fully dynamic databases where tuples can be inserted or deleted. The task is to design a dynamic data structure that can immediately report the new result of a fixed query after every database update. We consider unions of conjunctive queries (UCQs) and focus on the query evaluation tasks testing (decide whether an input tuple a belongs to the query result), enumeration (enumerate, without repetition, all tuples in the query result), and counting (output the number of tuples in the query result).

We identify three increasingly restrictive classes of UCQs which we call t-hierarchical, q-hierarchical, and exhaustively q-hierarchical UCQs. Our main results provide the following dichotomies: If the query's homomorphic core is t-hierarchical (q-hierarchical, exhaustively q-hierarchical), then the testing (enumeration, counting) problem can be solved with constant update time and constant testing time (delay, counting time). Otherwise, it cannot be solved with sublinear update time and sublinear testing time (delay, counting time), unless the OV-conjecture and/or the OMv-conjecture fails.

We also study the complexity of query evaluation in the dynamic setting in the presence of integrity constraints, and we obtain similar dichotomy results for the special case of small domain constraints (i.e., constraints which state that all values in a particular column of a relation belong to a fixed domain of constant size).

In this talk I will present joint work with Christoph Berkholz and Nicole Schweikardt (to appear in Proc. ICDT 2018).

Stephan Kreutzer (TU - Berlin)
On Zero-One and Convergence Laws for Graphs Embeddable on a Fixed Surface

We show that the zero-one law — and even the convergence law — for monadic second-order logic (MSO) fails for all surfaces except the plane on the class of (connected) graphs embeddable on the surface. In addition we show that every rational in [0,1] is the limiting probability of some MSO formula.

This strongly refutes a conjecture by Heinig et al. (2014) who proved a convergence law for planar graphs, and a zero-one law for connected planar graphs, and also identified the so-called gaps of [0,1]; the subintervals that are not limiting probabilities of any MSO formula.

Our proof relies on a combination of methods from structural graph theory — in particular large face-width embeddings of graphs on surfaces — analytic combinatorics, and finite model theory, and several parts of the proof may be of independent interest. In particular, we identify precisely the properties that make the zero-one law work on planar graphs but fail for every other surface.

This is joint work with Albert Atserias and Marc Noy, UPC Barcelona, Catalunia.

Peter Lindner (RWTH Aachen)
Theories of Automatic Structures within the Exponential Time Hierarchy

Automatic Structures are structures that can be described by the means of finite automata. The fundamental result of Khoussainov and Nerode states that every such structure has a decidable first order theory, what makes them of particular interest for algorithmic investigation. So far, the theories of automatic structures that have been encountered in literature and research were complexity-wise mostly located within the lower levels of the exponential time hierarchy, although we also know that there are automatic structures with even non-elementary theories (Grädel, Blumensath). We will present an answer to the question (as posed by Durand-Gasselin and Habermehl), if there are automatic structures in between these two extremes. We construct and investigate a family of automatic structures with the property that for each level of the exponential time hierarchy one of the structures has a theory in close proximity to that level.

Daniel Neuen (RWTH Aachen)
Towards faster isomorphism tests for bounded degree graphs

Luks algorithm to test isomorphism of bounded degree graphs in polynomial time is one of most important results in the context of the Graph Isomorphism Problem in the last four decades and has been used as a basic building block for many other algorithms. In the light of Babai's quasipolynomial time algorithm for general isomorphism testing we investigate the question whether the techniques developed for this algorithm can adapted to the bounded degree setting.

More precisely we consider the String Isomorphism Problem for groups, all of whose composition factors are isomorphic to subgroups of $S_d$, which generalizes (under polynomial time reductions) the isomorphism problem for graphs of maximum degree $d$. We identify a special case of this problem where Babai's techniques can be lifted to obtain more efficient algorithms. To demonstrate the importance of this special we give several applications. Perhaps most interestingly we show that isomorphism of degree $d$ expander graphs can be solved in time $n^{\beta \cdot \log^{c} d}$ (for some constant $c$) where the parameter $\beta$ only depends on the expansion of the input graphs.

Matthias Niewerth (Universität Bayreuth)
MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras

We investigate efficient view maintenance for MSO-definable queries over trees or, more precisely, efficient enumeration of answers to MSO-definable queries over trees which are subject to local updates. We exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log(n)) delay between them. When the tree is updated, the algorithm can avoid repeating expensive preprocessing and restart the enumeration phase within O(log(n)) time. This improves over previous results that require O(log^2(n)) time after updates and have O(log^2(n)) delay. Our algorithms and complexity results in the paper are presented in terms of node-selecting tree automata representing the MSO queries. To present our algorithm, we introduce a balancing scheme for parse trees of forest algebra formulas that is of its own interest to lift results from strings to trees.

Martin Otto (TU Darmstadt)
Modal Logics with Questions

Ciardelli and Roelofsen introduced a neat framework for "inquisitive" logics that can deal with information updates and e.g. naturally extend epistemic modal logics. Semantics for these logics is team-based, with the assignment of informations states (teams, sets of possible worlds) and of possible information updates (sets of information states) in a two-sorted setting that combines first-order features of modal logics with `local' monadic second-order features. The analysis of bisimulation, Ehrenfeucht-Fraisse, and model-theoretic characterisations of the resulting fragments poses some interesting challenges that have been explored in joint work with Ivano Ciardelli.

Gaurav Rattan (RWTH Aachen)
Weisfeiler-Leman Meets Homomorphisms

In this talk, we relate a beautiful theory by Lovász with a popular heuristic algorithm for the graph isomorphism problem, namely the color refinement algorithm and its k-dimensional generalization known as the Weisfeiler-Leman algorithm. We prove that two graphs G and H are indistinguishable by the color refinement algorithm if and only if for all trees T the number hom(T,G) of homomorphisms from T to G equals the corresponding number hom(T,H) for H.

Another characterization of color refinement equivalence (due to Tinhofer) is in terms of fractional isomorphism, that is, the existence of nonnegative real solutions of a natural system of linear equations whose nonnegative integral solutions are precisely the isomorphisms between the graphs. We show that if we drop the nonnegativity constraints, that is, look for arbitrary real solutions, then a solution exists if and only if all paths have the same number of homomorphisms into the two graphs.

Then we lift the tree result to an equivalence between numbers of homomorphisms of graphs of tree width k, the k-dimensional Weisfeiler-Leman algorithm, and the level-k Sherali-Adams relaxation of our linear program. We also obtain a partial result for graphs of pathwidth k and solutions to our system where we drop the nonnegativity constraints.

This is joint work with Holger Dell and Martin Grohe.

Martin Ritzert (RWTH Aachen)
Learning MSO-definable Hypotheses on Strings and Trees

We study the classification problems over string and tree data for hypotheses specified by formulas of monadic second-order logic MSO. The goal is to design learning algorithms that run in time polynomial in the size of the training set, independently of or at least sublinear in the size of the whole data set.

We prove negative as well as positive results. If the data set is an unprocessed string to which our algorithms have local access, then learning in sublinear time is impossible even for hypotheses definable in a small fragment of first- order logic. This argument naturally extends to the case of trees. If we allow for a linear time pre-processing of the string data to build an index data structure, then learning of MSO-definable hypotheses is possible in time polynomial in the size of the training set, independently of the size of the whole data set.

Building on the string result, we get that learning of MSO-definable hypotheses on trees is possible in logarithmic time in the tree size and linear in the size of the training set.

Svenja Schalthöfer (RWTH Aachen)
What is Choiceless Logspace?

One of the most expressive logics within PTIME is Choiceless Polynomial Time (CPT). It is actually still a candidate for a logic that captures all of polynomial time. CPT can also be viewed as a computation model on abstract structures, based on the manipulation of hereditarily finite sets of polynomial size, that avoids explicit choices between indistinguishable elements since these would break symmetries.

What would be an analogous choiceless model on the level of logspace? Can we define a reasonable restriction or variant of CPT that would play a similar role for logspace as CPT does for PTIME?

It turns out that naive restrictions of CPT to sets of logarithmic size result in formalisms that are either too strong (their simulation by traditional algorithms require more than logarithmic space) or too weak (they cannot solve certain natural and important problems in logspace). This is related to the problem what the „size“ of a set in a logspace computation really means. A logspace algorithm can store constantly many objects with a string representation of logarithmic size, but also logarithmically many objects with a constant size representation. It can even handle sets with polynomially many elements in a restricted fashion, such as count the number of elements or write it to the output tape.

In this talk we shall present an isomorphism-invariant computation model on finite structures that is included in both logspace and CPT. Our formalism is based on measuring the size of sets in terms of the logical formulae with which they were constructed, enabling more flexibility in the construction of sets and thus greater expressive power than previous notions of Choiceless Logspace.

Markus Schmid (Uni Trier)
Regular Expressions with Backreferences - Hardness and Tractability of Matching

In the context of this talk, the term ‘backreference’ subsumes mechanisms for defining string repetitions in regular expressions, e.g., the prefix and suffix over {a, b} of the words described by (a + b) ∗ c(a + b) ∗ can be synchronised by using a backreference: in the expression x{(a + b) ∗ }cx, the prefix is stored in variable x and is then referenced to (or repeated) after the occurrence of c. Extending regular expressions with such backreferences is rather common in theoretical and practical applications in various different contexts (in particular, this concept is becoming popular in certain fields of database theory).

Among other negative consequences, using backreferences turns matching of regular expres- sions into an NP-complete problem. The talk surveys some recent results on both the hardness and the tractability of the matching problem for restricted classes of regular expressions with backreferences.

Nicole Schweikardt (HU - Berlin)
Gaifman normal forms for counting extensions of first-order logic

We consider the extension of first-order logic FO by unary counting quantifiers and generalise the notion of Gaifman normal form from FO to this setting. For formulas that use only ultimately periodic counting quantifiers, we provide an algorithm that computes equivalent formulas in Gaifman normal form. We also show that this is not possible for formulas using at least one quantifier that is not ultimately periodic.

Now let d be a degree bound. We show that for any formula phi with arbitrary counting quantifiers, there is a formula gamma in Gaifman normal form that is equivalent to varphi on all finite structures of degree at most d. If the quantifiers of varphi are decidable (decidable in elementary time, ultimately periodic), gamma can be constructed effectively (in elementary time, in worst-case optimal 3-fold exponential time).

For the setting with unrestricted degree we show that by using our Gaifman normal form transformation for formulas with only ultimately periodic counting quantifiers, a known fixed-parameter tractability result for FO on classes of structures of bounded local tree-width can be lifted to the extension of FO with ultimately periodic counting quantifiers, a logic equally expressive as FO+MOD, i.e., first-oder logic with modulo-counting quantifiers.

This is joint work with Dietrich Kuske.

Sebastian Siebertz (University of Warsaw)
First-order interpretations of bounded expansion classes

The notion of bounded expansion captures uniform sparsity of graph classes, and renders various algorithmic problems that are hard in general tractable. In particular, the model checking problem for first-order logic is fixed-parameter tractable over such graph classes. With the aim of generalizing such results to dense graphs, we introduce classes of graphs with structurally bounded expansion, defined as first-order interpretations of classes of bounded expansion. As a first step towards their algorithmic treatment, we provide their characterization analogous to the characterization of classes of bounded expansion via low treedepth decompositions, replacing treedepth by its dense analogue called shrubdepth.

Joint work with Jakub Gajarsky, Stephan Kreutzer, Jaroslav Nesetril, Patrice Ossona de Mendez, Michał Pilipczuk and Szymon Toruńczyk.

Marco Voigt (Max Planck Institute, Saarbrücken)
On Implicit Dependence and Independence between Quantified First-Order Variables

In general, quantification of first-order variables leads to dependencies between universally and existentially quantified variables. Such dependencies become explicit when Skolemization is applied. In this talk, syntactic properties of first-order formulas will be discussed that entail a certain degree of independence of existentially quantified variables from universally quantified variables. The emerging patterns of (in)dependence are more subtle than a strict classification into full dependence vs. full independence as indicated by Henkin-style quantification.

One application of the presented concepts is the definition of novel decidable fragments of first-order sentences that syntactically extend well-known prefix classes: the Bernays– Schönfinkel–Ramsey fragment and the Ackermann fragment. The latter comprise relational ∃ ∗ ∀ ∗ -sentences and relational ∃ ∗ ∀∃ ∗ -sentences, respectively. Instead of restricted quantifier prefixes, the extended fragments are characterized by forbidding certain quantified variables to occur together in atoms.

Decidability of the satisfiability problem for the new fragments can be shown in different ways. One approach proceeds via equivalence-preserving translations into known decidable fragments. In this talk, however, the focus will be on an alternative approach that is based on model-checking games (over possibly infinite structures). The existence of special kinds of winning strategies can be proven, which facilitate the construction of finite models.

Nils Vortmeier (Uni Dortmund)
Reachability and Shortest Distances under Multiple Changes

Recently it was shown that the transitive closure of a directed graph can be updated using first-order formulas after insertions and deletions of single edge in the dynamic descriptive complexity framework by Dong, Su, and Topor, and Patnaik and Immerman. In other words, Reachability is in DynFO.

In this talk we extend the framework to changes of multiple edges at a time, and study the Reachability and Distance queries under these changes. We show that the former problem can be maintained in DynFO(≤, BIT) under changes affecting O(log n / log log n) nodes, for graphs with n nodes. If the update formulas may use a majority quantifier then both Reachability and Distance query can be maintained under changes that affect polylogarithmically many nodes. We also shortly discuss the limitations of our techniques towards showing that distances are in DynFO.

This talk presents joint work with Samir Datta, Anish Mukherjee, and Thomas Zeume.

Daniel Wiebking (RWTH Aachen)
Isomorphism of Bounded Tree Width Graphs

We analyze the structure of graphs of bounded tree width. We show that a graph of tree width at most k can be canonically decomposed into subgraphs which in turn can be canonically embedded into graphs of maximum degree bounded by a polynomial in k.

Combining these graph theoretic insights with novel group theoretic algorithms for the isomorphism problem for graphs of bounded degree, we design a new isomorphism test for graphs of tree width at most k running in time exp(O(k log^c k))poly(n) for some constant c. Using additional insights on the structure of the automorphism groups of graphs of bounded tree width, we extend our techniques to canonization with only a slightly worse running time exp(O(k^2 log k))poly(n). This significantly improves the previously best algorithms for both problems by Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh (FOCS 2014).

André Frochaux
Last modified: 5.03.2018