
CMUCS04100
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS04100
Abstractionbased Satisfiability Solving
of Presbuerger Arithmetic
Daniel Kroening, Joël Ouaknine, Sanjit Seshia, Ofer Strichman
January 2004
CMUCS04100.ps
CMUCS04100.pdf
Keywords: Presburger arithmetic, Boolean satisfiability,
theorem proving, abstraction
We present a new abstractionbased framework for deciding
satisfuability of quantifierfree 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 SATencodings 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 SATencodings 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.
16 pages
