Finite and Algorithmic Model Theory

Counting graph homomorphisms and its generalizations such as the Counting Constraint Satisfaction Problem (CSP), its variations, and counting problems in general have been intensively studied since the pioneering work of Valiant. While the complexity of exact counting of graph homomorphisms (Dyer and Greenhill, 2000) and the counting CSP (Bulatov, 2013, and Dyer and Richerby, 2013) is well understood, counting modulo some natural number has attracted considerable interest as well. In their 2015 paper Faben and Jerrum suggested a conjecture stating that counting homomorphisms to a fixed graph H modulo a prime number is hard whenever it is hard to count exactly, unless H has automorphisms of certain kind. In this paper we confirm this conjecture. As a part of this investigation we develop techniques that widen the spectrum of reductions available for modular counting and apply to the general CSP rather than being limited to graph homomorphisms.

In this talk, I will present several questions and results related to uniformisation questions for first-order and monadic second-order theory (MSO). Uniformisation consists in, given a formula $\varphi (X,\overline{p})$, where $\overline{p}$ is a tuple of parameters, to find a formula $\psi (X,\overline{p})$ such that: (1) If $\psi (X,\overline{p})$ holds, then $\varphi (X,\overline{p})$ holds, and (2) is $\varphi (X,\overline{p})$ holds for some $X$, then there exists a unique $X$ such that $psi(X,\overline{p})$ holds. in other words, if a formula has a solution, it is possible to define a unique solution. Of course these questions are parametrised by the logic and the family of models under consideration.

Question pertaining to uniformisation are various. Some logics may admit uniformisation on some models. Some logics may require a more expressive logic for uniformisation. And uniformisability can be seen as a decision procedure.

In this talk, I will survey some results of these forms on finite and infinite structure, for first-order or monadic second-order logic. In particular, I will explain how the algebraic approach can be used to answer some uniformisability questions for MSO logic over countable ordinals. More precisely, it was is known since 1998 by Shelah and Lifshes that MSO is uniformisable in itself over all ordinals shorter than ${\omega }^{\omega }$ (non-uniformly), and that it is not true beyond. I will present recent unpublished new results in collaboration with Alex Rabinovich: (a) there is a single construct that can be added to MSO in order to uniformise MSO over all countable ordinals (the ability to choose a unique cofinal set of order-type omega); and (2) that it is possible to decide, given an MSO formula, whether it can be uniformised in MSO itself over all countable ordinals.

In this talk I gave a brief introduction to algebraic topology intended for the finite model theory audience, leading up to a definition of cohomology. With this in hand, I discussed some potential applications of the ideas in finite model theory. In particular, we look at a collection of partial solutions to a constraint satisfaction problem as a presheaf and identify cohomological obstructions to satisfiability. This allows us to draw conclusions about the expressive power of fixed-point logic extended with operators for solving systems of linear Diophantine equations.

Lovász (1967) showed that two graphs G and H are isomorphic if and only if they are homomorphism indistinguishable over the class of all graphs, i.e. for every graph F, the number of homomorphisms from F to G equals the number of homomorphisms from F to H. Recently, homomorphism indistinguishability over restricted classes of graphs such as bounded treewidth, bounded treedepth and planar graphs, has emerged as a surprisingly powerful framework for capturing diverse equivalence relations on graphs arising from logical equivalence and algebraic equation systems. In this paper, we provide a unified algebraic framework for such results by examining the linear-algebraic and representation-theoretic structure of tensors counting homomorphisms from labelled graphs. The existence of certain linear transformations between such homomorphism tensor subspaces can be interpreted both as homomorphism indistinguishability over a graph class and as feasibility of an equational system. Following this framework, we obtain characterisations of homomorphism indistinguishability over two natural graph classes, namely trees of bounded degree and graphs of bounded pathwidth, answering a question of Dell et al. (2018).

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definable as a least fixed point. The case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the fixed-point definition involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies – strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables further applications such as game synthesis or determining minimal modifications to the game needed to change its outcome. Lastly, we discuss limitations of our approach and present questions that cannot be immediately answered by semiring semantics.

