Short Presburger arithmetic is hard!
This is a belated report on a remarkable breakthrough from 2017. The paper is Short Presburger arithmetic is hard, by Nguyen and Pak.
Integer programming in bounded dimension: Lenstra’s Theorem
Algorithmic tasks are often intractable. But there are a few miracles where efficient algorithms exist: Solving systems of linear equations, linear programming, testing primality, and solving integer programming problems when the number of variables is bounded. The last miracle is a historic 1983 theorem of Hendrik Lenstra (Here is the paper) and it is the starting point of this post.
Lensra’s theorem: Consider a system of linear inequalities
Ax ≤ b
where is a vector of variables, A is an integral k by n matrix and b is an integral vector of length n.
Let be a fixed integer. There is a polynomial time algorithm to determine if the system has an integral solution.
Of course, the full Integer Programming problem when is part of the input, is NP-complete. This problem came already (second in Karp’s list!) in the Mayflower of NP-complete problems – Karp’s paper.
Sasha Barvinok famously showed in 1993 that even counting the number of solutions is in P. (Barvinok utilized the short generating function approach pioneered by Brion, Vergne and others.)
Next, I want to describe an amazing 1990 theorem of Ravi Kannan,
Kannan’s theorem considers formulas with one quantifier alternation in the Presburger arithmetic and it asserts that when the number of variables is fixed, there is a polynomial time algorithm to decide if the formula is satisfiable.
(Here is a free version of Kannan’s paper.) Also here the counting problems were tackled with great success. Barvinok and Kevin Woods remarkably showed how to count projections of integer points in a (single) polytope in polynomial time, and subsequently Woods extended this approach to general Presburger expressions Φ with a fixed number of inequalities!
An important strengthening was achieved by Friedrich Eisenbrand and Gennady Shmonin in the 2008 paper Parametric integer programming in fixed dimension. See also the survey chapter by Barvinok Lattice points and lattice polytopes.
You can find the formulation of Kannan’s theorem in full generality a little further but let me present now a special case related to the famous Frobenius coin problem. (See this post on GLL for more on Presburger arithmetic)
Frobenius coin problem
Given k coins with integral values, the Frobinius coin problem is to determine the largest integer that cannot be described as positive integer combinations of the values of the coins. (See also this post on GLL.)
Theorem (Kannan): There is a polynomial time algorithm to solve the Frobenius coin problem for every fixed number of coins.
The issue of the way theory meets practice for the problems discussed in this post is very interesting but we will not discuss it. Let me remark that Herb Scarf (who along with Kannan played a role in B-L (Before Lenstra) developments) offered another approach for the solution of the Frobenius coin problem and related IP (Integer Programming) problems based on his theory of maximal lattice-free convex bodies. See this related post.
More than one quantifier
Given the result of Kannan and later that of Barvinok and Woods, many people expected that also for two alternations, or even for any other fixed number of alternations, Presburger arithmetic would be in polynomial time. Nguyen and Pak proved that the problem is NP-complete already for two quantifier alternations! Here is the link to the paper Short Presburger arithmetic is hard. Igor Pak’s homepage has a few other related papers.
Let me bring here Sasha Barvinok’s MathSciNet featured review of Nguyen and Pak’s paper which tells the story better than I could.
Barvinok’s featured review to Nguyen and Pak’s paper
Presburger arithmetic allows integer variables, integer constants, Boolean operations (&, ∧, ¬), quantifiers (∃, ∀), equations and inequalities (=, <, >, ≤, ≥), addition and subtraction (+, −) and multiplication by integer constants. It does not allow multiplication of variables (if we allow multiplication of variables, we get Peano arithmetic).
Geometrically, a quantifier-free formula of Presburger arithmetic describes the set of integer points in a Boolean combination of rational polyhedra (that is, in the set obtained from finitely many rational polyhedra by taking unions, intersections and complements). Similarly, a formula of Presburger arithmetic with existential quantifiers only describes the set of integer points obtained from the set of integer points in a Boolean combination of polyhedra by a projection along some coordinates.
Unlike Peano arithmetic, Presburger arithmetic is decidable. Here the authors zoom in on the computational complexity of Presburger arithmetic, once the combinatorial complexity of the formula is bounded in advance. If we fix the number of variables, the validity of a formula with no quantifier alternations (that is, of the type ∃ . . . ∃Φ() or of the type ∀ . . . ∀Φ()) can be established in polynomial time by Lenstra’s integer programming algorithm [see H. W. Lenstra Jr., Math. Oper. Res. 8 (1983), no. 4, 538–548; MR0727410].
For a fixed number of variables, formulas with one quantifier alternation (∃ . . . ∃∀ . . . ∀Φ()) can also be solved in polynomial time, as shown by R. Kannan [in Polyhedral combinatorics (Morristown, NJ, 1989), 39–47, DIMACS Ser. Discrete Math. Theoret. Comput. Sci., 1, Amer. Math. Soc., Providence, RI, 1990; MR1105115]. The decision procedure can be characterized as a polynomial time algorithm for parametric integer programming.
Suppose now that we fix the number of variables and the number of Boolean operations in advance (and hence get what is called a short formula of Presburger arithmetic). Thus the only parameters of the formula are the numerical values of the constants in the formula. The authors show that deciding validity becomes NP-complete if one allows
two quantifier alternations. Remarkably, they present an example of a formula
∃z ∈ ∀y ∈ ∃x ∈ Φ(x, y, z)
with an NP-complete decision problem, even though Φ contains at most 10 inequalities.
Another remarkable example is an NP-complete decision problem for a formula of the
∃z ∈ ∀y ∈ ∃x ∈ : Ax + By + Cz ≤ b,
with at most 24 inequalities.
As the number of quantifier alternations is allowed to increase, the computational complexity in the polynomial hierarchy also moves up. The authors also describe the computational complexity of corresponding counting problems.
The proof is very clever; it uses the continued fraction expansion of a rational number to encode a growing family of intervals, with the help of which the authors build an NP-complete problem.