Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Exploiting Symmetry in SMT Problems
verfasst von : David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Erschienen in: Automated Deduction – CADE-23
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here recast a technique to enhance the performance of SMT-solvers by detecting symmetries in the input formulas and use them to prune the search space of the SMT algorithm. This technique is based on the concept of (syntactic) invariance by permutation of constants. An algorithm for solving SMT by taking advantage of such symmetries is presented. The implementation of this algorithm in the SMT-solver
veriT
is used to illustrate the practical benefits of this approach. It results in a significant improvement of
veriT
’s performances on the SMT-LIB benchmarks that places it ahead of the winners of the last editions of the SMT-COMP contest in the QF_UF category.