## Viktor Kuncak and Martin Rinard.
Towards efficient satisfiability checking for Boolean Algebra
with Presburger Arithmetic.
In *Conference on Automateded Deduction (CADE-21)*, volume 4603
of *LNCS*, 2007.

Boolean Algebra with Presburger Arithmetic (BAPA) is a
decidable logic that combines 1) Boolean algebra of sets of
uninterpreted elements (BA) and 2) Presburger arithmetic (PA).
BAPA can express relationships between
integer variables and cardinalities of unbounded sets. In
combination with other decision procedures and theorem
provers, BAPA is useful for automatically verifying quantitative
properties of data structures. This paper examines QFBAPA, the
quantifier-free fragment of BAPA. The computational
complexity of QFBAPA satisfiability was previously unknown;
previous QFBAPA algorithms have non-deterministic
exponential time complexity due to an explosion in the
number of introduced integer variables.
This paper shows, for the first time, how to avoid such
exponential explosion. We present an algorithm for checking
satisfiability of QFBAPA formulas by reducing them to
formulas of quantifier-free PA, with only O(n log(n))
increase in formula size. We prove the correctness of our
algorithm using a theorem about sparse solutions of integer
linear programming problems. This is the first proof that
QFBAPA satisfiability is in NP and therefore NP-complete.
We implemented our algorithm in the context of the Jahob
verification system. Our preliminary experiments suggest
that our algorithm, although not necessarily better for proving
formula unsatisfiability, is more effective in
detecting formula satisfiability than previous approaches.

[ bib ]
Back