Sets with Cardinality Constraints in Satisfiability Modulo Theories

paper ps   
Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier-free BAPA (QFBAPA). In contrast to many other NP-complete problems (such as quantifier-free first-order logic or linear arithmetic), the applications of QFBAPA to a broader set of problems has so far been hindered by the lack of an efficient implementation that can be used alongside other efficient decision procedures. We overcome these limitations by extending the efficient SMT solver Z3 with the ability to reason about cardinality (QFBAPA) constraints. Our implementation uses the DPLL(T) mechanism of Z3 to reason about the top-level propositional structure of a QFBAPA formula, improving the efficiency compared to previous implementations. Moreover, we present a new algorithm for automatically decomposing QFBAPA formulas. Our algorithm alleviates the exponential explosion of considering all Venn regions, significantly improving the tractability of formulas with many set variables. Because it is implemented as a theory plugin, our implementation enables Z3 to prove formulas that use QFBAPA constructs with constructs from other theories that Z3 supports, as well as with quantifiers. We have applied our implementation to the verification of functional programs; we show it can automatically prove formulas that no automated approach was reported to be able to prove before.

Citation

Philippe Suter, Robin Steiger, and Viktor Kuncak. Sets with cardinality constraints in satisfiability modulo theories. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011.

BibTex Entry

@inproceedings{SuterETAL11SetswithCardinalityConstraintsin,
  author = {Philippe Suter and Robin Steiger and Viktor Kuncak},
  title = {Sets with Cardinality Constraints in Satisfiability Modulo Theories},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2011,
  abstract = {   Boolean Algebra with Presburger Arithmetic (BAPA) is a
  decidable logic that can express constraints on sets of
  elements and their cardinalities. Problems from
  verification of complex properties of software 
  often contain fragments that belong to
  quantifier-free BAPA (QFBAPA).  
  In contrast to many other NP-complete problems (such
  as quantifier-free first-order logic or linear arithmetic),
  the applications of QFBAPA to a broader set of problems has
  so far been hindered by the lack of an efficient
  implementation that can be used alongside other efficient
  decision procedures.
  We overcome these limitations by extending the efficient
  SMT solver Z3 with the ability to reason about cardinality (QFBAPA)
  constraints. Our implementation uses the DPLL(T) mechanism
  of Z3 to reason about the top-level propositional
  structure of a QFBAPA formula, improving the efficiency
  compared to previous implementations.  Moreover, we
  present a new algorithm for automatically decomposing 
  QFBAPA formulas. Our algorithm alleviates the exponential
  explosion of considering all Venn regions, significantly
  improving the tractability of formulas with many set
  variables.  Because it is implemented as a theory plugin,
  our implementation enables Z3 to prove formulas that use
  QFBAPA constructs with constructs from other theories
  that Z3 supports,
  as well as with quantifiers.  We have applied our
  implementation to the verification of functional programs; we
  show it can automatically prove formulas that no automated
  approach was reported to be able to prove before. }
}