Document Open Access Logo

Integer Linear-Exponential Programming in NP by Quantifier Elimination

Authors Dmitry Chistikov , Alessio Mansutti , Mikhail R. Starchak

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.132.pdf
  • Filesize: 0.9 MB
  • 20 pages

Document Identifiers

Author Details

Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain
Mikhail R. Starchak
  • St. Petersburg State University, Russia

Funding

  • Chistikov, Dmitry: Supported in part by the Engineering and Physical Sciences Research Council [EP/X03027X/1].
  • Mansutti, Alessio: funded by the Madrid Regional Government (César Nombela grant 2023-T1/COM-29001), and by MCIN/AEI/10.13039/501100011033/FEDER, EU (grant PID2022-138072OB-I00).
  • Starchak, Mikhail R.: Supported by the Russian Science Foundation, project 23-71-01041.

Cite AsGet BibTex

Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer Linear-Exponential Programming in NP by Quantifier Elimination. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 132:1-132:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.132

Abstract

This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms 2^x and remainder terms (x mod 2^y). Our result implies that the existential theory of the structure (ℕ,0,1,+,2^(⋅),V_2(⋅,⋅), ≤) has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function x ↦ 2^x and the binary predicate V_2(x,y) that is true whenever y ≥ 1 is the largest power of 2 dividing x. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic algorithms
  • Theory of computation → Logic
Keywords
  • decision procedures
  • integer programming
  • quantifier elimination

Metrics

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

References

  1. Erwin H. Bareiss. Sylvester’s identity and multistep integer-preserving Gaussian elimination. Math. Comput., 22:565-578, 1968. URL: https://doi.org/10.1090/S0025-5718-1968-0226829-0.
  2. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In ICALP, pages 112:1-112:18, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.112.
  3. Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc., 55(2):299-304, 1976. URL: https://doi.org/10.2307/2041711.
  4. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc., 1(2):191-238, 1994. Corrigendum: Bull. Belgian Math. Soc., 1, 1994, 577. URL: https://doi.org/10.36045/bbms/1103408547.
  5. 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.
  6. Gregory Cherlin and Françoise Point. On extensions of Presburger arithmetic. In 4th Easter Conference on Model Theory, volume 86 of Humboldt-Univ. Berlin Seminarberichte, pages 17-34, 1986. URL: https://webusers.imj-prg.fr/~francoise.point/papiers/cherlin_point86.pdf.
  7. 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.
  8. Kevin J. Compton and C. Ward Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Log., 48(1):1-79, 1990. URL: https://doi.org/10.1016/0168-0072(90)90080-L.
  9. David C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7(91-99):300, 1972. Google Scholar
  10. Charles L. Dodgson. Condensation of determinants, being a new and brief method for computing their arithmetical values. Proc. R. Soc. Lond., 15:150-155, 1867. URL: https://doi.org/10.1098/rspl.1866.0037.
  11. Andrei Draghici, Christoph Haase, and Florin Manea. Semënov arithmetic, affine VASS, and string constraints. In STACS, pages 29:1-29:19, 2024. URL: https://doi.org/10.4230/LIPICS.STACS.2024.29.
  12. Florian Frohn and Jürgen Giesl. Satisfiability modulo exponential integer arithmetic, 2024. To appear in IJCAR. URL: https://arxiv.org/abs/2402.01501.
  13. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In LICS, pages 1-10, 2019. URL: https://doi.org/10.1109/LICS.2019.8785681.
  14. Christoph Haase. Approaching arithmetic theories with finite-state automata. In LATA, pages 33-43, 2020. URL: https://doi.org/10.1007/978-3-030-40608-0_3.
  15. Christoph Haase and Jakub Różycki. On the expressiveness of Büchi arithmetic. In FoSSaCS, pages 310-323, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_16.
  16. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In IJCAR, pages 122-140, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_8.
  17. Philipp Hieronymi and Christian Schulz. A strong version of Cobham’s theorem. In STOC, pages 1-21, 2022. URL: https://doi.org/10.1145/3519935.3519958.
  18. Antoine Joux, Andrew Odlyzko, and Cécile Pierrot. The past, evolving present, and future of the discrete logarithm. In Open Problems in Mathematics and Computational Science, pages 5-36. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10683-0_2.
  19. 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.
  20. Michael Jünger, Thomas M. Liebling, Denis Naddef, George L. Nemhauser, William R. Pulleyblank, Gerhard Reinelt, Giovanni Rinaldi, and Laurence A. Wolsey. 50 years of integer programming 1958-2008: From the early years to the state-of-the-art. Springer, 2009. Google Scholar
  21. Anna Karapiperi, Michela Redivo-Zaglia, and Maria Rosaria Russo. Generalizations of Sylvester’s determinantal identity, 2015. URL: https://arxiv.org/abs/1503.00519.
  22. Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 254-266, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  23. Aless Lasaruk and Thomas Sturm. Weak integer quantifier elimination beyond the linear case. In CASC, pages 275-294, 2007. URL: https://doi.org/10.1007/978-3-540-75187-8_22.
  24. Leonid Libkin. Variable independence for first-order definable constraints. ACM Trans. Comput. Log., 4(4):431-451, 2003. URL: https://doi.org/10.1145/937555.937557.
  25. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  26. Derek C. Oppen. Elementary bounds for Presburger arithmetic. In STOC, pages 34-37, 1973. URL: https://doi.org/10.1145/800125.804033.
  27. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. URL: https://doi.org/10.1145/322276.322287.
  28. Françoise Point. On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers. J. Symb. Log., 65(3):1347-1374, 2000. URL: https://doi.org/10.2307/2586704.
  29. Françoise Point. On the expansion (ℕ;+,2^x) of Presburger arithmetic, 2007. Preprint. URL: https://webusers.imj-prg.fr/~francoise.point/papiers/Pres.pdf.
  30. 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 Congrès des Mathématiciens des Pays Slaves, pages 92-101. Warsaw, 1929. Google Scholar
  31. Sylvain Schmitz. Complexity hierarchies beyond Elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  32. Alexander Schrijver. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 1999. Google Scholar
  33. Aleksei L. Semenov. On certain extensions of the arithmetic of addition of natural numbers. Math. USSR Izv., 15(2):401-418, 1980. URL: https://doi.org/10.1070/im1980v015n02abeh001252.
  34. Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587-618, 1984. URL: https://doi.org/10.1070/im1984v022n03abeh001456.
  35. Jeffrey Shallit. The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with Walnut. Cambridge University Press, 2022. URL: https://doi.org/10.1017/9781108775267.
  36. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In STOC, pages 1-9, 1973. URL: https://doi.org/10.1145/800125.804029.
  37. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. P. Am. Math. Soc., 72(1):155-158, 1978. URL: https://doi.org/10.1090/S0002-9939-1978-0500555-0.
  38. Volker Weispfenning. The complexity of almost linear Diophantine problems. J. Symb. Comput., 10(5):395-404, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
  39. Volker Weispfenning. Complexity and uniformity of elimination in Presburger arithmetic. In ISSAC, pages 48-53, 1997. URL: https://doi.org/10.1145/258726.258746.
  40. Volker Weispfenning. Deciding linear-exponential problems. SIGSAM Bull., 34(1):30-31, 2000. URL: https://doi.org/10.1145/373500.373513.
  41. Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, and Naijun Zhan. A decision procedure for string constraints with string-integer conversion and flat regular constraints. Acta Inform., 2023. URL: https://doi.org/10.1007/s00236-023-00446-4.
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