Since September 2018, I am a postdoctoral researcher involved in the project Symmetry in Computational Complexity at the Charles University in Prague. Before that, I was a doctoral student at the Institute of Algebra at TU Dresden and defended my thesis on August 14, 2018 with the title "Dichotomies in Constraint Satisfaction: Canonical Functions and Numeric CSPs". I am interested in applications of algebraic and model-theoretic methods to the study of problems from theoretical computer science, such as the study of constraint satisfaction problems over infinite domains.
Discrete Temporal Constraint Satisfaction Problems.Manuel Bodirsky, Barnaby Martin, Antoine Mottet.
In Journal of the ACM 65(2). Abstract
A discrete temporal constraint satisfaction problem is a constraint satisfaction problem (CSP) over the set of integers whose constraint language consists of relations that are first-order definable over the order of the integers. We prove that every discrete temporal CSP is in P or NP-complete, unless it can be formulated as a finite domain CSP, in which case the computational complexity is not known in general.
Topology is relevant (in the dichotomy conjecture for infinite domain constraint satisfaction problems).Manuel Bodirsky, Antoine Mottet, Mirek Olšák, Jakub Opršal, Michael Pinsker, Ross Willard.
Proceedings of LICS 2019.
The algebraic dichotomy conjecture for Constraint Satisfaction Problems (CSPs) of reducts of (infinite) finitely bounded homogeneous structures states that such CSPs are polynomial-time tractable when the model-complete core of the template has a pseudo-Siggers polymorphism, and NP-complete otherwise. One of the important questions related to this conjecture is whether, similarly to the case of finite structures, the condition of having a pseudo-Siggers polymorphism can be replaced by the condition of having polymorphisms satisfying a fixed set of identities of height 1, i.e., identities which do not contain any nesting of functional symbols. We provide a negative answer to this question by constructing for each non-trivial set of height 1 identities a structure whose polymorphisms do not satisfy these identities, but whose CSP is tractable nevertheless. An equivalent formulation of the dichotomy conjecture characterizes tractability of the CSP via the local satisfaction of non-trivial height 1 identities by polymorphisms of the structure. We show that local satisfaction and global satisfaction of non-trivial height 1 identities differ for $\omega$-categorical structures with less than double exponential orbit growth, thereby resolving one of the main open problems in the algebraic theory of such structures.
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP.Manuel Bodirsky, Florent Madelaine, Antoine Mottet.
Proceedings of LICS 2018. Abstract
The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is computationally equivalent to a finite-domain constraint satisfaction problem (CSP); the involved probabilistic reductions were derandomized by Kun using explicit constructions of expander structures. We present a new proof of the reduction to finite-domain CSPs that does not rely on the results of Kun. This new proof allows us to obtain a stronger statement and to verify the more general Bodirsky-Pinsker dichotomy conjecture for CSPs in MMSNP. Our approach uses the fact that every MMSNP sentencedescribes a finite union of CSPs for countable 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.
Seminars, conferences, workshopsFuture events:
- 13-16/01/2020: Computer Science Logic, Barcelona.
- 19-24/07/2020: Mathematics of Constraint Satisfaction, Durham.