Abstract
The 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).
M. Bodirsky and J. Greiner have received funding from the European Research Council (ERC Grant Agreement no. 681988), the German Research Foundation (DFG, project number 622397), and the DFG Graduiertenkolleg 1763 (QuantLA).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In other words: for all sets S of atomic \((\tau _1 \cup \tau _2)\)-formulas, we have that \(S \cup T\) is satisfiable if and only if \(S \cup (T_1 \cup T_2)\) is satisfiable.
References
Ackerman, N., Freer, C., Patel, R.: Invariant measures concentrated on countable structures. In: Forum of Mathematics Sigma, vol. 4 (2016)
Baader, F., Schulz, K.U.: Combining constraint solving. In: Goos, G., Hartmanis, J., van Leeuwen, J., Comon, H., Marché, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, pp. 104–158. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45406-3_3
Barto, L., Kompatscher, M., Olšák, M., Pinsker, M., Pham, T.V.: The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems. In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 (2017). Preprint arXiv:1612.07551
Barto, L., Opršal, J., Pinsker, M.: The wonderland of reflections. Israel J. Math. 223, 363–398 (2017). Preprint arXiv:1510.04521
Barto, L., Pinsker, M.: The algebraic dichotomy conjecture for infinite domain constraint satisfaction problems. In: Proceedings of the 31st Annual IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 615–622 (2016). Preprint arXiv:1602.04353
Bodirsky, M.: Complexity classification in infinite-domain constraint satisfaction. Mémoire d’habilitation à diriger des recherches, Université Diderot - Paris 7. arXiv:1201.0856 (2012)
Bodirsky, M., Greiner, J.: Complexity of combinations of qualitative constraint satisfaction problems. Preprint arXiv:1801.05965 (2018)
Bodirsky, M., Grohe, M.: Non-dichotomies in constraint satisfaction complexity. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 184–196. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_16
Bodirsky, M., Jonsson, P.: A model-theoretic view on qualitative constraint reasoning. J. Artif. Intell. Res. 58, 339–385 (2017)
Bodirsky, M., Jonsson, P., Pham, T.V.: The complexity of phylogeny constraint satisfaction problems. ACM Trans. Comput. Log. (TOCL) 18(3), 23 (2017). An extended abstract appeared in the conference STACS 2016
Bodirsky, M., Kára, J.: The complexity of equality constraint languages. Theory Comput. Syst. 3(2), 136–158 (2008). A conference version appeared in the proceedings of Computer Science Russia, CSR 2006
Bodirsky, M., Kára, J.: The complexity of temporal constraint satisfaction problems. J. ACM 57(2), 1–41 (2009). An extended abstract appeared in the Proceedings of the Symposium on Theory of Computing, STOC
Bodirsky, M., Kára, J.: A fast algorithm and Datalog inexpressibility for temporal reasoning. ACM Trans. Comput. Log. 11(3), 15 (2010)
Bodirsky, M., Mottet, A.: Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction. In: Proceedings of the 31st Annual IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 623–632 (2016). Preprint ArXiv:1601.04520
Bodirsky, M., Nešetřil, J.: Constraint satisfaction with countable homogeneous templates. J. Log. Comput. 16(3), 359–373 (2006)
Bodirsky, M., Pinsker, M.: Topological Birkhoff. Trans. Am. Math. Soc. 367, 2527–2549 (2015)
Bodirsky, M., Pinsker, M., Pongrácz, A.: Projective clone homomorphisms. J. Symb. Log. (2014, accepted for publication). Preprint arXiv:1409.4601
Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 513–527. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_42
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5 (2014)
Bulatov, A.A.: A dichotomy theorem for nonuniform CSPs. FOCS 2017 (2017, accepted for publication). arXiv:1703.03021
Cameron, P.J.: Oligomorphic Permutation Groups. Cambridge University Press, Cambridge (1990)
Cameron, P.J.: Homogeneous permutations. Electron. J. Comb. 9(2), 2 (2002)
Cherlin, G.: The Classification of Countable Homogeneous Directed Graphs and Countable Homogeneous \(n\)-Tournaments, vol. 131, no. 621. AMS Memoirs, New York, January 1998
Creignou, N., Kolaitis, P.G., Vollmer, H. (eds.): Complexity of Constraints. LNCS, vol. 5250. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92800-3
Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)
Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)
Kompatscher, M., Pham, T.V.: A complexity dichotomy for poset constraint satisfaction. In: 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017. Leibniz International Proceedings in Informatics, LIPIcs, vol. 66, pp. 47:1–47:12 (2017)
Lachlan, A.H.: Countable homogeneous tournaments. TAMS 284, 431–461 (1984)
Linman, J., Pinsker, M.: Permutations on the random permutation. Electron. J. Comb. 22(2), 1–22 (2015)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)
Zhuk, D.: The proof of CSP dichotomy conjecture. FOCS 2017 (2017, accepted for publication). arXiv:1704.01914
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Bodirsky, M., Greiner, J. (2018). Complexity of Combinations of Qualitative Constraint Satisfaction Problems. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-94205-6_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94204-9
Online ISBN: 978-3-319-94205-6
eBook Packages: Computer ScienceComputer Science (R0)