Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Reducing the Complexity of Quantified Formulas via Variable Elimination

Reviewed Paper In Proceedings

Author(s):Aboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri, and Mihai Herda
In:11th International Workshop on Satisfiability Modulo Theories (SMT 2013)
Year:2013
Pages:87-99
URL:http://i57www.ira.uka.de/~ulbrich/pub/smt2013.pdf
Links:

Abstract

We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite set of sufficient ground terms can be eliminated by instantiating them with the computed ground terms. The resulting SMT formula contains potentially fewer quantifiers and thus is potentially easier to solve. We describe how a satisfying model of the resulting formula can be modified to satisfy the original formula. Our experiments show that in many cases, this simplification considerably improves the solving time, and our evaluations using Z3 and CVC4 indicate that the idea is not specific to a particular solver, but can be applied in general.

BibTeX

@INPROCEEDINGS{elghazi-ulbrich-taghdiri-herda-smt2013,
  author = {Aboubakr Achraf {El Ghazi} and Mattias Ulbrich and Mana Taghdiri and Mihai
	Herda},
  title = {Reducing the Complexity of Quantified Formulas via Variable Elimination},
  booktitle = {11th International Workshop on Satisfiability Modulo Theories (SMT 2013)},
  year = {2013},
  pages = {87--99},
  month = {July},
  abstract = {We present a general simplification of quantified SMT formulas using
	variable elimination. The simplification is based on an analysis
	of the ground terms occurring as arguments in function applications.
	We use this information to generate a system of set constraints,
	which is then solved to compute a set of sufficient ground terms
	for each variable. Universally quantified variables with a finite
	set of sufficient ground terms can be eliminated by instantiating
	them with the computed ground terms. The resulting SMT formula contains
	potentially fewer quantifiers and thus is potentially easier to solve.
	We describe how a satisfying model of the resulting formula can be
	modified to satisfy the original formula. Our experiments show that
	in many cases, this simplification considerably improves the solving
	time, and our evaluations using Z3 and CVC4 indicate that the idea
	is not specific to a particular solver, but can be applied in general.},
  url = {http://i57www.ira.uka.de/~ulbrich/pub/smt2013.pdf},
  links = {Slides:http://i57www.ira.uka.de/~ulbrich/pub/smt2013_slides.pdf}
}