Sciweavers

FOSSACS
2007
Springer

Polynomial Constraints for Sets with Cardinality Bounds

13 years 9 months ago
Polynomial Constraints for Sets with Cardinality Bounds
Abstract. Logics that can reason about sets and their cardinality bounds are useful in program analysis, program verification, databases, and knowledge bases. This paper presents a class of constraints on sets and their cardinalities for which the satisfiability and the entailment problems are computable in polynomial time. Our class of constraints, based on tree-shaped formulas, is unique in being simultaneously tractable and able to express 1) that a set is a union of other sets, 2) that sets are disjoint, and 3) that a set has cardinality within a given range. As the main result we present a polynomial-time algorithm for checking entailment of our constraints.
Bruno Marnette, Viktor Kuncak, Martin C. Rinard
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FOSSACS
Authors Bruno Marnette, Viktor Kuncak, Martin C. Rinard
Comments (0)