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:
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:
- 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.
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.
Models get bigger if we allow bitvector operations: