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

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.

[ bib | http ] Back