Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
Boolean Algebra with Presburger Arithmetic (BAPA) combines1) Boolean algebras of sets of uninterpreted elements (BA)and 2) Presburger arithmetic operations (PA). BAPA canexpress the relationship between integer variables andcardinalities of unbounded finite sets and can be used toexpress verificati...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2007
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/35258 |
| _version_ | 1826189452736724992 |
|---|---|
| author | Kuncak, Viktor |
| author2 | Martin Rinard |
| author_facet | Martin Rinard Kuncak, Viktor |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | Boolean Algebra with Presburger Arithmetic (BAPA) combines1) Boolean algebras of sets of uninterpreted elements (BA)and 2) Presburger arithmetic operations (PA). BAPA canexpress the relationship between integer variables andcardinalities of unbounded finite sets and can be used toexpress verification conditions in verification of datastructure consistency properties.In this report I consider the Quantifier-Free fragment ofBoolean Algebra with Presburger Arithmetic (QFBAPA).Previous algorithms for QFBAPA had non-deterministicexponential time complexity. In this report I show thatQFBAPA is in NP, and is therefore NP-complete. My resultyields an algorithm for checking satisfiability of QFBAPAformulas by converting them to polynomially sized formulasof quantifier-free Presburger arithmetic. I expect thisalgorithm to substantially extend the range of QFBAPAproblems whose satisfiability can be checked in practice. |
| first_indexed | 2024-09-23T08:14:53Z |
| id | mit-1721.1/35258 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:14:53Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | mit-1721.1/352582019-04-14T07:09:36Z Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete Kuncak, Viktor Martin Rinard Computer Architecture Caratheodory theorem integer linear programming integer cone Hilbert basis Boolean Algebra with Presburger Arithmetic (BAPA) combines1) Boolean algebras of sets of uninterpreted elements (BA)and 2) Presburger arithmetic operations (PA). BAPA canexpress the relationship between integer variables andcardinalities of unbounded finite sets and can be used toexpress verification conditions in verification of datastructure consistency properties.In this report I consider the Quantifier-Free fragment ofBoolean Algebra with Presburger Arithmetic (QFBAPA).Previous algorithms for QFBAPA had non-deterministicexponential time complexity. In this report I show thatQFBAPA is in NP, and is therefore NP-complete. My resultyields an algorithm for checking satisfiability of QFBAPAformulas by converting them to polynomially sized formulasof quantifier-free Presburger arithmetic. I expect thisalgorithm to substantially extend the range of QFBAPAproblems whose satisfiability can be checked in practice. 2007-01-02T20:21:50Z 2007-01-02T20:21:50Z 2007-01-01 MIT-CSAIL-TR-2007-001 http://hdl.handle.net/1721.1/35258 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 14 p. 315999 bytes 842090 bytes application/pdf application/postscript application/pdf application/postscript |
| spellingShingle | Caratheodory theorem integer linear programming integer cone Hilbert basis Kuncak, Viktor Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title_full | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title_fullStr | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title_full_unstemmed | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title_short | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete |
| title_sort | quantifier free boolean algebra with presburger arithmetic is np complete |
| topic | Caratheodory theorem integer linear programming integer cone Hilbert basis |
| url | http://hdl.handle.net/1721.1/35258 |
| work_keys_str_mv | AT kuncakviktor quantifierfreebooleanalgebrawithpresburgerarithmeticisnpcomplete |