Identifying Tractable Quantified Temporal Constraints Within Ord-Horn

Authors Jakub Rydval , Žaneta Semanišinová , Michał Wrona

Thumbnail PDF


  • Filesize: 2.25 MB
  • 20 pages

Document Identifiers

Author Details

Jakub Rydval
  • Technische Universität Wien, Austria
Žaneta Semanišinová
  • Technische Universität Dresden, Germany
Michał Wrona
  • Jagiellonian University, Kraków, Poland


The authors thank Dmitriy Zhuk for many inspiring discussions on the topic, and the anonymous reviewers for many helpful suggestions.

Cite AsGet BibTex

Jakub Rydval, Žaneta Semanišinová, and Michał Wrona. Identifying Tractable Quantified Temporal Constraints Within Ord-Horn. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 151:1-151:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. Already the restriction to the class of all finite structures forms an interesting microcosm on its own, but to express decision problems in temporal reasoning one has to take a step beyond the finite-domain realm. An important class of templates used in this context are temporal structures, i.e., structures over ℚ whose relations are first-order definable using the usual countable dense linear order without endpoints. In the standard setting, which allows only existential quantification over input variables, the complexity of finite and temporal constraints has been fully classified. In the quantified setting, i.e., when one also allows universal quantifiers, there is only a handful of partial classification results and many concrete cases of unknown complexity. This paper presents a significant progress towards understanding the complexity of the quantified constraint satisfaction problem for temporal structures. We provide a complexity dichotomy for quantified constraints over the Ord-Horn fragment, which played an important role in understanding the complexity of constraints both over temporal structures and in Allen’s interval algebra. We show that all problems under consideration are in P or coNP-hard. In particular, we determine the complexity of the quantified constraint satisfaction problem for (ℚ;x = y⇒ x ≥ z), hereby settling a question open for more than ten years.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
  • Theory of computation → Logic
  • Theory of computation → Computational complexity and cryptography
  • constraint satisfaction problems
  • quantifiers
  • dichotomy
  • temporal reasoning
  • Ord-Horn


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of databases, volume 8. Addison-Wesley, Boston, 1995. URL:
  2. Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Cambridge University Press, Cambridge, 2021. URL:
  3. Manuel Bodirsky and Hubie Chen. Quantified equality constraints. SIAM J. Comput., 39(8):3682-3699, 2010. A preliminary version of the paper appeared in the proceedings of LICS'07. URL:
  4. Manuel Bodirsky, Hubie Chen, and Michał Wrona. Tractability of quantified temporal constraints to the max. Int. J. Algebra Comput., 24(8):1141-1156, 2014. URL:
  5. Manuel Bodirsky and Víctor Dalmau. Datalog and constraint satisfaction with infinite templates. J. Comput. Syst. Sci., 79(1):79-100, 2013. A preliminary version appeared in the proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'05). URL:
  6. Manuel Bodirsky and Jan Kára. The complexity of equality constraint languages. Theory Comput. Syst., 43(2):136-158, 2008. URL:
  7. Manuel Bodirsky and Jan Kára. The complexity of temporal constraint satisfaction problems. J. ACM, 57(2):9:1-9:41, 2010. URL:
  8. Manuel Bodirsky and Jakub Rydval. On the descriptive complexity of temporal constraint satisfaction problems. J. ACM, 70(1):2:1-2:58, 2023. URL:
  9. Stefano Ceri, Georg Gottlob, and Letizia Tanca. Logic programming and databases. Surveys in computer science. Springer, Berlin, Heidelberg, 1990. URL:
  10. Witold Charatonik and Michał Wrona. Quantified positive temporal constraints. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 94-108, Berlin, Heidelberg, 2008. Springer. URL:
  11. Witold Charatonik and Michał Wrona. Tractable quantified constraint satisfaction problems over positive temporal templates. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, volume 5330 of Lecture Notes in Computer Science, pages 543-557, Berlin, Heidelberg, 2008. Springer, Springer. URL:
  12. Hubie Chen and Michał Wrona. Guarded ord-horn: A tractable fragment of quantified constraint satisfaction. In Ben C. Moszkowski, Mark Reynolds, and Paolo Terenziani, editors, 19th International Symposium on Temporal Representation and Reasoning, TIME 2012, Leicester, United Kingdom, September 12-14, 2012, pages 99-106, Leicester, UK, 2012. IEEE Computer Society. URL:
  13. Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997. Google Scholar
  14. Dexter Kozen. Theory of computation, volume 170 of Texts in Computer Science. Springer, 2006. URL:
  15. Andrei A. Krokhin, Peter Jeavons, and Peter Jonsson. Reasoning about temporal relations: The tractable subalgebras of allen’s interval algebra. J. ACM, 50(5):591-640, 2003. URL:
  16. Bernhard Nebel and Hans-Jürgen Bürckert. Reasoning about temporal relations: A maximal tractable subclass of allen’s interval algebra. J. ACM, 42(1):43-66, 1995. URL:
  17. Jakub Rydval, Žaneta Semanišinová, and Michał Wrona. Identifying tractable quantified temporal constraints within ord-horn. CoRR, abs/2402.09187, 2024. URL:
  18. Michał Wrona. Tractability frontier for dually-closed ord-horn quantified constraint satisfaction problems. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 535-546, Berlin, Heidelberg, 2014. Springer. URL:
  19. Dmitriy Zhuk. A proof of the CSP dichotomy conjecture. J. ACM, 67(5):30:1-30:78, 2020. URL:
  20. Dmitriy Zhuk. Personal communication, 2022. Google Scholar
  21. Dmitriy Zhuk and Barnaby Martin. QCSP monsters and the demise of the chen conjecture. J. ACM, 69(5):35:1-35:44, 2022. URL:
  22. Dmitriy Zhuk, Barnaby Martin, and Michał Wrona. The complete classification for quantified equality constraints. In Nikhil Bansal and Viswanath Nagarajan, editors, Proceedings of the 2023 ACM-SIAM Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, January 22-25, 2023, pages 2746-2760, Florence, Italy, 2023. SIAM. URL: