Tutorial: Logic for algorithms

The theme of this tutorial is (recent) applications of logic in the design and analysis of efficient algorithms. I will cover the following three topics. Logical techniques in the analysis of generic algorithms Certain generic (families of) algorithms, such as the Weisfeiler-Lehman algorithm for graph isomorphism testing and k-consistency tests for constraint satisfaction problems have logical characterisations. Thus logical techniques can be used to analyse the power of these algorithms and also to prove lower bounds for their running time. Algorithmic meta theorems Algorithmic meta theorems attempt to explain and unify algorithmic results by proving tractability not only for individual problems, but for whole classes of problems. These classes are typically defined in terms of logic. The prototypical example of an algorithmic meta theorem is Courcelle's Theorem, stating that all properties of graphs of bounded tree-width that are definable in monadic second-order logic are decidable in linear time. In the tutorial, I will focus on meta theorems for first-order logic, where by now we have a fairly complete picture of graph classes admitting a nontrivial meta theorem Applications of meta theorems in algorithmic graph structure theory In this last part I will discuss applications of algorithmic meta theorems to problems in algorithmic graph structure theory. By this I mean graph algorithms that use meta theorems to solve tasks for which no other (direct combinatorial) algorithm is known. It is worth noting that the algorithmic problems considered in all three parts are not derived from logic, such as satisfiability or model-checking problems, but "standard" algorithmic problems, often with a strong combinatorial and graph theoretical flavour. On the way, I will introduce the necessary graph theory, including nowhere dense graphs and certain aspects of graph minor theory.

Authors

• Martin Grohe

Keywords

No keywords are indexed for this paper.