Complexity of short Presburger arithmetic

ABSTRACT

We study complexity of short sentences in Presburger arithmetic (Short-PA). Here by “short” we mean sentences with a bounded number of variables, quantifers, inequalities and Boolean operations; the input consists only of the integers involved in the inequalities. We prove that assuming Kannan’s partition can be found in polynomial time, the satisfability of Short-PA sentences can be decided in polynomial time. Furthermore, under the same assumption, we show that the numbers of satisfying assignments of short Presburger sentences can also be computed in polynomial time.

References

1. {BP99} A. Barvinok and J. E. Pommersheim, An algorithmic theory of lattice points in polyhedra, in New Perspectives in Algebraic Combinatorics, Cambridge Univ. Press, Cambridge, 1999, 91–147.
2. {BW03} A. Barvinok and K. Woods, Short rational generating functions for lattice point problems, Jour. AMS 16 (2003), 957–979.
3. {BV07} N. Berline and M. Vergne, Local Euler–Maclaurin formula for polytopes, Mosc. Math. J. 7 (2007), 355–386.
4. {CH16} D. Chistikov and C. Haase, The taming of the semi-linear set, in Proc. ICALP 2016, 127:1–127:13.
5. {DHTY04} J. A. De Loera, R. Hemmecke, J. Tauzer and R. Yoshida, Effective lattice point counting in rational convex polytopes, J. Symbolic Comput. 38 (2004), 1273–1302.
6. {DK97} M. Dyer and R. Kannan, On Barvinok’s algorithm for counting lattice points in fixed dimension, Math. Oper. Res. 22 (1997), 545–549. {Eis03} F. Eisenbrand, Fast integer programming in fixed dimension, in Proc. 11th ESA, Springer, Berlin, 2003, 196–207. {Eis10} F. Eisenbrand, Integer programming and algorithmic geometry of numbers, in 50 years of Integer Programming, Springer, Berlin, 2010, 505–560.
7. {EH12} F. Eisenbrand and N. Hähnle, Minimizing the number of lattice points in a translated polygon, in Proc. 24th SODA, SIAM, Philadelphia, PA, 2012, 1123–1130.
8. {ES08} F. Eisenbrand and G. Shmonin, Parametric integer programming in fixed dimension, Math. Oper. Res. 33 (2008), 839–850.
9. {FR74} M. J. Fischer and M. O. Rabin, Super-Exponential Complexity of Presburger Arithmetic, in Proc. SIAM-AMS Symposium in Applied Mathematics, AMS, Providence, RI, 1974, 27–41.
10. {FT87} A. Frank and É. Tardos, An application of simultaneous Diophantine approximation in combinatorial optimization, Combinatorica 7 (1987), 49–65. {Für82} M. Fürer, The complexity of Presburger arithmetic with bounded quantifier alternation depth, Theoret. Comput. Sci. 18 (1982), 105–111. {Grä87} E. Grädel, The complexity of subclasses of logical theories, Dissertation, Universität Basel, 1987.
11. {Kan90} R. Kannan, Test sets for integer programs, ∀ ∃ sentences, in Polyhedral Combinatorics, AMS, Providence, RI, 1990, 39–47 {Kan92} R. Kannan, Lattice translates of a polytope and the Frobenius problem, Combinatorica 12 (1992), 161–177. {Köp07} M. Köppe, A primal Barvinok algorithm based on irrational decompositions, SIAM J. Discrete Math. 21 (2007), 220–236.
12. {KV08} M. Köppe and S. Verdoolaege, Computing parametric rational generating functions with a primal Barvinok algorithm, Electron. J. Combin. 15 (2008), no. 1, RP 16, 19 pp. {Len83} H. Lenstra, Integer programming with a fixed number of variables, Math. Oper. Res. 8 (1983), 538–548.
13. {MS05} E. Miller and B. Sturmfels, Combinatorial commutative algebra, Springer, New York, 2005.
14. {NP17a} D. Nguyen and I. Pak, Enumeration of integer points in projections of unbounded polyhedra, extended abstract to appear in Proc. IPCO 2017 ; arXiv:1612.08030. {NP17b} D. Nguyen and I. Pak, The computational complexity of integer programming with alternations; arXiv:1702.08662.
15. {NP17c} D. Nguyen and I. Pak, Complexity of short generating functions; arXiv:1702.08660. {Opp78} D. C. Oppen, A 2 22 pn upper bound on the complexity of Presburger arithmetic, J. Comput. System Sci. 16 (1978), 323–332. {Pak02} I. Pak, On sampling integer points in polyhedra, in Foundations of Computational Mathematics, World Sci., River Edge, NJ, 2002, 319–324.
16. {PP15} I. Pak and G. Panova, On the complexity of computing Kronecker coefficients, to appear in Computational Complexity; arXiv:1404.0653.
17. {Pre29} M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt (in German), in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa, 1929, 92–101; English transltion in Hist. Philos. Logic 12 (1991), 225–233.
18. {RL78} C. R. Reddy and D. W. Loveland, Presburger arithmetic with bounded quantifier alternation, Proc. 10th STOC (1978), 320-325. {Sca84} B. Scarpellini, Complexity of subcases of Presburger arithmetic, Trans. AMS 284 (1984), 203–218. {Sch86} A. Schrijver, Theory of linear and integer programming, John Wiley, Chichester, 1986.
19. {Sch97} U. Schöning, Complexity of Presburger arithmetic with fixed quantifier dimension, Theory Comput. Syst. 30 (1997), 423–428. {V+07} S. Verdoolaege, R. Seghir, K. Beyls, V. Loechner and M. Bruynooghe, Counting integer points in parametric polytopes using Barvinok’s rational functions, Algorithmica 48 (2007), 37–66. {Woo04} K. Woods, Rational Generating Functions and Lattice Point Sets, Ph.D. thesis, University of Michigan, 2004, 112 pp. {Woo15} K. Woods, Presburger arithmetic, rational generating functions, and quasipolynomials, J. Symb. Log. 80 (2015), 433–449.

Index Terms

• Mathematics of computing

  • Discrete mathematics

    • Combinatorics

      • Generating functions

  • Mathematical analysis

    • Mathematical optimization

      • Mixed discrete-continuous optimization

        • Integer programming

• Theory of computation

  • Computational complexity and cryptography

    • Complexity theory and logic

    • Problems, reductions and completeness

  • Design and analysis of algorithms

    • Mathematical optimization

      • Mixed discrete-continuous optimization

        • Integer programming

  • Logic

    • Logic and verification