paper ps
Boolean Algebra with Presburger Arithmetic (BAPA) combines
1) Boolean algebras of sets of uninterpreted elements (BA)
and 2) Presburger arithmetic operations (PA). BAPA can
express the relationship between integer variables and
cardinalities of unbounded finite sets and can be used to
express verification conditions in verification of data
structure consistency properties.
In this report I consider the Quantifier-Free fragment of
Boolean Algebra with Presburger Arithmetic (QFBAPA).
Previous algorithms for QFBAPA had non-deterministic
exponential time complexity. In this report I show that
QFBAPA is in NP, and is therefore NP-complete. My result
yields an algorithm for checking satisfiability of QFBAPA
formulas by converting them to polynomially sized formulas
of quantifier-free Presburger arithmetic. I expect this
algorithm to substantially extend the range of QFBAPA
problems whose satisfiability can be checked in practice.

### Citation

Viktor Kuncak.
Quantifier-free boolean algebra with presburger arithmetic is
np-complete.
Technical Report MIT-CSAIL-TR-2007-001, MIT CSAIL, January 2007.### BibTex Entry

@techreport{Kuncak07QuantifierFreeBAPAinNP,
author = {Viktor Kuncak},
title = {Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete},
institution = {MIT CSAIL},
year = 2007,
month = {January},
url = {http://hdl.handle.net/1721.1/35258},
number = {MIT-CSAIL-TR-2007-001},
abstract = {
Boolean Algebra with Presburger Arithmetic (BAPA) combines
1) Boolean algebras of sets of uninterpreted elements (BA)
and 2) Presburger arithmetic operations (PA). BAPA can
express the relationship between integer variables and
cardinalities of unbounded finite sets and can be used to
express verification conditions in verification of data
structure consistency properties.
In this report I consider the Quantifier-Free fragment of
Boolean Algebra with Presburger Arithmetic (QFBAPA).
Previous algorithms for QFBAPA had non-deterministic
exponential time complexity. In this report I show that
QFBAPA is in NP, and is therefore NP-complete. My result
yields an algorithm for checking satisfiability of QFBAPA
formulas by converting them to polynomially sized formulas
of quantifier-free Presburger arithmetic. I expect this
algorithm to substantially extend the range of QFBAPA
problems whose satisfiability can be checked in practice.
}
}