SyMT: finding symmetries in SMT formulas

Abstract : The QF UF category of the SMT-LIB test set contains many formulas with symmetries, and breaking these symmetries results in an important speedup [8]. This paper presents SyMT, a tool to nd and report symmetries in SMT formulas. SyMT is based on the reduction of the problem of detecting symmetries in formulas to nding automorphisms in a graph representation of these formulas. The output of SyMT may be used to improve SMT formulas to enforce the SMT solver to examine only one assignment out of many symmetric ones. We show that the classic propositional symmetry breaking technique can be lifted to SMT and yields a generic technique to break the symmetries found by SyMT. Experiments on a large part of the SMT-LIB show that symmetries are pervasive in most categories.
Type de document :
Communication dans un congrès
11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00867816
Contributeur : Pascal Fontaine <>
Soumis le : lundi 30 septembre 2013 - 15:23:48
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

  • HAL Id : hal-00867816, version 1

Collections

Citation

Carlos Areces, David Déharbe, Pascal Fontaine, Orbe Ezequiel. SyMT: finding symmetries in SMT formulas. 11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland. 2013. 〈hal-00867816〉

Partager

Métriques

Consultations de la notice

158