The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs and it is widely used in graph-isomorphism tests. It proceeds by iteratively refining a colouring of vertex tuples. The number of iterations needed to obtain the final output is crucial for the parallelisability of the algorithm.

In my talk, I presented recent work concerning the number of iterations of the WL algorithm on planar graphs. To be more precise, we found that there is a constant $k$ such that every planar graph can be identified (that is, distinguished from every non-isomorphic graph) by the $k$-dimensional WL algorithm within a logarithmic number of iterations. This generalises a result due to Verbitsky (STACS 2007), who proved the same for 3-connected planar graphs.

The number of iterations needed by the $k$-dimensional WL algorithm to identify a graph corresponds to the quantifier depth of a sentence that defines the graph in the $(k+1)$-variable fragment C^k+1 of first-order logic with counting quantifiers. Thus, our result implies that every planar graph is definable with a C^k+1-sentence of logarithmic quantifier depth.

In their classical 1993 paper [CV93] Chaudhuri and Vardi notice that some fundamental database theory results and techniques fail to survive when we try to see query answers as bags (multisets) of tuples rather than as sets of tuples. But disappointingly, almost 30 years after [CV93], the bag-semantics based database theory is still in its infancy. We do not even know whether conjunctive query containment is decidable. And this is not due to lack of interest, but because, in the multiset world, everything suddenly gets discouragingly complicated. In this paper, we try to re-examine, in the bag semantics scenario, the query determinacy problem, which has recently been intensively studied in the set semantics scenario. We show that query determinacy (under bag semantics) is decidable for boolean conjunctive queries and undecidable for unions of such queries (in contrast to the set semantics scenario, where the UCQ case remains decidable even for unary queries). We also show that – surprisingly – for path queries determinacy under bag semantics coincides with determinacy under set semantics (and thus it is decidable).

Over 50 years ago, Lovász proved that two graphs are isomorphic if and only if they admit the same number of homomorphisms from any graph. Other equivalence relations on graphs, such as cospectrality or fractional isomorphism, can be characterized by equality of homomorphism counts from an appropriately chosen class of graphs. Dvořák [J. Graph Theory 2010] showed that taking this class to be the graphs of treewidth at most k yields a tractable relaxation of graph isomorphism known as k-dimensional Weisfeiler-Leman equivalence. Together with a famous result of Cai, Fürer, and Immerman [FOCS 1989], this shows that homomorphism counts from graphs of bounded treewidth do not determine a graph up to isomorphism. Dell, Grohe, and Rattan [ICALP 2018] raised the questions of whether homomorphism counts from planar graphs determine a graph up to isomorphism, and what is the complexity of the resulting relation. We answer the former in the negative by showing that the resulting relation is equivalent to the so-called quantum isomorphism [Mančinska et al, ICALP 2017]. Using this equivalence, we further resolve the latter question, showing that testing whether two graphs have the same number of homomorphisms from any planar graph is, surprisingly, an undecidable problem, and moreover is complete for the class coRE (the complement of recursively enumerable problems). Quantum isomorphism is defined in terms of a one-round, two-prover interactive proof system in which quantum provers, who are allowed to share entanglement, attempt to convince the verifier that the graphs are isomorphic. Our combinatorial proof leverages the quantum automorphism group of a graph, a notion from noncommutative mathematics.

First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates $con{n}_k(x,y,z_1,\mathrm{\dots },z_k)$ that hold true in a graph if there exists a path between (the valuations of) $x$ and $y$ after (the valuations of) $z_1,\mathrm{\dots },z_k$ have been deleted, we obtain separator logic $FO+conn$. We thereby obtain a logic that can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes.

