Monotone Monadic SNP 1: Classical Results and Applications

Talk by Manuel Bodirsky

Location: WIL C115
Start: 1. September 2017 at 1:15 pm
End: 1. September 2017 at 1:45 pm
iCal

The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory, database theory, and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is polynomially equivalent to a finite-domain constraint satisfaction problem (CSP); the clever probabilistic reduction was derandomized by Kun using explicit constructions of expander structures. Several authors have recently announced proofs that every finite-domain CSP is either in P or NP-complete; hence, the same is true for MMSNP.

We present a new proof of the complexity dichotomy for MMSNP. Our new proof has the advantage that it confirms a tractability conjecture by Pinsker and myself that we have made for a much larger class of computational problems. Another advantage is that it does not rely on the intricate expander constructions of Kun (but we do use the finite domain CSP dichotomy). Our approach is based on the fact that every MMSNP sentence can be effectively rewritten into a finite union of CSPs for countably infinite omega-categorical structures; moreover, by a recent result of Hubička and Nešetřil, these structures can be expanded to homogeneous structures with finite relational signature and the Ramsey property. This allows us to use the universal-algebraic approach to study the computational complexity of MMSNP.

In this first part of the talk we will give an introduction to MMSNP with many examples and the classical results, including the Feder-Vardi reduction to finite-domain CSPs, but also usages of MMSNP to classify the complexity of problems that arose in the context of descriptions logics (by Bienvenu, ten Cate, Lutz, Wolter). In the second part, Antoine presents our new analysis of MMSNP sentences using the universal-algebraic approach and Ramsey theory.