@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",
}