Source Code
Benchmarks
References
People Involved
Related Software Tools
Acknowledgments
|
Summary Source Code Benchmarks References People Involved Related Software Tools Acknowledgments |
|
Many computational tools have recently begun to benefit from the use of the symmetry inherent in the tasks they solve, and use general-purpose graph symmetry tools to uncover this symmetry. Common applications include organic chemistry, constraint solvers, logistics, optimization, bio-informatics, and finite group theory. However, older symmetry-finding tools often suffer quadratic runtime (or worse!) in the number of symmetries explicitly returned and are therefore of limited use on very large, sparse, symmetric graphs. Over the last 10+ years, we developed a symmetry-discovery algorithm which exploits the sparsity present not only in the input but also the output, i.e., the symmetry generators themselves. By avoiding quadratic runtime on large graphs, it improved state-of-the-art runtimes from several days to less than a second. Recent improvements to our algorithm include additional pruning that quickly solves the hard Miyazaki graphs.
Our implementation has been stable and reliable for many years. While it accounts for several types of sparsity, it works well on dense graphs too. As we continue looking for performance improvements, please send us any graphs on which saucy takes long time. If you find saucy useful in your applications, check this page for future updates. Also, consider citing some of our publications listed below, along with this URL.
Saucy currently does not deal with approximate symmetries and with spatial data. For spatial and visual symmetries, see this page.
June 2013: in addition to the current saucy implementation, we have developed an algorithm to find symmetries of Boolean functions represented by (sizable) circuits. Such functional symmetries may or may not be structural. For example, the n-input AND function has all possible permutations as its functional symmetries, but any minimal circuit (a tree) for this function loses most of those symmetries. Our implementation is being added to the ABC system for circuit synthesis and verification, developed at Berkeley. The command is saucy3. The algorithms will be described in a paper at ICCAD 2013.
The latest version of saucy is available upon request. Send an email to saucy.request@gmail.com, and tell us your name, affiliation, intended use of saucy and whether you agree to the terms of the saucy license. If you use saucy in a publication, please cite relevant publications from the list below.
The benchmarks used in our publications are available for download. Additionally, Brendan McKay generated more graphs than you could imagine. If that is not enough, several interesting graphs can be found at the GI-EXT page. Peter Cameron wrote a survey on regular graphs (2001)
Graph Automorphism from Wolfram Mathworld
P. Codenotti, H. Katebi, K. A. Sakallah and I. L. Markov, ``Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms,'' in Proc. Int'l. Conf. on Tools with artificial Intelligence (ICTAI), Washington DC, 2013.
H. Katebi, K. A. Sakallah and I. L. Markov, ``Graph Symmetry Detection and Canonical Labeling: Differences and Synergies,'' in Proc. Turing-100, Manchester, UK, 2012.
H. Katebi, K. A. Sakallah and I. L. Markov,
``Conflict Anticipation in the Search for Graph Automorphisms''
in Proc.
Int'l Conf. on Logic for Programming, Artificial Intelligence
and Reasoning (LPAR), pp. 243-257, Mérida, Venezuela, 2012.
H. Katebi, K. A. Sakallah, I. L. Markov, ``Symmetry and Satisfiability: An Update,'' in Proc. Satisfiability Symposium (SAT), Edinburgh, Scotland, July 2010.
P. T. Darga, K. A. Sakallah, and I. L. Markov,
“Faster Symmetry Discovery using Sparsity of Symmetries”,
Proceedings of
the 45th Design Automation Conference, Anaheim, California, June 2008.
[ppt]
[empirical results].
R. C. Johnson, “ Saucy algorithm exploits symmetries,'' EE Times, June 2008.
P. T. Darga, M. H. Liffiton, K. A. Sakallah, and I. L. Markov,
“Exploiting Structure in Symmetry Detection for CNF”,
Proceedings of
the 41st Design Automation Conference, pp. 530-534, San Diego,
California, June 2004.
[ppt]
A 1963 paper by Erdos and Renyi showing that most graphs are asymmetric
A 1980 paper by Babai, Erdos and Selkow showing that graph isomorphism of most random graphs is very easy
A 1982 paper by Luks showing that graph isomorphism of bounded-degree graphs is poly-time
A STOC 1983 paper by Babai showing poly-time canonical labeling of bounded-degree graphs
A 1992 paper by Cai and Furer lower bounds for graph iso (great survey of prior literature)
A SODA 1995 paper by Furer on poly-time isomorphism testing without numerics for graphs of bounded eigenvalue multiplicity
A STOC 1996 paper by Spielman giving tighter analysis of individualization-refinement algorithms
A 2001 survey paper on graph iso by Cameron
A 2007 overview of nauty by Hartke and Radcliffe
A 2011 bliss paper on canonical labeling by Junttila and Kaski
Paul T. Darga
Hadi Katebi
Mark Liffiton
Igor L. Markov
Karem Sakallah
All research was performed at the University of Michigan, in the Electrical Engineering and Computer Science department.
nauty: the original graph symmetry and canonical labeling program, by Brendan McKay.
bliss: another symmetry and canonical labeling program, by Tommi Junttila and Patteri Kaski.
traces: a canonical labeling package by Adolfo Piperno
nishe: a canonical labeling package by Greg Tener
conauto: a graph ismorphism package by José Luis López-Presa
GI-EXT: a graph iromorphism package by Daniel Cosmin Porumbel
shatter: adds symmetry-breaking predicates to CNF formulas to assist in determining their satisfiability, by Fadi Aloul.
This work was funded in part by the National Science Foundation and by the DARPA/MARCO Gigascale Systems Research Center.