On Algorithms and Complexity for Sets with Cardinality Constraints
Typestate systems ensure many desirable properties of imperativeprograms, including initialization of object fields and correct use ofstateful library interfaces. Abstract sets with cardinalityconstraints naturally generalize typestate properties: relationshipsbetween the typestates of objects can...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30561 |
| _version_ | 1811088791896588288 |
|---|---|
| author | Marnette, Bruno Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Marnette, Bruno Kuncak, Viktor Rinard, Martin |
| author_sort | Marnette, Bruno |
| collection | MIT |
| description | Typestate systems ensure many desirable properties of imperativeprograms, including initialization of object fields and correct use ofstateful library interfaces. Abstract sets with cardinalityconstraints naturally generalize typestate properties: relationshipsbetween the typestates of objects can be expressed as subset anddisjointness relations on sets, and elements of sets can berepresented as sets of cardinality one. In addition, sets withcardinality constraints provide a natural language for specifyingoperations and invariants of data structures.Motivated by these program analysis applications, thispaper presents new algorithms and new complexity results forconstraints on sets and their cardinalities. We studyseveral classes of constraints and demonstrate a trade-offbetween their expressive power and their complexity.Our first result concerns a quantifier-free fragment of BooleanAlgebra with Presburger Arithmetic. We give a nondeterministicpolynomial-time algorithm for reducing the satisfiability of sets withsymbolic cardinalities to constraints on constant cardinalities, andgive a polynomial-space algorithm for the resulting problem. The bestpreviously existing algorithm runs in exponential space andnondeterministic exponential time.In a quest for more efficient fragments, we identify severalsubclasses of sets with cardinality constraints whose satisfiabilityis NP-hard. Finally, we identify a class of constraints that haspolynomial-time satisfiability and entailment problems and can serveas a foundation for efficient program analysis. We give a system ofrewriting rules for enforcing certain consistency properties of theseconstraints and show how to extract complete information fromconstraints in normal form. This result implies the soundness andcompleteness of our algorithms. |
| first_indexed | 2024-09-23T14:07:37Z |
| id | mit-1721.1/30561 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:07:37Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305612019-04-12T13:39:28Z On Algorithms and Complexity for Sets with Cardinality Constraints Marnette, Bruno Kuncak, Viktor Rinard, Martin Computer Architecture Typestate systems ensure many desirable properties of imperativeprograms, including initialization of object fields and correct use ofstateful library interfaces. Abstract sets with cardinalityconstraints naturally generalize typestate properties: relationshipsbetween the typestates of objects can be expressed as subset anddisjointness relations on sets, and elements of sets can berepresented as sets of cardinality one. In addition, sets withcardinality constraints provide a natural language for specifyingoperations and invariants of data structures.Motivated by these program analysis applications, thispaper presents new algorithms and new complexity results forconstraints on sets and their cardinalities. We studyseveral classes of constraints and demonstrate a trade-offbetween their expressive power and their complexity.Our first result concerns a quantifier-free fragment of BooleanAlgebra with Presburger Arithmetic. We give a nondeterministicpolynomial-time algorithm for reducing the satisfiability of sets withsymbolic cardinalities to constraints on constant cardinalities, andgive a polynomial-space algorithm for the resulting problem. The bestpreviously existing algorithm runs in exponential space andnondeterministic exponential time.In a quest for more efficient fragments, we identify severalsubclasses of sets with cardinality constraints whose satisfiabilityis NP-hard. Finally, we identify a class of constraints that haspolynomial-time satisfiability and entailment problems and can serveas a foundation for efficient program analysis. We give a system ofrewriting rules for enforcing certain consistency properties of theseconstraints and show how to extract complete information fromconstraints in normal form. This result implies the soundness andcompleteness of our algorithms. 2005-12-22T02:33:49Z 2005-12-22T02:33:49Z 2005-08-03 MIT-CSAIL-TR-2005-050 MIT-LCS-TR-997 http://hdl.handle.net/1721.1/30561 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 19 p. 33171425 bytes 1663929 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Marnette, Bruno Kuncak, Viktor Rinard, Martin On Algorithms and Complexity for Sets with Cardinality Constraints |
| title | On Algorithms and Complexity for Sets with Cardinality Constraints |
| title_full | On Algorithms and Complexity for Sets with Cardinality Constraints |
| title_fullStr | On Algorithms and Complexity for Sets with Cardinality Constraints |
| title_full_unstemmed | On Algorithms and Complexity for Sets with Cardinality Constraints |
| title_short | On Algorithms and Complexity for Sets with Cardinality Constraints |
| title_sort | on algorithms and complexity for sets with cardinality constraints |
| url | http://hdl.handle.net/1721.1/30561 |
| work_keys_str_mv | AT marnettebruno onalgorithmsandcomplexityforsetswithcardinalityconstraints AT kuncakviktor onalgorithmsandcomplexityforsetswithcardinalityconstraints AT rinardmartin onalgorithmsandcomplexityforsetswithcardinalityconstraints |