SyMT: finding symmetries in SMT formulas

C. Areces, D. Deharbe, P. Fontaine, and E. Orbe. SyMT: finding symmetries in SMT formulas. In Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, Helsinki, Finland, 2013.

Download

[pdf] 

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]. We here propose SyMT, a simple tool based on graph automorphism detection algorithms to find out symmetries in SMT formulas. SyMT helps SMT users by highlighting the symmetries in theirformulas, giving thus hints on how they can improve them to enforce the SMT solver to examine one path out of many symmetric ones in the search tree. The classic propositional symmetry breaking technique can be lifted to SMT and yield 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.

BibTeX

@InProceedings{Areces2013,
  author =       "C. Areces and D. Deharbe and P. Fontaine and E. Orbe",
  booktitle =    "Proceedings of the 11th International Workshop on
                 Satisfiability Modulo Theories",
  title =        "{SyMT:} finding symmetries in {SMT} formulas",
  year =         "2013",
  address =      "Helsinki, Finland",
  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]. We here
                 propose SyMT, a simple tool based on graph automorphism
                 detection algorithms to find out symmetries in SMT
                 formulas. SyMT helps SMT users by highlighting the
                 symmetries in theirformulas, giving thus hints on how
                 they can improve them to enforce the SMT solver to
                 examine one path out of many symmetric ones in the
                 search tree. The classic propositional symmetry
                 breaking technique can be lifted to SMT and yield 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.",
  owner =        "areces",
  timestamp =    "2013.06.24",
}