Exploiting Symmetry in SMT Problems

David Déharbe 1 Pascal Fontaine 2, 3 Stephan Merz 2, 3 Bruno Woltzenlogel Paleo 2, 3
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. Springer, 6803, pp.222-236, 2011, 〈10.1007/978-3-642-22438-6_18〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00617843
Contributeur : Pascal Fontaine <>
Soumis le : mardi 30 août 2011 - 15:53:59
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

Collections

Citation

David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Exploiting Symmetry in SMT Problems. Nikolaj Bjrner and Viorica Sofronie-Stokkermans. International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. Springer, 6803, pp.222-236, 2011, 〈10.1007/978-3-642-22438-6_18〉. 〈inria-00617843〉

Partager

Métriques

Consultations de la notice

193