LARA

Small Solutions for Quantifier-Free Presburger Arithmetic

We next consider satisfiability of quantifier-free formulas of Presburger arithmetic (denoted QFPA).

We have seen that, by existentially quantifying over all variables, this problem can be solved using quantifier elimination for Presburger Arithmetic.

However, this approach can be expensive.

We next quote a result that allows us to reduce this problem to a polynomially sized SAT formula. This result implies that the satisfiability of QFPA is in NP. The problem is also NP-hard (why?), so it is NP-complete.

QFPA is just PA without quantifiers:

\begin{equation*}\begin{array}{l} F ::= A \mid F_1 \land F_2 \mid \lnot F_1 \mid F_1 \lor F_2 \\ A ::= T_1 = T_2 \mid T_1 \le T_2 \mid (K|T) \\ T ::= K \mid T_1 + T_2 \mid K \cdot T \\ K ::= \ldots -2 \mid -1 \mid 0 \mid 1 \mid 2 \ldots \end{array} \end{equation*}

We also do not need divisibility constraints: $K|t$ is satisfiable iff

Integer Linear Ineqautions

In matrix form, integer linear inequation is

\begin{equation*} A \vec x \leq \vec b \end{equation*}

where $A \vec x$ denotes matrix $A$ multiplied by vector $\vec x$. When $A$ is $m \times n$ matrix, this denotes the system of inequations:

\begin{equation*} \bigwedge_{j=1}^m \sum_{i=1}^n a_{ij} x_i \le b_j \end{equation*}

Note that equations can be expressed as well by stating two inequations.

Conversely, if variables range over non-negative integers, then we can rewrite $A x \le b$ as $Ax + u = b$.

Relatively well studied problem

Reduction of QFPA to Integer Linear Programming

Each QFPA formula can be reduced to a disjunction of linear integer inequations.

Theorem on Solution Bounds

Theorem (Papadimitriou): Let $A$ be $m \times n$ matrix and $b$ an $m$-vector, both with entries from $\{0,\pm 1,\ldots, \pm a\}$. Then if $Ax = b$ has a solution in $x \in \mathbb{N}^n$, it also has a solution in $\{0,1,\ldots,n(ma)^{2m+1}\}^n$.

Proof uses duality in integer linear programming and is given here:

Consequence: it suffices to search for those solutions whose variables denote integers with the number of bits bounded by:

\begin{equation*} \log (n(ma)^{2m+1}) = (2m+1) (\log(ma)) + \log n \end{equation*}

here

  • $a$ is the maximum of values of integers occuring in the problem
  • $m$ is number of constraints
  • $n$ is number of variables

Extending Theorem to QFPA

Note that coefficients in the $A,b$ of the disjuncts are polynomially bounded by coefficients in the QFPA from which they are obtained.

We therefore obtain a “small model theorem”: if there are solutions, there are “small” solutions. In this case, small means “polynomially many bits”.

We obtain a polynomial-time reduction from quantifier-free Presburger arithmetic to SAT.

Reduction to SAT

Observe that if we have bounded integers we can encode the formula into SAT.

Implementation

In practice these bounds are not small enough to be useful. More refined bounds exist for special cases:

But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming.

Extensions

Models get bigger if we allow bitvector operations: