paper ps
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.

### Citation

Bruno Marnette, Viktor Kuncak, and Martin Rinard.
Polynomial constraints for sets with cardinality bounds.
In *Foundations of Software Science and Computation Structures
(FOSSACS)*, volume 4423 of *LNCS*, March 2007.### BibTex Entry

@inproceedings{MarnetteETAL07PolynomialConstraintsSetsCardinalityBounds,
author = {Bruno Marnette and Viktor Kuncak and Martin Rinard},
title = {Polynomial Constraints for Sets with Cardinality Bounds},
booktitle = {Foundations of Software Science and Computation Structures (FOSSACS)},
series = {LNCS},
volume = {4423},
year = 2007,
month = {March},
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.
}
}