SyMT: finding symmetries in SMT formulas

Areces, C., Deharbe, D., Fontaine, P., and Orbe, E.. SyMT: finding symmetries in SMT formulas. In Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, Helsinki, Finland, July 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: (download)

@INPROCEEDINGS{arec:symt13,
  author = {Areces, C. and Deharbe, D. and Fontaine, P. and Orbe, E.},
  title = {{SyMT:} finding symmetries in {SMT} formulas},
  booktitle = {Proceedings of the 11th International Workshop on Satisfiability
	Modulo Theories},
  year = {2013},
  address = {Helsinki, Finland},
  month = {July},
  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}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49