Sciweavers

Share
CADE
2007
Springer

Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

12 years 3 days ago
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
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 nondeterministic 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 algo...
Viktor Kuncak, Martin C. Rinard
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)
books