On Algorithms and Complexity for Sets with Cardinality Constraints PSPACE and PTIME Logics for Program Analysis
Bruno Marnette, Viktor Kunčak, Martin Rinard · 2005
Typestate systems ensure many desirable properties of imperative programs, including initialization of object fields and cor rect use of stateful library interfaces. Abstract sets with cardinali ty constraints naturally generalize typestate properties: relationship s 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 cons traints 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 Boole an Algebra with Presburger Arithmetic. We give a nondeterministic polynomial-time algorithm for reducing the satisfiability of sets with symbolic cardinalities to constraints on constant car dinalities, 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 sati sfiability is NP-hard. Finally, we identify a class of constraints t hat has polynomial-time satisfiability and entailment problems an d can serve as a foundation for efficient program analysis. We give a system of rewriting rules for enforcing certain consistency pr operties 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.