Document Open Access Logo

On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

Authors Christoph Haase , Alessio Mansutti , Amaury Pouly

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.52.pdf
  • Filesize: 0.91 MB
  • 14 pages

Document Identifiers

Author Details

Christoph Haase
  • University of Oxford, UK
Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain
Amaury Pouly
  • University of Oxford, UK
  • Université Paris Cité, CNRS, IRIF, France

Funding

This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

Cite AsGet BibTex

Christoph Haase, Alessio Mansutti, and Amaury Pouly. On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.MFCS.2023.52

Abstract

This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1-31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • first-order theories
  • arithmetic theories
  • fixed-parameter tractability

Metrics

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

References

  1. Eric Bach and Jeffrey Shallit. Algorithmic Number Theory, Vol 1: Efficient Algorithms. Foundations of Computing. MIT Press, 1996. Google Scholar
  2. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In ICALP, 2023. To appear. Google Scholar
  3. Garrett Birkhoff. Rings of sets. Duke Math. J., 3(3):443-454, 1937. URL: https://doi.org/10.1215/S0012-7094-37-00334-X.
  4. Manuel Bodirsky, Barnaby Martin, Marcello Mamino, and Antoine Mottet. The complexity of disjunctive linear diophantine constraints. In MFCS, pages 33:1-33:16, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.33.
  5. Itshak Borosh and Leon B. Treybing. Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc., 55:299-304, 1976. URL: https://doi.org/10.2307/2041711.
  6. J. Richard Büchi. Weak second-order arithmetic and finite automata. Math. Logic Quart., 6(1‐6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  7. Hubie Chen. A rendezvous of logic, complexity, and algebra. ACM Comput. Surv., 42(1):2:1-2:32, 2009. URL: https://doi.org/10.1145/1592451.1592453.
  8. Dmitry Chistikov and Christoph Haase. On the complexity of quantified integer programming. In ICALP, pages 94:1-94:13, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.94.
  9. Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti. Higher-order quantified Boolean satisfiability. In MFCS, pages 33:1-33:15, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.33.
  10. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In LICS, pages 59:1-59:13, 2022. URL: https://doi.org/10.1145/3531130.3533372.
  11. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0515-9.
  12. Erich Grädel. Simple sentences that are hard to decide. Inf. Comput., 94(1):62-82, 1991. URL: https://doi.org/10.1016/0890-5401(91)90033-X.
  13. Felix Hausdorff. Grundzüge der Mengenlehre. Veit and Company, Leipzig, 1914. [Accessed 2023-08-07]. URL: https://archive.org/details/grundzgedermen00hausuoft.
  14. Markus Junker. A note on equational theories. J. Symb. Log., 65(4):1705-1712, 2000. URL: https://doi.org/10.2307/2695070.
  15. Ravindran Kannan. Test sets for integer programs, ∀∃ sentences. Polyhedral Combinatorics, Proc. of a DIMACS workshop, pages 38-48, 1990. Google Scholar
  16. Ravindran Kannan and Achim Bachem. Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput., 8(4):499-507, 1979. URL: https://doi.org/10.1137/0208040.
  17. Marek Karpinski, Hans Kleine Büning, and Peter H. Schmitt. On the computational complexity of quantified horn clauses. In CSL, pages 129-137, 1987. URL: https://doi.org/10.1007/3-540-50241-6_34.
  18. Hendrik W. Lenstra Jr. Integer programming with a fixed number of variables. Math. Oper. Res., 8(4):538-548, 1983. URL: https://doi.org/10.1287/moor.8.4.538.
  19. Antoine Miné. The octagon abstract domain. High. Order Symb. Comput., 19(1):31-100, 2006. URL: https://doi.org/10.1007/s10990-006-8609-1.
  20. Danny Nguyen and Igor Pak. Short Presburger arithmetic is hard. SIAM J. Comput., 51(2):17:1-30, 2022. URL: https://doi.org/10.1137/17M1151146.
  21. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pages 92-101, 1929. Google Scholar
  22. Bruno Scarpellini. Complexity of subcases of Presburger arithmetic. Trans. Am. Math. Soc., 284:203-218, 1984. URL: https://doi.org/10.2307/1999283.
  23. Uwe Schöning. Complexity of presburger arithmetic with fixed quantifier dimension. Theory Comput. Syst., 30(4):423-428, 1997. URL: https://doi.org/10.1007/s002240000059.
  24. Larry J. Stockmeyer. The polynomial-time hierarchy. Theor. Comput. Sci., 3(1):1-22, 1976. URL: https://doi.org/10.1016/0304-3975(76)90061-X.
  25. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc., 72(1):155-158, 1978. URL: https://doi.org/10.1080/00029890.1978.11994639.
  26. Klaus Weihrauch. Computable Analysis. Springer, 2000. URL: https://doi.org/10.1007/978-3-642-56999-9.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact