Exploiting Symmetry in SMT Problems

David Déharbe, Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo

Abstract

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.

© Springer-Verlag 2011

Available as: PDF

Reference

@InProceedings{deharbe:symmetry,
  author =       {David D{\'e}harbe and Pascal Fontaine and Stephan Merz and Bruno {Woltzenlogel Paleo}},
  title =        {Exploiting Symmetry in {SMT} Problems},
  booktitle = {23rd Intl. Conf. Automated Deduction (CADE 2011)},
  pages =     {222-236},
  year =      2011,
  editor =    {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans},
  volume =    6803,
  series =    {LNCS},
  address =   {Wroclaw, Poland},
  publisher = {Springer},
}