Danny Nguyen and Igor Pak: Presburger Arithmetic Problem Solved!

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.

Danny Nguyen

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 $x=(x_1,x_2,\dots x_k)$ is a vector of $k$ variables, A is an integral k by n matrix and b is an integral vector of length n.

Let $k$ 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 $k$ 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.)

Kannan’s theorem

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 ∃ $x_1$ . . . ∃ $x_k$ Φ( $x_1, \dots , latex x_k$ ) or of the type ∀ $x_1$ . . . ∀ $x_k$ Φ( $x_1, \dots , x_k$ )) 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 (∃ $x_1$ . . . ∃ $x_k$ ∀ $y_1$ . . . ∀ $y_m$ Φ( $x_1, \dots , x_k, y_1, \dots , y_m$ )) 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 ∈ $\mathbb Z$ ∀y ∈ $\mathbb Z^2$ ∃x ∈ $\mathbb Z^2$ Φ(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
type

∃z ∈ $\mathbb Z$ ∀y ∈ $\mathbb Z^2$ ∃x ∈ $\mathbb Z^6$ : 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.

	Gil Kalai on Three Remarkable Quantum Event…
	Arturo Merino, Torst… on Updates from Cambridge
	ryeguy10 on Updates from Cambridge
	Gil Kalai on Updates from Cambridge
	Gil Kalai on Updates from Cambridge
	Rivki on Updates from Cambridge
	Sandy H on Updates from Cambridge
	ryeguy10 on Updates from Cambridge
	Updates from Cambrid… on Random Circuit Sampling: Fouri…
	Gil Kalai on Random Circuit Sampling: Fouri…
	Gil Kalai on Random Circuit Sampling: Fouri…
	kodlu on Random Circuit Sampling: Fouri…