We first study the expressive power of the new logic. We then study the model-checking problem and prove that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor. From the atomic case of connectivity predicates we obtain the first deterministic data structure for connectivity under batched vertex failures where for every fixed number of failures, all operations can be performed in constant time.

This talk is based on the results presented in [2] and [1].

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.

Guarded logics and team logics are logics of imperfect information, in different ways. When combined, some fragments have nice model theoretic properties while still being reasonably expressive. In particular, a technique called “strategy tree transfer” can be applied to show a finite model property for these fragments.

A classical result by Lovasz states that two graphs are isomorphic if and only if they have the same left profile, i.e., they have the same homomorphism counts “from” all graphs. A similar result by Chaudhuri and Vardi states that two graphs are isomorphic if and only if they have the same right profile, in other words, they have the same homomorphism counts “to” all graphs. By restricting the left or right profile to a class of graphs, we have a relaxation of isomorphism. In this talk, I will share some results about what relaxations of isomorphism do/don’t coincide with a restriced left or right profile.

The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed with the objective to allow for simple inclusion of new educational tasks; to pipeline such tasks into more complex exercises; and to allow simple inclusion and cascading of feedback mechanisms. Currently, exercises for many typical automated reasoning workflows for propositional logic, modal logic, and some parts of first-order logic are covered.

In this talk I will address (algorithmic) challenges and solution approaches for building such systems, but also show how the system can be used in logic instruction.

Let $[N]=\{1,\mathrm{\dots },N\}$.

Consider a function

mapping the finite $d$-dimensional euclidean grid lattice with sides of length $N$ to itself.

Suppose the function $f$ is monotone with respect to the standard coordinate-wise partial order on vectors in ${[N]}^d$ , meaning that for all $x,y\in {[N]}^d$, if $x\le y$ then $f(x)\le f(y)$. By Tarski’s (1953) fixed point theorem, such a monotone function $f$ must have a fixed point, i.e., there must exist a point

such that $f(x^{\prime })=x^{\prime }$.

How hard is it to compute such a fixed point when (a) the function $f$ is given to us as a black box and we wish to find a fixed point with a minimum number of queries? or, (b) the function $f$ is given to us explicitly but succinctly using a boolean circuit, with $d\cdot \log (N)$ input gates and $d\cdot \log (N)$ output gates.

For (a), it is easy to see that standard (Kleene) value iteration, starting from the bottom $\overline{1}$ (or, respectively, top $\overline{N}$) of the lattice ${[N]}^d$ requires at most $d\cdot N$ queries to find the least (respectively, greatest) fixed point of $f$. On the other hand, suppose we don’t care which fixed point we compute. Suppose any fixed point will do. Can we do better?

This problem has a number of important applications. In particular, efficient algorithms for this problem (polynomial in both $d$ and $\log (N)$) would imply polynomial time algorithms for supermodular games (a very well studied class of games in economic theory), as well as for both Condon’s simple stochastic games and Shapley’s stochastic games, which are long standing open questions (see [1].)

There is a black-box algorithm due to Dang, Qi, and Ye [2], which requires at most ${\log }^d(N)$ queries to find a fixed point, and uses a combination of recursion and binary search. This algorithm has recently been improved by Fearnley, Palvolgyi, and Savani [3], who give an upper bound of ${\log }^{\lceil \frac{2d}{3}\rceil }(N)$ queries for finding a fixed point. There has also been some even more recent (unpublished) results which improve the exponent further, but it remains exponential in $d$.

What is the best upper bound we can obtain for computing a Tarski fixed point? This is very much an open question. Etessami, Papadimitriou, Rubinstein, and Yannakakis [1] provide a lower bound of $\mathrm{\Omega }({\log }^2(N))$ queries in the black-box model for (a), already for 2-dimensional monotone functions $f:{[N]}^2\to {[N]}^2$. They also show that a total search version of the white-box Tarski problem (b) is in both the complexity classes PPAD and PLS. (It thus follows from recent results that the Tarski problem is also in the total search complexity classes CLS and EOPL.)