Decision Procedures for Multisets with Cardinality Constraints

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},
  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.  }
}