# 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:

We also do not need divisibility constraints: is satisfiable iff

## Integer Linear Ineqautions

In matrix form, integer linear inequation is

where denotes matrix multiplied by vector . When is matrix, this denotes the system of inequations:

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

Conversely, if variables range over non-negative integers, then we can rewrite as .

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 be matrix and an -vector, both with entries from . Then if has a solution in , it also has a solution in .

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:

here

• is the maximum of values of integers occuring in the problem
• is number of constraints
• is number of variables

## Extending Theorem to QFPA

Note that coefficients in the 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: