Saucy3: Fast Symmetry Discovery in Graphs (original) (raw)

Saucy - Summer 2004 Saucy2 - Summer 2008 Saucy3 - Spring 2012

Summary

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, seethis 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 theABC system for circuit synthesis and verification, developed at Berkeley. The command is saucy3. The algorithms will be described in a paper at ICCAD 2013.

Source Code

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 saucyand 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.

Benchmarks

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-EXTpage. Peter Cameron wrote a survey on regular graphs (2001)

References

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 1963paper 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 1982paper by Luks showing that graph isomorphism of bounded-degree graphs is poly-time

A STOC 1983paper by Babai showing poly-time canonical labeling of bounded-degree graphs

A 1992paper 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 1996paper by Spielman giving tighter analysis of individualization-refinement algorithms

A 2001survey paper on graph iso by Cameron

A 2007overview of nauty by Hartke and Radcliffe

A 2011 blisspaper on canonical labeling by Junttila and Kaski

People Involved in Research on Saucy(listed alphabetically)

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, byBrendan McKay.

bliss: another symmetry and canonical labeling program, byTommi Junttila andPatteri Kaski.

traces: a canonical labeling package byAdolfo Piperno

nishe: a canonical labeling package byGreg 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.

Acknowledgments

This work was funded in part by the National Science Foundation and by the DARPA/MARCO Gigascale Systems Research Center.