Section: New Results

Using symmetries in SMT

Participants : David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo.

Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We propose a similar technique for enhancing the performance of SMT-solvers by detecting symmetries in the input formulas and using 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 results in an impressive 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.

This technique has immediately been adopted by the SMT community. For instance, we are aware that Z3 (Microsoft) and CVC3 (University of New-York and University of Iowa) implemented this technique for the 2011 competition.