VLDB 2026 Research / reviewers in the wild / expert
Manuel Bodirsky
dblp:b/ManuelBodirsky
· DBLP profile ↗
102ranked-venue papers
102as first author
28since 2021 · last 2026
0000-0001-8228-3611ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 87 · 87 first-author · 24 since 2021Artificial intelligence and machine learning · 10 · 10 first-author · 3 since 2021Graphics, computer vision, multimedia, augmented reality and games · 4 · 4 first-author · 1 since 2021Applied, interdisciplinary, general and emerging computing · 4 · 4 first-author · 1 since 2021Databases, data management, data science and information retrieval · 3 · 3 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Hereditary First-Order Logic: the Tractable Quantifier Prefix ClassesabstractMany computational problems can be modelled as the class of all finite structures A that satisfy a fixed first-order sentence ϕ hereditarily, i.e., we require that every (induced) substructure of A satisfies ϕ. We call the corresponding computational problem the hereditary model checking problem for ϕ, and denote it by Her(ϕ). We present a complete description of the quantifier prefixes for ϕ such that Her(ϕ) is in P; we show that for every other quantifier prefix there exists a formula ϕ with this prefix such that Her(ϕ) is coNP-complete. Specifically, we show that if Q is of the form ∀*∃∀* or of the form ∀*∃*, then Her(ϕ) can be solved in polynomial time whenever the quantifier prefix of ϕ is Q. Otherwise, Q contains ∃∃∀ or ∃∀∃ as a subword, and in this case, there is a first-order formula ϕ whose quantifier prefix is Q and Her(ϕ) is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula ϕ whether Her(ϕ) is in P (unless P=NP). Manuel Bodirsky, Santiago Guzmán-Pro |
CSL | 1 |
| 2026 | The Network Satisfaction Problem for Relation Algebras with at Most 4 AtomsabstractAndréka and Maddux classified the relation algebras with at most 3 atoms, and in particular they showed that all of them are representable [Hajnal Andréka and Roger D. Maddux, 1994]. Hirsch and Cristiani showed that the network satisfaction problem (NSP) for each of these algebras is in P or NP-hard [Matteo Cristiani and Robin Hirsch, 2004]. The literature contains many results on representations of relation algebras; in particular, some relation algebras with four atoms are not representable. We extend the result of Cristiani and Hirsch to relation algebras with at most 4 atoms: the NSP is always either in P or NP-hard. To this end, we construct universal, fully universal, or even normal representations for these algebras, whenever possible. Manuel Bodirsky, Moritz Jahn, Simon Knäuer, Matej Konecný, Paul Winkler |
ICALP | 1 |
| 2026 | The Complexity of Finding Coset-Generating Polymorphisms and the Promise MetaproblemabstractWe show that the metaproblem for coset-generating polymorphisms is NP-complete, answering a question of Chen and Larose: given a finite structure, the computational question is whether this structure has a polymorphism of the form (x,y,z) ↦ x y^{-1} z with respect to some group; such operations are also called coset-generating, or heaps. Furthermore, we introduce a promise version of the metaproblem, parametrised by two polymorphism conditions Σ₁ and Σ₂ and defined analogously to the promise constraint satisfaction problem. We give sufficient conditions under which the promise metaproblem for (Σ₁,Σ₂) is in 𝖯 and under which it is NP-hard. In particular, the promise metaproblem is in 𝖯 if Σ₁ states the existence of a Maltsev polymorphism and Σ₂ states the existence of an abelian heap polymorphism - despite the fact that neither the metaproblem for Σ₁ nor the metaproblem for Σ₂ is known to be in 𝖯. We also show that the creation-metaproblem for Maltsev polymorphisms, under the promise that a heap polymorphism exists, is in 𝖯 if and only if there is a uniform polynomial-time algorithm for CSPs with a heap polymorphism. Manuel Bodirsky, Armin Weiß |
ICALP | 1 |
| 2026 | On the Computational Power of Extensional ESOabstractExtensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence Ψ and an input structure A the task is to decide whether there is an extension B of A that satisfies the first-order part of Ψ, i.e., a structure B such that R^A ⊆ R^B for every existentially quantified predicate R of Ψ, and R^A = R^B for every non-quantified predicate R of Ψ. In particular, extensional ESO describes all pre-coloured finite-domain constraint satisfaction problems (CSPs). In this paper we study the computational power of extensional ESO; we ask, for which problems in NP is there a polynomial-time equivalent problem in extensional ESO? One of our main results states that extensional ESO has the same computational power as hereditary first-order logic. We also characterize the computational power of the fragment of extensional ESO with monotone universal first-order part in terms of finitely bounded CSPs. These results suggest a rich computational power of this logic, and we conjecture that extensional ESO captures NP-intermediate problems. We further support this conjecture by showing that extensional ESO can express current candidate NP-intermediate problems such as Graph Isomorphism, and Monotone Dualization (up to polynomial-time equivalence). On the other hand, another main result proves that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESP (unless E=NE). Manuel Bodirsky, Santiago Guzmán-Pro |
LICS | 1 |
| 2026 | A CSP approach to Graph Sandwich ProblemsabstractThe Sandwich Problem (SP) for a graph class \(\mathcal{C}\) is the following computational problem. The input is a pair of graphs \((V,E_1)\) and \((V,E_2)\) where \(E_1 \subseteq E_2\), and the task is to decide whether there is an edge set \(E\) where \(E_1 \subseteq E \subseteq E_2\) such that the graph \((V,E)\) belongs to \(\mathcal{C}\). In this paper we show that many SPs correspond to the constraint satisfaction problem (CSP) of an infinite 2-edge-coloured graph \(H\). We then notice that several known complexity results for SPs also follow from general complexity classifications of infinite-domain CSPs, suggesting a fruitful application of the theory of CSPs to complexity classifications of SPs. We strengthen this evidence by using basic tools from constraint satisfaction theory to propose new complexity results of the SP for several graph classes including line graphs of multigraphs, line graphs of bipartite multigraphs, \(K_k\)-free perfect graphs, and classes described by forbidding finitely many induced subgraphs, such as \(\{I_4,P_4\}\)-free graphs, settling an open problem of Alvarado, Dantas, and Rautenbach (2019). We also construct a graph sandwich problem which is in \(\mathrm{coNP}\), but neither in \(\mathrm{P}\) nor \(\mathrm{coNP}\)-complete (unless \(\mathrm{P}=\mathrm{coNP}\)). Manuel Bodirsky, Santiago Guzmán-Pro |
SODA | 1 |
| 2026 | The Complexity of Resilience for Digraph Queries
Manuel Bodirsky, Zaneta Semanisinová |
STACS | 1 |
| 2026 | Symmetric Linear Arc Monadic Datalog and Gadget ReductionsabstractAbstract A Datalog program solves a constraint satisfaction problem (CSP) if and only if it derives the goal predicate precisely on the unsatisfiable instances of the CSP. There are three Datalog fragments that are particularly important for finite-domain constraint satisfaction: arc monadic Datalog , linear Datalog , and symmetric linear Datalog , each having good computational properties. We consider the fragment of Datalog where we impose all of these restrictions simultaneously, i.e., we study symmetric linear arc monadic (slam) Datalog . We characterise the CSPs that can be solved by a slam Datalog program as those that have a gadget reduction to a particular Boolean constraint satisfaction problem. We also present exact characterisations in terms of a homomorphism duality (which we call unfolded caterpillar duality ), and in universal-algebraic terms (using known minor conditions, namely the existence of quasi Maltsev operations and k -absorptive operations of arity nk , for all $$n,k \ge 1$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>n</mml:mi> <mml:mo>,</mml:mo> <mml:mi>k</mml:mi> <mml:mo>≥</mml:mo> <mml:mn>1</mml:mn> </mml:mrow> </mml:math> ). Our characterisations also imply that the question whether a given finite-domain CSP can be expressed by a slam Datalog program is decidable. Manuel Bodirsky, Florian Starke |
Theory Comput. Syst. | 1 |
| 2026 | Datalog-Expressibility for Monadic and Guarded Second-Order LogicabstractWe characterise the sentences in Monadic Second-Order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class \({\mathcal{C}}\) of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all \(\ell,k\in{\mathbb{N}}\) , there exists a canonical Datalog program \(\Pi\) of width \((\ell,k)\) in the sense of Feder and Vardi. The same characterisations also hold for Guarded Second-Order Logic (GSO), which properly extends MSO. To prove our results, we show that every class \({\mathcal{C}}\) in GSO whose complement is closed under homomorphisms is a finite union of Constraint Satisfaction Problems (CSPs) of \(\omega\) -categorical structures. The intersection of MSO and Datalog is known to contain the class of nested monadically defined queries (Nemodeq) ; likewise, we show that the intersection of GSO and Datalog contains all problems that can be expressed by the more expressive language of nested guarded queries (GQ \({}^{+}\) ) . Yet, by exploiting our results, we can show that neither of the two query languages can serve as a characterisation, as we exhibit a CSP whose complement corresponds to a query in the intersection of MSO and Datalog that is not expressible in GQ \({}^{+}\) . Manuel Bodirsky, Simon Knäuer, Sebastian Rudolph |
ACM Trans. Comput. Log. | 1 |
| 2026 | The Complexity of Resilience Problems via Valued Constraint SatisfactionabstractValued Constraint Satisfaction Problems (VCSPs) constitute a large class of computational optimization problems. It was recently shown that, over finite domains, every VCSP is in P or NP-complete, depending on the admitted cost functions. In this article, we study cost functions over countably infinite domains whose automorphisms form an oligomorphic permutation group. Our results include a hardness condition based on a generalization of pp-constructability as known from classical CSPs and a polynomial-time tractability condition based on the concept of fractional polymorphisms. We then observe that the resilience problem for Unions of Conjunctive Queries (UCQs) studied in database theory, under bag semantics, may be viewed as a special case of the VCSPs that we consider. We obtain a complexity dichotomy for the case of incidence-acyclic UCQs and exemplarily use our methods to determine the complexity of a conjunctive query that has been stated as an open problem in the literature. We conjecture that our hardness and tractability conditions match for resilience problems for UCQs. Further, we obtain a complete dichotomy for resilience problems for two-way regular path queries, under bag semantics. Manuel Bodirsky, Zaneta Semanisinová, Carsten Lutz |
ACM Trans. Comput. Log. | 1 |
| 2025 | Reducing Stochastic Games to Semidefinite ProgrammingabstractWe present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon’s simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming. Manuel Bodirsky, Georg Loho, Mateusz Skomra |
ICALP | 1 |
| 2025 | Symmetric Linear Arc Monadic Datalog and Gadget ReductionsabstractA Datalog program solves a constraint satisfaction problem (CSP) if and only if it derives the goal predicate precisely on the unsatisfiable instances of the CSP. There are three Datalog fragments that are particularly important for finite-domain constraint satisfaction: arc monadic Datalog, linear Datalog, and symmetric linear Datalog, each having good computational properties. We consider the fragment of Datalog where we impose all of these restrictions simultaneously, i.e., we study symmetric linear arc monadic (slam) Datalog. We characterise the CSPs that can be solved by a slam Datalog program as those that have a gadget reduction to a particular Boolean constraint satisfaction problem. We also present exact characterisations in terms of a homomorphism duality (which we call unfolded caterpillar duality), and in universal-algebraic terms (using known minor conditions, namely the existence of quasi Maltsev operations and k-absorptive operations of arity nk, for all n,k ≥ 1). Our characterisations also imply that the question whether a given finite-domain CSP can be expressed by a slam Datalog program is decidable. Manuel Bodirsky, Florian Starke |
ICDT | 1 |
| 2025 | Temporal Valued Constraint Satisfaction Problems
Manuel Bodirsky, Édouard Bonnet, Zaneta Semanisinová |
MFCS | 1 |
| 2025 | Polynomial-Time Tractable Problems over the p-Adic NumbersabstractWe study the computational complexity of fundamental problems over the p-adic numbers {ℚ}_p and the p-adic integers {ℤ}_p. Guépin, Haase, and Worrell [Florent Guépin et al., 2019] proved that checking satisfiability of systems of linear equations combined with valuation constraints of the form v_p(x) = c for p ≥ 5 is NP-complete (both over {ℤ}_p and over {ℚ}_p), and left the cases p = 2 and p = 3 open. We solve their problem by showing that the problem is NP-complete for {ℤ}₃ and for {ℚ}₃, but that it is in P for {ℤ}₂ and for {ℚ}₂. We also present different polynomial-time algorithms for solvability of systems of linear equations in {ℚ}_p with either constraints of the form v_p(x) ≤ c or of the form v_p(x) ≥ c for c ∈ {ℤ}. Finally, we show how our algorithms can be used to decide in polynomial time the satisfiability of systems of (strict and non-strict) linear inequalities over {ℚ} together with valuation constraints v_p(x) ≥ c for several different prime numbers p simultaneously. Manuel Bodirsky, Arno Fehm |
MFCS | 1 |
| 2025 | Forbidden Tournaments and the Orientation Completion ProblemabstractAbstract. For a fixed finite set of finite tournaments [Formula: see text], the [Formula: see text] -free orientation problem asks whether a given finite undirected graph [Formula: see text] has an [Formula: see text] -free orientation, i.e., whether the edges of [Formula: see text] can be oriented so that the resulting digraph does not embed any of the tournaments from [Formula: see text]. We prove that for every [Formula: see text] this problem is in P or NP-complete. Our proof reduces the classification task to a complete complexity classification of the orientation completion problem for [Formula: see text], which is the variant of the problem above where the input is a directed graph instead of an undirected graph, introduced by Bang-Jensen, Huang, and Zhu [ J. Graph Theory, 87 (2018), pp. 285–304]. Our proof uses results from the theory of constraint satisfaction and a result of Agarwal and Kompatscher [ J. Symb. Log., 83 (2018), pp. 395–415] about infinite permutation groups and transformation monoids. Manuel Bodirsky, Santiago Guzmán-Pro |
SIAM J. Discret. Math. | 1 |
| 2024 | The Complexity of Resilience Problems via Valued Constraint Satisfaction ProblemsabstractValued constraint satisfaction problems (VCSPs) constitute a large class of computational optimisation problems. It was shown recently that, over finite domains, every VCSP is in P or NP-complete, depending on the admitted cost functions. In this article, we study cost functions over countably infinite domains whose automorphisms form an oligomorphic permutation group. Our results include a hardness condition based on a generalisation of pp-constructability as known from classical CSPs and a polynomial-time tractability condition based on the concept of fractional polymorphisms. We then observe that the resilience problem for unions of conjunctive queries (UCQs) studied in database theory, under bag semantics, may be viewed as a special case of the VCSPs that we consider. We obtain a complexity dichotomy for the case of incidence-acyclic UCQs and exemplarily use our methods to determine the complexity of a query that had remained open in the literature. Further, we conjecture that our hardness and tractability conditions match for resilience problems for UCQs. Manuel Bodirsky, Zaneta Semanisinová, Carsten Lutz |
LICS | 1 |
| 2024 | Complexity Classification Transfer for CSPs via Algebraic ProductsabstractAbstract. We study the complexity of infinite-domain constraint satisfaction problems (CSPs): our basic setting is that a complexity classification for the CSPs of first-order expansions of a structure [Formula: see text] can be transferred to a classification of the CSPs of first-order expansions of another structure [Formula: see text]. We exploit a product of structures (the algebraic product) that corresponds to the product of the respective polymorphism clones and present a complete complexity classification of the CSPs for first-order expansions of the [Formula: see text]-fold algebraic power of [Formula: see text]. This is proved by various algebraic and logical methods in combination with knowledge of the polymorphisms of the tractable first-order expansions of [Formula: see text] and explicit descriptions of the expressible relations in terms of syntactically restricted first-order formulas. By combining our classification result with general classification transfer techniques, we obtain surprisingly strong new classification results for highly relevant formalisms such as Allen’s Interval Algebra, the [Formula: see text]-dimensional Block Algebra, and the Cardinal Direction Calculus, even if higher-arity relations are allowed. Our results confirm the infinite-domain tractability conjecture for classes of structures that have been difficult to analyze with older methods. For the special case of structures with binary signatures, the results can be substantially strengthened and tightly connected to Ord-Horn formulas; this solves several longstanding open problems from the artificial intelligence (AI) literature. Manuel Bodirsky, Peter Jonsson, Barnaby Martin, Antoine Mottet, Zaneta Semanisinová |
SIAM J. Comput. | 1 |
| 2023 | Network Satisfaction Problems Solved by k-ConsistencyabstractWe show that the problem of deciding for a given finite relation algebra A whether the network satisfaction problem for A can be solved by the k-consistency procedure, for some k ∈ ℕ, is undecidable. For the important class of finite relation algebras A with a normal representation, however, the decidability of this problem remains open. We show that if A is symmetric and has a flexible atom, then the question whether NSP(A) can be solved by k-consistency, for some k ∈ ℕ, is decidable (even in polynomial time in the number of atoms of A). This result follows from a more general sufficient condition for the correctness of the k-consistency procedure for finite symmetric relation algebras. In our proof we make use of a result of Alexandr Kazda about finite binary conservative structures. Manuel Bodirsky, Simon Knäuer |
ICALP | 1 |
| 2023 | On the Descriptive Complexity of Temporal Constraint Satisfaction ProblemsabstractFinite-domain constraint satisfaction problems are either solvable by Datalog or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a universal-algebraic minor condition. For infinite-domain constraint satisfaction problems (CSPs), the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (ℚ;<); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the mod-2 rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs. Manuel Bodirsky, Jakub Rydval |
J. ACM | 1 |
| 2022 | The Complexity of Network Satisfaction Problems for Symmetric Relation Algebras with a Flexible AtomabstractRobin Hirsch posed in 1996 the Really Big Complexity Problem: classify the computational complexity of the network satisfaction problem for all finite relation algebras A. We provide a complete classification for the case that A is symmetric and has a fexible atom; in this case, the problem is NP-complete or in P. The classification task can be reduced to the case where A is integral. If a finite integral relation algebra has a flexible atom, then it has a normal representation B. We can then study the computational complexity of the network satisfaction problem of A using the universal-algebraic approach, via an analysis of the polymorphisms of B. We also use a Ramsey-type result of Nešetřil and Rödl and a complexity dichotomy result of Bulatov for conservative finite-domain constraint satisfaction problems. Manuel Bodirsky, Simon Knäuer |
J. Artif. Intell. Res. | 1 |
| 2022 | Tractable Combinations of Temporal CSPsabstractThe constraint satisfaction problem (CSP) of a first-order theory T is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of T. We study the computational complexity of CSP$(T_1 \cup T_2)$ where $T_1$ and $T_2$ are theories with disjoint finite relational signatures. We prove that if $T_1$ and $T_2$ are the theories of temporal structures, i.e., structures where all relations have a first-order definition in $(Q;<)$, then CSP$(T_1 \cup T_2)$ is in P or NP-complete. To this end we prove a purely algebraic statement about the structure of the lattice of locally closed clones over the domain $Q$ that contain Aut$(Q;<)$. Manuel Bodirsky, Johannes Greiner, Jakub Rydval |
Log. Methods Comput. Sci. | 1 |
| 2022 | Piecewise Linear Valued CSPs Solvable by Linear Programming RelaxationabstractValued constraint satisfaction problems (VCSPs) are a large class of combinatorial optimisation problems. The computational complexity of VCSPs depends on the set of allowed cost functions in the input. Recently, the computational complexity of all VCSPs for finite sets of cost functions over finite domains has been classified. Many natural optimisation problems, however, cannot be formulated as VCSPs over a finite domain. We initiate the systematic investigation of the complexity of infinite-domain VCSPs with piecewise linear homogeneous cost functions. Such VCSPs can be solved in polynomial time if the cost functions are improved by fully symmetric fractional operations of all arities. We show this by reducing the problem to a finite-domain VCSP which can be solved using the basic linear program relaxation. It follows that VCSPs for submodular PLH cost functions can be solved in polynomial time; in fact, we show that submodular PLH functions form a maximally tractable class of PLH cost functions. Manuel Bodirsky, Marcello Mamino, Caterina Viola |
ACM Trans. Comput. Log. | 1 |
| 2021 | Network Satisfaction for Symmetric Relation Algebras with a Flexible AtomabstractRobin Hirsch posed in 1996 the Really Big Complexity Problem: classify the computational complexity of the network satisfaction problem for all finite relation algebras A. We provide a complete classification for the case that A is symmetric and has a flexible atom; the problem is in this case NP-complete or in P. If a finite integral relation algebra has a flexible atom, then it has a normal representation B. We can then study the computational complexity of the network satisfaction problem of A using the universal-algebraic approach, via an analysis of the polymorphisms of B. We also use a Ramsey-type result of Nešetřil and Rödl and a complexity dichotomy result of Bulatov for conservative finite-domain constraint satisfaction problems. Manuel Bodirsky, Simon Knäuer |
AAAI | 1 |
| 2021 | Datalog-Expressibility for Monadic and Guarded Second-Order Logic
Manuel Bodirsky, Simon Knäuer, Sebastian Rudolph |
ICALP | 1 |
| 2021 | Tractable Combinations of Theories via Sampling
Manuel Bodirsky, Johannes Greiner |
JELIA | 1 |
| 2021 | Canonical Polymorphisms of Ramsey Structures and the Unique Interpolation PropertyabstractConstraint satisfaction problems for first-order reducts of finitely bounded homogeneous structures form a large class of computational problems that might exhibit a complexity dichotomy, P versus NP-complete. A powerful method to obtain polynomial-time tractability results for such CSPs is a certain reduction to polynomial-time tractable finite-domain CSPs de-fined over k-types, for a sufficiently large k. We give sufficient conditions when this method can be applied and illustrate how to use the general results to prove a new complexity dichotomy for first-order expansions of the basic relations of the spatial reasoning formalism RCC5. Manuel Bodirsky, Bertalan Bodor |
LICS | 1 |
| 2021 | On Logics and Homomorphism ClosureabstractPredicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characterizing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomorphism closure (homclosure) of the class of all (finite or arbitrary) models of logical sentences: membership of structures in a sentence's homclosure; sentence homclosedness; homclosure characterizability in a logic; normal forms for homclosed sentences in certain logics. For a wide variety of fragments of first- and second-order predicate logic, we clarify these problems' computational properties. Manuel Bodirsky, Thomas Feller 0001, Simon Knäuer, Sebastian Rudolph |
LICS | 1 |
| 2021 | Projective clone HomomorphismsabstractAbstract It is known that a countable $\omega $ -categorical structure interprets all finite structures primitively positively if and only if its polymorphism clone maps to the clone of projections on a two-element set via a continuous clone homomorphism. We investigate the relationship between the existence of a clone homomorphism to the projection clone, and the existence of such a homomorphism which is continuous and thus meets the above criterion. Manuel Bodirsky, Michael Pinsker, András Pongrácz |
J. Symb. Log. | 1 |
| 2021 | A Proof of the Algebraic Tractability Conjecture for Monotone Monadic SNPabstractThe logic MMSNP is a restricted fragment of existential second-order logic which can 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. The new universal-algebraic 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 sentence describes 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. Manuel Bodirsky, Florent R. Madelaine, Antoine Mottet |
SIAM J. Comput. | 1 |
| 2020 | Hardness of Network Satisfaction for Relation Algebras with Normal Representations
Manuel Bodirsky, Simon Knäuer |
RAMiCS | 1 |
| 2020 | ASNP: A Tame Fragment of Existential Second-Order Logic
Manuel Bodirsky, Simon Knäuer, Florian Starke |
CiE | 1 |
| 2020 | Temporal Constraint Satisfaction Problems in Fixed-Point LogicabstractFinite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q; <); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs. Manuel Bodirsky, Wied Pakusa, Jakub Rydval |
LICS | 1 |
| 2020 | The Complexity of Combinations of Qualitative Constraint Satisfaction ProblemsabstractThe CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of $\mathrm{CSP}(T_1 \cup T_2)$ under the assumption that $\mathrm{CSP}(T_1)$ and $\mathrm{CSP}(T_2)$ are decidable (or polynomial-time decidable). We show that for a large class of $\omega$-categorical theories $T_1, T_2$ the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of $\mathrm{CSP}(T_1 \cup T_2)$ (unless P=NP). Manuel Bodirsky, Johannes Greiner |
Log. Methods Comput. Sci. | 1 |
| 2019 | Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems)abstractThe 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 nontrivial height 1 identities by polymorphisms of the structure. We show that local satisfaction and global satisfaction of nontrivial height 1 identities differ for ω -categorical structures with less than double exponential orbit growth, thereby resolving one of the main open problems in the algebraic theory of such structures. Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard |
LICS | 1 |
| 2019 | Constraint Satisfaction Problems for Reducts of Homogeneous GraphsabstractFor $n\geq 3$, let $(H_n, E)$ denote the $n$th Henson graph, i.e., the unique countable homogeneous graph with exactly those finite graphs as induced subgraphs that do not embed the complete graph on $n$ vertices. We show that for all structures $\Gamma$ with domain $H_n$ whose relations are first-order definable in $(H_n,E)$ the constraint satisfaction problem for $\Gamma$ either is in P or is NP-complete. We moreover show a similar complexity dichotomy for all structures whose relations are first-order definable in a homogeneous graph whose reflexive closure is an equivalence relation. Together with earlier results, in particular for the random graph, this completes the complexity classification of constraint satisfaction problems of structures first-order definable in countably infinite homogeneous graphs: all such problems are either in P or NP-complete. Manuel Bodirsky, Barnaby Martin, Michael Pinsker, András Pongrácz |
SIAM J. Comput. | 1 |
| 2018 | Finite Relation Algebras with Normal Representations
Manuel Bodirsky |
RAMiCS | 1 |
| 2018 | Submodular Functions and Valued Constraint Satisfaction Problems over Infinite DomainsabstractValued constraint satisfaction problems (VCSPs) are a large class of combinatorial optimisation problems. It is desirable to classify the computational complexity of VCSPs depending on a fixed set of allowed cost functions in the input. Recently, the computational complexity of all VCSPs for finite sets of cost functions over finite domains has been classified in this sense. Many natural optimisation problems, however, cannot be formulated as VCSPs over a finite domain. We initiate the systematic investigation of infinite-domain VCSPs by studying the complexity of VCSPs for piecewise linear homogeneous cost functions. We show that such VCSPs can be solved in polynomial time when the cost functions are additionally submodular, and that this is indeed a maximally tractable class: adding any cost function that is not submodular leads to an NP-hard VCSP. Manuel Bodirsky, Marcello Mamino, Caterina Viola |
CSL | 1 |
| 2018 | Classification Transfer for Qualitative Reasoning ProblemsabstractWe study formalisms for temporal and spatial reasoning in the modern context of Constraint Satisfaction Problems (CSPs). We show how questions on the complexity of their subclasses can be solved using existing results via the powerful use of primitive positive (pp) interpretations and pp-homotopy. We demonstrate the methodology by giving a full complexity classification of all constraint languages that are first-order definable in Allen's Interval Algebra and contain the basic relations (s) and (f). In the case of the Rectangle Algebra we answer in the affirmative the old open question as to whether ORD-Horn is a maximally tractable subset among the (disjunctive, binary) relations. We then generalise our results for the Rectangle Algebra to the r-dimensional Block Algebra. Manuel Bodirsky, Peter Jonsson, Barnaby Martin, Antoine Mottet |
IJCAI | 1 |
| 2018 | A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNPabstractThe 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 Bodirsky-Pinsker dichotomy conjecture for CSPs in MMSNP. Our approach uses the fact that every MMSNP sentence describes a finite union of CSPs for countably infinite ω-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. Manuel Bodirsky, Florent R. Madelaine, Antoine Mottet |
LICS | 1 |
| 2018 | The Complexity of Disjunctive Linear Diophantine ConstraintsabstractWe study the Constraint Satisfaction Problem CSP( A), where A is first-order definable in (Z;+,1) and contains +. We prove such problems are either in P or NP-complete. Manuel Bodirsky, Barnaby Martin, Marcello Mamino, Antoine Mottet |
MFCS | 1 |
| 2018 | Discrete Temporal Constraint Satisfaction ProblemsabstractA 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. Manuel Bodirsky, Barnaby Martin, Antoine Mottet |
J. ACM | 1 |
| 2018 | A Dichotomy for First-Order Reducts of Unary StructuresabstractMany natural decision problems can be formulated as constraint satisfaction problems for reducts $\mathbb{A}$ of finitely bounded homogeneous structures. This class of problems is a large generalisation of the class of CSPs over finite domains. Our first result is a general polynomial-time reduction from such infinite-domain CSPs to finite-domain CSPs. We use this reduction to obtain new powerful polynomial-time tractability conditions that can be expressed in terms of the topological polymorphism clone of $\mathbb{A}$. Moreover, we study the subclass $\mathcal{C}$ of CSPs for structures $\mathbb{A}$ that are reducts of a structure with a unary language. Also this class $\mathcal{C}$ properly extends the class of all finite-domain CSPs. We apply our new tractability conditions to prove the general tractability conjecture of Bodirsky and Pinsker for reducts of finitely bounded homogeneous structures for the class $\mathcal{C}$. Manuel Bodirsky, Antoine Mottet |
Log. Methods Comput. Sci. | 1 |
| 2018 | The universal homogeneous binary treeabstractA partial order is called semilinear if the upper bounds of each element are linearly ordered and any two elements have a common upper bound. There exists, up to isomorphism, a unique countable existentially closed semilinear order, which we denote by |$(\mathbb{S}_{2};\leq )$|. We study the reducts of |$(\mathbb{S}_{2};\leq )$|, that is, the relational structures with domain |$\mathbb{S}_{2}$|, all of whose relations are first-order definable in |$(\mathbb{S}_{2};\leq )$|. Our main result is a classification of the model-complete cores of the reducts of |$\mathbb{S}_{2}$|. From this, we also obtain a classification of reducts up to first-order interdefinability, which is equivalent to a classification of all subgroups of the full symmetric group on |$\mathbb{S}_{2}$| that contain the automorphism group of |$(\mathbb{S}_{2};\leq )$| and are closed with respect to the pointwise convergence topology. Manuel Bodirsky, David Bradley-Williams, Michael Pinsker, András Pongrácz |
J. Log. Comput. | 1 |
| 2018 | Tropically Convex Constraint Satisfaction
Manuel Bodirsky, Marcello Mamino |
Theory Comput. Syst. | 1 |
| 2017 | A Model-Theoretic View on Qualitative Constraint ReasoningabstractQualitative reasoning formalisms are an active research topic in artificial intelligence. In this survey we present a model-theoretic perspective on qualitative constraint reasoning and explain some of the basic concepts and results in an accessible way. In particular, we discuss the significance of omega-categoricity for qualitative reasoning, of primitive positive interpretations for complexity analysis, and of Datalog as a unifying language for describing local consistency algorithms. Manuel Bodirsky, Peter Jonsson |
J. Artif. Intell. Res. | 1 |
| 2017 | The Complexity of Phylogeny Constraint Satisfaction ProblemsabstractWe systematically study the computational complexity of a broad class of computational problems in phylogenetic reconstruction. The class contains, for example, the rooted triple consistency problem, forbidden subtree problems, the quartet consistency problem, and many other problems studied in the bioinformatics literature. The studied problems can be described as constraint satisfaction problems , where the constraints have a first-order definition over the rooted triple relation. We show that every such phylogeny problem can be solved in polynomial time or is NP-complete. On the algorithmic side, we generalize a well-known polynomial-time algorithm of Aho, Sagiv, Szymanski, and Ullman for the rooted triple consistency problem. Our algorithm repeatedly solves linear equation systems to construct a solution in polynomial time. We then show that every phylogeny problem that cannot be solved by our algorithm is NP-complete. Our classification establishes a dichotomy for a large class of infinite structures that we believe is of independent interest in universal algebra, model theory, and topology. The proof of our main result combines results and techniques from various research areas: a recent classification of the model-complete cores of the reducts of the homogeneous binary branching C-relation, Leeb’s Ramsey theorem for rooted trees, and universal algebra. Manuel Bodirsky, Peter Jonsson, Van Trung Pham |
ACM Trans. Comput. Log. | 1 |
| 2016 | Constraint Satisfaction Problems for Reducts of Homogeneous Graphs
Manuel Bodirsky, Barnaby Martin, Michael Pinsker, András Pongrácz |
ICALP | 1 |
| 2016 | Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfactionabstractMany natural decision problems can be formulated as constraint satisfaction problems for reducts of finitely bounded homogeneous structures. This class of problems is a large generalisation of the class of CSPs over finite domains. Our first result is a general polynomial-time reduction from such infinite-domain CSPs to finite-domain CSPs. We use this reduction to obtain new powerful polynomial-time tractability conditions that can be expressed in terms of topological polymorphism clones. Moreover, we study the subclass C of CSPs for structures that are first-order definable over equality with parameters. Also this class C properly extends the class of all finite-domain CSPs. We show that the tractability conjecture for reducts of finitely bounded homogeneous structures is for C equivalent to the finite-domain tractability conjecture. Manuel Bodirsky, Antoine Mottet |
LICS | 1 |
| 2016 | The Complexity of Phylogeny Constraint SatisfactionabstractWe systematically study the computational complexity of a broad class of computational problems in phylogenetic reconstruction. The class contains for example the rooted triple consistency problem, forbidden subtree problems, the quartet consistency problem, and many other problems studied in the bioinformatics literature. The studied problems can be described as constraint satisfaction problems where the constraints have a first-order definition over the rooted triple relation. We show that every such phylogeny problem can be solved in polynomial time or is NP-complete. On the algorithmic side, we generalize a well-known polynomial-time algorithm of Aho, Sagiv, Szymanski, and Ullman for the rooted triple consistency problem. Our algorithm repeatedly solves linear equation systems to construct a solution in polynomial time. We then show that every phylogeny problem that cannot be solved by our algorithm is NP-complete. Our classification establishes a dichotomy for a large class of infinite structures that we believe is of independent interest in universal algebra, model theory, and topology. The proof of our main result combines results and techniques from various research areas: a recent classification of the model-complete cores of the reducts of the homogeneous binary branching C-relation, Leeb’s Ramsey theorem for rooted trees, and universal algebra. Manuel Bodirsky, Peter Jonsson, Van Trung Pham |
STACS | 1 |
| 2016 | Distance constraint satisfaction problems
Manuel Bodirsky, Víctor Dalmau, Barnaby Martin, Antoine Mottet, Michael Pinsker |
Inf. Comput. | 1 |
| 2016 | The Reducts of the homogeneous Binary Branching C-RelationabstractAbstract Let ( $\rm L$ ;C) be the (up to isomorphism unique) countable homogeneous structure carrying a binary branching C-relation. We study the reducts of ( $\rm L$ ;C), i.e., the structures with domain $\rm L$ that are first-order definable in ( $\rm L$ ;C). We show that up to existential interdefinability, there are finitely many such reducts. This implies that there are finitely many reducts up to first-order interdefinability, thus confirming a conjecture of Simon Thomas for the special case of ( $\rm L$ ;C). We also study the endomorphism monoids of such reducts and show that they fall into four categories. Manuel Bodirsky, Peter Jonsson, Van Trung Pham |
J. Symb. Log. | 1 |
| 2016 | Reducts of Structures and Maximal-Closed Permutation GroupsabstractAbstract Answering a question of Junker and Ziegler, we construct a countable first order structure which is not ω-categorical, but does not have any proper nontrivial reducts, in either of two senses (model-theoretic, and group-theoretic). We also construct a strongly minimal set which is not ω-categorical but has no proper nontrivial reducts in the model-theoretic sense. Manuel Bodirsky, Dugald Macpherson |
J. Symb. Log. | 1 |
| 2015 | Constraint Satisfaction Problems over the Integers with Successor
Manuel Bodirsky, Barnaby Martin, Antoine Mottet |
ICALP (1) | 1 |
| 2015 | The Complexity of Constraint Satisfaction Problems (Invited Talk)abstractThe tractability conjecture for constraint satisfaction problems (CSPs) describes the constraint languages over a finite domain whose CSP can be solved in polynomial-time. The precise formulation of the conjecture uses basic notions from universal algebra. In this talk, we give a short introduction to the universal-algebraic approach to the study of the complexity of CSPs. Finally, we discuss attempts to generalise the tractability conjecture to large classes of constraint languages over infinite domains, in particular for constraint languages that arise in qualitative temporal and spatial reasoning. Manuel Bodirsky |
STACS | 1 |
| 2015 | Schaefer's Theorem for GraphsabstractSchaefer's theorem is a complexity classification result for so-called Boolean constraint satisfaction problems : it states that every Boolean constraint satisfaction problem is either contained in one out of six classes and can be solved in polynomial time, or is NP-complete. We present an analog of this dichotomy result for the propositional logic of graphs instead of Boolean logic. In this generalization of Schaefer's result, the input consists of a set W of variables and a conjunction Φ of statements (“constraints”) about these variables in the language of graphs, where each statement is taken from a fixed finite set Ψ of allowed quantifier-free first-order formulas; the question is whether Φ is satisfiable in a graph. We prove that either Ψ is contained in one out of 17 classes of graph formulas and the corresponding problem can be solved in polynomial time, or the problem is NP-complete. This is achieved by a universal-algebraic approach, which in turn allows us to use structural Ramsey theory. To apply the universal-algebraic approach, we formulate the computational problems under consideration as constraint satisfaction problems (CSPs) whose templates are first-order definable in the countably infinite random graph. Our method for classifying the computational complexity of those CSPs is based on a Ramsey-theoretic analysis of functions acting on the random graph, and we develop general tools suitable for such an analysis which are of independent mathematical interest. Manuel Bodirsky, Michael Pinsker |
J. ACM | 1 |
| 2013 | Datalog and constraint satisfaction with infinite templates
Manuel Bodirsky, Víctor Dalmau |
J. Comput. Syst. Sci. | 1 |
| 2013 | Decidability of definabilityabstractAbstract For a fixed countably infinite structure Γ with finite relational signature τ, we study the following computational problem: input are quantifier-free τ-formulas ϕ0, ϕ1, …, ϕn that define relations R0, R1, …, Rn over Γ. The question is whether the relation R0 is primitive positive definable from R1, …, Rn, i.e., definable by a first-order formula that uses only relation symbols for R1, …, Rn, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden). We show decidability of this problem for all structures Γ that have a first-order definition in an ordered homogeneous structure Δ with a finite relational signature whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples of structures Γ with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics. Manuel Bodirsky, Michael Pinsker, Todor Tsankov |
J. Symb. Log. | 1 |
| 2013 | Complexity of existential positive first-order logicabstractLet Γ be a (not necessarily finite) structure with a finite relational signature. We prove that deciding whether a given existential positive sentence holds in Γ is in LogSpace or complete for the class CSP(Γ)NP under deterministic polynomial-time many-one reductions. Here, CSP(Γ)NP is the class of problems that can be reduced to the constraint satisfaction problem of Γ under non-deterministic polynomial-time many-one reductions. Manuel Bodirsky, Miki Hermann, Florian Richoux |
J. Log. Comput. | 1 |
| 2013 | Constraint satisfaction tractability from semi-lattice operations on infinite setsabstractA famous result by Jeavons, Cohen, and Gyssens shows that every Constraint Satisfaction Problem (CSP) where the constraints are preserved by a semi-lattice operation can be solved in polynomial time. This is one of the basic facts for the so-called universal algebraic approach to a systematic theory of tractability and hardness in finite domain constraint satisfaction. Not surprisingly, the theorem of Jeavons et al. fails for arbitrary infinite domain CSPs. Many CSPs of practical interest, though, and in particular those CSPs that are motivated by qualitative reasoning calculi from artificial intelligence, can be formulated with constraint languages that are rather well-behaved from a model-theoretic point of view. In particular, the automorphism group of these constraint languages tends to be large in the sense that the number of orbits of n -subsets of the automorphism group is bounded by some function in n . In this article we present a generalization of the theorem by Jeavons et al. to infinite domain CSPs where the number of orbits of n -subsets grows subexponentially in n , and prove that preservation under a semi-lattice operation for such CSPs implies polynomial-time tractability. Unlike the result of Jeavons et al., this includes CSPs that cannot be solved by Datalog. Manuel Bodirsky, Dugald Macpherson, Johan Thapper |
ACM Trans. Comput. Log. | 1 |
| 2012 | The complexity of surjective homomorphism problems - a survey
Manuel Bodirsky, Jan Kára, Barnaby Martin |
Discret. Appl. Math. | 1 |
| 2012 | Tractable Set ConstraintsabstractMany fundamental problems in artificial intelligence, knowledge representation, and verification involve reasoning about sets and relations between sets and can be modeled as set constraint satisfaction problems (set CSPs). Such problems are frequently intractable, but there are several important set CSPs that are known to be polynomial-time tractable. We introduce a large class of set CSPs that can be solved in quadratic time. Our class, which we call EI, contains all previously known tractable set CSPs, but also some new ones that are of crucial importance for example in description logics. The class of EI set constraints has an elegant universal-algebraic characterization, which we use to show that every set constraint language that properly contains all EI set constraints already has a finite sublanguage with an NP-hard constraint satisfaction problem. Manuel Bodirsky, Martin Hils |
J. Artif. Intell. Res. | 1 |
| 2012 | Horn versus full first-order: Complexity dichotomies in algebraic constraint satisfactionabstractWe study techniques for deciding the computational complexity of infinite-domain constraint satisfaction problems. For certain basic algebraic structures Δ, we prove definability theorems of the following form: for every first-order expansion Γ of Δ, either Γ has a quantifier-free Horn definition in Δ, or there is an element d of Γ such that all non-empty relations in Γ contain a tuple of the form (d,…,d), or all relations with a first-order definition in Δ have a primitive positive definition in Γ. The results imply that several families of constraint satisfaction problems exhibit a complexity dichotomy: the problems are either polynomial-time solvable or NP-hard depending on the choice of the allowed relations. As concrete examples, we investigate fundamental algebraic constraint satisfaction problems. The first class consists of all relational structures with a first-order definition in (ℚ; +) that contain the relation {(x, y, z) ∈ ℚ3 | x + y = z}. The second class is the affine variant of the first class. In both cases, we obtain full dichotomies by utilizing our general methods. Manuel Bodirsky, Peter Jonsson, Timo von Oertzen |
J. Log. Comput. | 1 |
| 2012 | On the Complexity of MMSNPabstractMonotone monadic strict NP (MMSNP) is a class of computational problems that is closely related to the class of constraint satisfaction problems for constraint languages over finite domains. It is known that one of those classes has a complexity dichotomy if and only if the other class has. Whereas the dichotomy conjecture has been verified for several subclasses of constraint satisfaction problems, little is known about the the computational complexity for subclasses of MMSNP. In this paper we completely classify the complexity of MMSNP for the case where the obstructions are monochromatic and where loops in the input are forbidden. That is, we determine the computational complexity of natural partition problems of the following type. For fixed sets of finite structures ${\cal S}_1, \dots, {\cal S}_k$, decide whether a given loopless structure can be vertex-partitioned into k parts such that for each $i \leq k$ none of the structures in ${\cal S}_i$ is homomorphic to the ith part. Manuel Bodirsky, Hubie Chen, Tomás Feder |
SIAM J. Discret. Math. | 1 |
| 2011 | Tractable Set ConstraintsabstractMany fundamental problems in artificial intelligence, knowledge representation, and verification involve reasoning about sets and relations between sets and can be modeled as set constraint satisfaction problems (set CSPs). Such problems are frequently intractable, but there are several important set CSPs that are known to be polynomial-time tractable. We introduce a large class of set CSPs that can be solved in quadratic time. Our class, which we call EI, contains all previously known tractable set CSPs, but also some new ones that are of crucial importance for example in description logics. The class of EI set constraints has an elegant universal-algebraic characterization, which we use to show that every set constraint language that properly contains all EI set constraints already has a finite sublanguage with an NP-hard constraint satisfaction problem. Manuel Bodirsky, Martin Hils, Alex Krimkevitch |
IJCAI | 1 |
| 2011 | RCC8 Is Polynomial on Networks of Bounded TreewidthabstractWe construct an homogeneous (and ω-categorical) representation of the relation algebra RCC8, which is one of the fundamental formalisms for spatial reasoning. As a consequence we obtain that the network consistency problem for RCC8 can be solved in polynomial time for networks of bounded treewidth. Manuel Bodirsky, Stefan Wölfl 0001 |
IJCAI | 1 |
| 2011 | Decidability of DefinabilityabstractFor a fixed infinite structure Γ with finite signature τ, we study the following computational problem: input are quantifier-free first-order τ-formulas φ0, φ1,..., φnthat define relations R0, R1,..., Rnover Γ. The question is whether the relation R0is primitive positive definable from R1,..., Rn, i.e., definable by a first-order formula that uses only relation symbols for R1,..., Rn, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden). We show decidability of this problem for all structures Γ that have a first-order definition in an ordered homogeneous structure Δ with a finite language whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples for structures Γ with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics. Manuel Bodirsky, Michael Pinsker, Todor Tsankov |
LICS | 1 |
| 2011 | Schaefer's theorem for graphsabstractSchaefer's theorem is a complexity classification result for so-called Boolean constraint satisfaction problems: it states that every Boolean constraint satisfaction problem is either contained in one out of six classes and can be solved in polynomial time, or is NP-complete. We present an analog of this dichotomy result for the propositional logic of graphs instead of Boolean logic. In this generalization of Schaefer's result, the input consists of a set W of variables and a conjunction Phi of statements ("constraints") about these variables in the language of graphs, where each statement is taken from a fixed finite set Psi of allowed quantifier-free first-order formulas; the question is whether Phi is satisfiable in a graph. Manuel Bodirsky, Michael Pinsker |
STOC | 1 |
| 2011 | Boltzmann Samplers, Pólya Theory, and Cycle PointingabstractWe introduce a general method to count unlabeled combinatorial structures and to efficiently generate them at random. The approach is based on pointing unlabeled structures in an “unbiased” way so that a structure of size n gives rise to n pointed structures. We extend Pólya theory to the corresponding pointing operator and present a random sampling framework based on both the principles of Boltzmann sampling and Pólya operators. All previously known unlabeled construction principles for Boltzmann samplers are special cases of our new results. Our method is illustrated in several examples: in each case, we provide enumerative results and efficient random samplers. The approach applies to unlabeled families of plane and nonplane unrooted trees, and tree-like structures in general, but also to families of graphs (such as cacti graphs and outerplanar graphs) and families of planar maps. Manuel Bodirsky, Éric Fusy, Mihyun Kang, Stefan Vigerske |
SIAM J. Comput. | 1 |
| 2011 | Limit Behavior of Locally Consistent Constraint Satisfaction ProblemsabstractAn instance of a constraint satisfaction problem (CSP) is variable [Formula: see text]- consistent if any subinstance with at most [Formula: see text] variables has a solution. For a fixed constraint language [Formula: see text], [Formula: see text] is the largest ratio such that any variable [Formula: see text]-consistent instance has a solution that satisfies at least a fraction of [Formula: see text] of the constraints. We provide an expression for the limit [Formula: see text], and show that this limit coincides with the corresponding limit for constraint [Formula: see text]- consistent instances, i.e., instances where all subinstances with at most [Formula: see text] constraints have a solution. We also design an algorithm running in time polynomial in the size of input and [Formula: see text] that for an input instance and a given [Formula: see text] either computes a solution that satisfies at least a fraction of [Formula: see text] constraints or finds a set of inconsistent constraints whose size depends only on [Formula: see text]. Most of our results apply both to weighted and to unweighted instances of the CSP. Manuel Bodirsky, Daniel Král |
SIAM J. Discret. Math. | 1 |
| 2010 | The complexity of rooted phylogeny problemsabstractSeveral computational problems in phylogenetic reconstruction can be formulated as restrictions of the following general problem: given a formula in conjunctive normal form where the atomic formulas are rooted triples, is there a rooted binary tree that satisfies the formula? If the formulas do not contain disjunctions and negations, the problem becomes the famous rooted triple consistency problem, which can be solved in polynomial time by an algorithm of Aho, Sagiv, Szymanski, and Ullman. If the clauses in the formulas are restricted to disjunctions of negated triples, Ng, Steel, and Wormald showed that the problem remains NP-complete. We systematically study the computational complexity of the problem for all such restrictions of the clauses in the input formula. For certain restricted disjunctions of triples we present an algorithm that has sub-quadratic running time and is asymptotically as fast as the fastest known algorithm for the rooted triple consistency problem. We also show that any restriction of the general rooted phylogeny problem that does not fall into our tractable class is NP-complete, using known results about the complexity of Boolean constraint satisfaction problems. Finally, we present a pebble game argument that shows that the rooted triple consistency problem (and also all generalizations studied in this paper) cannot be solved by Datalog. Manuel Bodirsky, Jens K. Müller |
ICDT | 1 |
| 2010 | On the Scope of the Universal-Algebraic Approach to Constraint SatisfactionabstractThe universal-algebraic approach has proved a powerful tool in the study of the computational complexity of constraint satisfaction problems (CSPs). This approach has previously been applied to the study of CSPs with finite or (infinite) ω-categorical templates. Our first result is an exact characterization of those CSPs that can be formulated with (a finite or) an ω-categorical template. The universal-algebraic approach relies on the fact that in finite or ω-categorical structures A, a relation is primitive positive definable if and only if it is preserved by the polymorphisms of A. In this paper, we present results that can be used to study the computational complexity of CSPs with arbitrary infinite templates. Specifically, we prove that every CSP can be formulated with a template A such that a relation is primitive positive definable in A if and only if it is first-order definable on A and preserved by the infinitary polymorphisms of A. We present applications of our general results to the description and analysis of the computational complexity of CSPs. In particular, we present a polymorphism-based description of those CSPs that are first-order definable (and therefore can be solved in polynomial-time), and give general hardness criteria based on the absence of polymorphisms that depend on more than one argument. Manuel Bodirsky, Martin Hils, Barnaby Martin |
LICS | 1 |
| 2010 | Distance Constraint Satisfaction Problems
Manuel Bodirsky, Víctor Dalmau, Barnaby Martin, Michael Pinsker |
MFCS | 1 |
| 2010 | The complexity of temporal constraint satisfaction problemsabstractA temporal constraint language is a set of relations that has a first-order definition in(Q;<), the dense linear order of the rational numbers. We present a complete complexity classification of the constraint satisfaction problem (CSP) for temporal constraint languages: if the constraint language is contained in one out of nine temporal constraint languages, then the CSP can be solved in polynomial time; otherwise, the CSP is NP-complete. Our proof combines model-theoretic concepts with techniques from universal algebra, and also applies the so-called product Ramsey theorem, which we believe will useful in similar contexts of constraint satisfaction complexity classification. An extended abstract of this article appeared in the proceedings of STOC'08. Manuel Bodirsky, Jan Kára |
J. ACM | 1 |
| 2010 | The reducts of equality up to primitive positive interdefinabilityabstractAbstract We initiate the study of reducts of relational structures up to primitive positive interdefinability: After providing the tools for such a study, we apply these tools in order to obtain a classification of the reducts of the logic of equality. It turns out that there exists a continuum of such reducts. Equivalently, expressed in the language of universal algebra, we classify those locally closed clones over a countable domain which contain all permutations of the domain. Manuel Bodirsky, Hubie Chen, Michael Pinsker |
J. Symb. Log. | 1 |
| 2010 | Quantified Equality ConstraintsabstractAn equality template is a relational structure with infinite universe whose relations can be defined by Boolean combinations of equalities. We prove a complexity classification for quantified constraint satisfaction problems (QCSPs) over equality templates: These problems are in L (decidable in logarithmic space), NP-hard, or coNP-hard. To establish our classification theorem we combine methods from universal algebra with concepts from model theory. Manuel Bodirsky, Hubie Chen |
SIAM J. Comput. | 1 |
| 2010 | Peek arc consistency
Manuel Bodirsky, Hubie Chen |
Theor. Comput. Sci. | 1 |
| 2010 | A fast algorithm and datalog inexpressibility for temporal reasoningabstractWe introduce a new tractable temporal constraint language, which strictly contains the Ord-Horn language of Bürkert and Nebel and the class of AND/OR precedence constraints. The algorithm we present for this language decides whether a given set of constraints is consistent in time that is quadratic in the input size. We also prove that (unlike Ord-Horn) the constraint satisfaction problem of this language cannot be solved by Datalog or by establishing local consistency. Manuel Bodirsky, Jan Kára |
ACM Trans. Comput. Log. | 1 |
| 2009 | Complexity of Existential Positive First-Order Logic
Manuel Bodirsky, Miki Hermann, Florian Richoux |
CiE | 1 |
| 2009 | Integer Programming with 2-Variable Equations and 1-Variable Inequalities
Manuel Bodirsky, Gustav Nordh, Timo von Oertzen |
CTW | 1 |
| 2009 | Semilinear Program Feasibility
Manuel Bodirsky, Peter Jonsson, Timo von Oertzen |
ICALP (2) | 1 |
| 2009 | Integer programming with 2-variable equations and 1-variable inequalities
Manuel Bodirsky, Gustav Nordh, Timo von Oertzen |
Inf. Process. Lett. | 1 |
| 2009 | Qualitative Temporal and Spatial Reasoning RevisitedabstractEstablishing local consistency is one of the main algorithmic techniques in temporal and spatial reasoning. Acentral question for the various proposed temporal and spatial constraint languages is whether local consistency implies global consistency. Showing that a constraint language Γ has this ‘local-to-global’ property implies polynomial-time tractability of the constraint language, and has further pleasant algorithmic consequences. In the present article, we study the ‘local-to-global’ property by making use of a recently established connection of this property with universal algebra. Roughly speaking, the connection shows that this property is equivalent to the presence of a so-called quasi near-unanimity (QNU) polymorphism of the constraint language. We obtain new algorithmic results and give very concise proofs of previously known theorems. Our results concern well-known and heavily studied formalisms such as the point algebra, Allen's interval algebra and the spatial reasoning language RCC-5. Manuel Bodirsky, Hubie Chen |
J. Log. Comput. | 1 |
| 2009 | Maximal infinite-valued constraint languages
Manuel Bodirsky, Hubie Chen, Jan Kára, Timo von Oertzen |
Theor. Comput. Sci. | 1 |
| 2008 | Non-dichotomies in Constraint Satisfaction Complexity
Manuel Bodirsky, Martin Grohe |
ICALP (2) | 1 |
| 2008 | The complexity of temporal constraint satisfaction problemsabstractA temporal constraint language is a set of relations that has a first-order definition in (b Q,<), the dense linear order of the rational numbers. We present a complete complexity classification of the constraint satisfaction problem (CSP) for temporal constraint languages: if the constraint language is contained in one out of nine temporal constraint languages, then the CSP can be solved in polynomial time; otherwise, the CSP is NP-complete. Our proof combines model-theoretic concepts with techniques from universal algebra, and also applies the so-called product Ramsey theorem, which we believe will be useful in similar contexts of constraint satisfaction complexity classification. Manuel Bodirsky, Jan Kára |
STOC | 1 |
| 2008 | The Complexity of Equality Constraint Languages
Manuel Bodirsky, Jan Kára |
Theory Comput. Syst. | 1 |
| 2007 | Maximal Infinite-Valued Constraint Languages
Manuel Bodirsky, Hubie Chen, Jan Kára, Timo von Oertzen |
ICALP | 1 |
| 2007 | Quantified Equality ConstraintsabstractAn equality template (also equality constraint language) is a relational structure with infinite universe whose relations can be defined by boolean combinations of equalities. We prove a complete complexity classification for quantified constraint satisfaction problems (QCSPs) over equality templates: these problems are in L (decidable in logarithmic space), NP-complete, or PSPACE-complete. To establish our classification theorem we combine methods from universal algebra with concepts from model theory. Manuel Bodirsky, Hubie Chen |
LICS | 1 |
| 2007 | An unbiased pointing operator for unlabeled structures, with applications to counting and sampling
Manuel Bodirsky, Éric Fusy, Mihyun Kang, Stefan Vigerske |
SODA | 1 |
| 2007 | Determining the consistency of partial tree descriptions
Manuel Bodirsky, Martin Kutz |
Artif. Intell. | 1 |
| 2007 | Cores of Countably Categorical StructuresabstractA relational structure is a core, if all its endomorphisms are embeddings. This notion is important for computational complexity classification of constraint satisfaction problems. It is a fundamental fact that every finite structure has a core, i.e., has an endomorphism such that the structure induced by its image is a core; moreover, the core is unique up to isomorphism. Weprove that every \omega -categorical structure has a core. Moreover, every \omega-categorical structure is homomorphically equivalent to a model-complete core, which is unique up to isomorphism, and which is finite or \omega -categorical. We discuss consequences for constraint satisfaction with \omega -categorical templates. Manuel Bodirsky |
Log. Methods Comput. Sci. | 1 |
| 2007 | Generating labeled planar graphs uniformly at random
Manuel Bodirsky, Clemens Gröpl, Mihyun Kang |
Theor. Comput. Sci. | 1 |
| 2006 | Datalog and Constraint Satisfaction with Infinite Templates
Manuel Bodirsky, Víctor Dalmau |
STACS | 1 |
| 2006 | Constraint Satisfaction with Countable Homogeneous TemplatesabstractFor a fixed countable homogeneous relational structure Γ we study the computational problem whether a given finite structure of the same signature homomorphically maps to Γ. This problem is known as the constraint satisfaction problem CSP(Γ) for the template Γ and has been intensively studied for finite Γ. We show that — as in the case of finite Γ — the computational complexity of CSP(Γ) for countable homogeneous Γ is determined by the clone of polymorphisms of Γ. To this end we prove the following theorem, which is of independent interest: the primitive positive definable relations over an ω-categorical structure Γ are precisely the relations that are preserved by the polymorphisms of Γ. If the age of Γ is given by a finite number of finite forbidden induced substructures, then CSP(Γ) is in NP. We use a classification result by Cherlin and prove that in this case every constraint satisfaction problem for a countable homogeneous digraph is either tractable or NP-complete. Manuel Bodirsky, Jaroslav Nesetril |
J. Log. Comput. | 1 |
| 2005 | Sampling Unlabeled Biconnected Planar Graphs
Manuel Bodirsky, Clemens Gröpl, Mihyun Kang |
ISAAC | 1 |
| 2005 | The Core of a Countably Categorical Structure
Manuel Bodirsky |
STACS | 1 |
| 2005 | Locally Consistent Constraint Satisfaction Problems with Binary Constraints
Manuel Bodirsky, Daniel Král |
WG | 1 |
| 2004 | Effciently Computing the Density of Regular Languages
Manuel Bodirsky, Tobias Gärtner, Timo von Oertzen, Jan Schwinghammer |
LATIN | 1 |
| 2004 | A new algorithm for normal dominance constraints
Manuel Bodirsky, Denys Duchier, Joachim Niehren, Sebastian Miele |
SODA | 1 |
| 2003 | Generating Labeled Planar Graphs Uniformly at Random
Manuel Bodirsky, Clemens Gröpl, Mihyun Kang |
ICALP | 1 |
| 2002 | Pure Dominance Constraints
Manuel Bodirsky, Martin Kutz |
STACS | 1 |
| 2001 | Underspecified Beta ReductionabstractFor ambiguous sentences, traditional semantics construction produces large numbers of higher-order formulas, which must then be -reduced individually.Underspecified versions can produce compact descriptions of all readings, but it is not known how to perform -reduction on these descriptions.We show how to do this using -reduction constraints in the constraint language for -structures (CLLS). Manuel Bodirsky, Katrin Erk, Alexander Koller, Joachim Niehren |
ACL | 1 |
| 2001 | Beta Reduction Constraints
Manuel Bodirsky, Katrin Erk, Alexander Koller, Joachim Niehren |
RTA | 1 |