[ list |
abstracts |
bib ]

## Decision Procedures for Multisets with
Cardinality Constraints

paper pdf
### Abstract

Applications in software verification and interactive
theorem proving often involve reasoning about sets
of objects. Cardinality constraints on such
collections also arise in these
applications. Multisets arise in these applications
for analogous reasons as sets: abstracting the
content of linked data structure with duplicate
elements leads to multisets. Interactive theorem
provers such as Isabelle specify theories of
multisets and prove a number of theorems about them
to enable their use in interactive
verification. However, the decidability and
complexity of constraints on multisets is much less
understood than for constraints on sets. The first
contribution of this paper is a polynomial-space
algorithm for deciding expressive quantifier-free
constraints on multisets with cardinality
operators. Our decision procedure reduces in
polynomial time constraints on multisets to
constraints in an extension of quantifier-free
Presburger arithmetic with certain “unbounded sum”
expressions. We prove bounds on solutions of
resulting constraints and describe a
polynomial-space decision procedure for these
constraints. The second contribution of this paper
is a proof that adding quantifiers to a constraint
language containing subset and cardinality operators
yields undecidable constraints. The result follows
by reduction from Hilbert's 10th problem.

### Citation

Ruzica Piskac and Viktor Kuncak.
Decision procedures for multisets with cardinality constraints.
Technical Report LARA-REPORT-2007-002, EPFL, 2007.### BibTex Entry

@TECHREPORT{PiskacKuncak07MultisetsCardinality,
author = {Ruzica Piskac and Viktor Kuncak},
title = {Decision Procedures for Multisets with
Cardinality Constraints},
year = 2007,
number = {LARA-REPORT-2007-002},
institution = {EPFL},
localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak07MultisetsCardinality.pdf}
}

[ list |
abstracts |
bib ]