## Abstraction-based satisfiability solving of Presburger arithmetic

*Daniel Kroening*,
*Joël
Ouaknine*, *Sanjit Seshia*, and *Ofer Strichman*
We present a new abstraction-based framework for deciding
satisfiability of quantifier-free Presburger arithmetic formulas.
Given a Presburger formula *φ*, our algorithm invokes a SAT solver
to produce proofs of unsatisfiability of approximations of *φ*.
These proofs are in turn used to generate abstractions of *φ* as
inputs to a theorem prover. The SAT-encodings of the approximations of
*φ* are obtained by instantiating the variables of the formula over
finite domains. The satisfying integer assignments provided by the
theorem prover are then used to selectively increase domain sizes and
generate fresh SAT-encodings of *φ*.
The efficiency of this approach derives from the ability of SAT
solvers to extract small unsatisfiable cores, leading to small
abstracted formulas. We present experimental results which suggest
that our algorithm is considerably more efficient than directly
invoking the theorem prover on the original formula.

*Proceedings of CAV 04*, LNCS 3114, 2004. 13 pages.

PostScript /
PDF
© 2004
Springer-Verlag.

Imprint / Data Protection