Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic

47Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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 0(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. © Springer-Verlag Berlin Heidelberg 2007.

Cite

CITATION STYLE

APA

Kuncak, V., & Rinard, M. (2007). Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 215–230). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_15

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free