[ list |
abstracts |
bib |
http ]

## On Algorithms and Complexity for Sets with Cardinality Constraints

paper pdf
paper ps
### Abstract

Typestate systems ensure many desirable properties of imperative
programs, including initialization of object fields and correct use of
stateful library interfaces. Abstract sets with cardinality
constraints naturally generalize typestate properties: relationships
between the typestates of objects can be expressed as subset and
disjointness relations on sets, and elements of sets can be
represented as sets of cardinality one. In addition, sets with
cardinality constraints provide a natural language for specifying
operations and invariants of data structures.
Motivated by these program analysis applications, this
paper presents new algorithms and new complexity results for
constraints on sets and their cardinalities. We study
several classes of constraints and demonstrate a trade-off
between their expressive power and their complexity.
Our first result concerns a quantifier-free fragment of Boolean
Algebra with Presburger Arithmetic. We give a nondeterministic
polynomial-time algorithm for reducing the satisfiability of sets with
symbolic cardinalities to constraints on constant cardinalities, and
give a polynomial-space algorithm for the resulting problem. The best
previously existing algorithm runs in exponential space and
nondeterministic exponential time.
In a quest for more efficient fragments, we identify several
subclasses of sets with cardinality constraints whose satisfiability
is NP-hard. Finally, we identify a class of constraints that has
polynomial-time satisfiability and entailment problems and can serve
as a foundation for efficient program analysis. We give a system of
rewriting rules for enforcing certain consistency properties of these
constraints and show how to extract complete information from
constraints in normal form. This result implies the soundness and
completeness of our algorithms.

### Citation

Bruno Marnette, Viktor Kuncak, and Martin Rinard.
On algorithms and complexity for sets with cardinality constraints.
Technical report, MIT CSAIL, August 2005.### BibTex Entry

@TECHREPORT{MarnetteETAL05AlgorithmsComplexitySetsCardinalityConstraints,
author = {Bruno Marnette and Viktor Kuncak and Martin Rinard},
title = {On Algorithms and Complexity for Sets with Cardinality Constraints},
institution = {MIT CSAIL},
year = 2005,
month = {August},
url = {http://arxiv.org/abs/cs/0508123},
localurl = {http://lara.epfl.ch/~kuncak/papers/MarnetteETAL05AlgorithmsComplexitySetsCardinalityConstraints.pdf}
}

[ list |
abstracts |
bib |
http ]