Saucy: Fast Symmetry Finding in Sparse Domains

source code (1.1) +[updated license terms] paper presentation benchmarks manual page

The search for symmetries of discrete objects can often be reduced to finding symmetries of sparse graphs. This latter problem is isomorphic to the graph isomorphism problem, a difficult (but not proved NP-complete) problem. Brendan D. McKay published the first practical algorithm for finding the symmetries of a graph; this work is available in his tool nauty. However, nauty is tuned to efficiently batch process many small graphs and does not scale to graphs with many vertices.

Graphs with millions of vertices or more are prevalent in many domains with interesting symmetries. For example, propositional logic formulas generated to model verification problems often exhibit considerable structural symmetry--there exist many rearrangements of the variables which yield the same formula. Shatter is a tool which takes the symmetries present in such a formula and appends additional predicates to achieve often exponentially faster Boolean satisfiability solving. In fact, Shatter makes SAT solving so fast for many problems that finding symmetries is the critical path in its flow.

Saucy makes symmetry finding fast for real-world propositional formulas and other domains because it takes advantage of the inherent structure present in them. The primary manifestation of this structure in the corresponding graphs is their sparsity: the number of edges present in the graph is roughly linear, as opposed to quadratic, in the number of vertices. Saucy takes advantage of this sparsity to achieve considerable gains in efficiency over nauty.

Saucy was introduced in this paper:
P. T. Darga, M. H. Liffiton, K. A. Sakallah, and I. L. Markov, ``Exploiting Structure in Symmetry Generation for CNF'', Proceedings of the 41st Design Automation Conference, pp. 530-534, San Diego, California, June 2004.

To get a better idea of how nauty and saucy work, and the improvements made by saucy, see the DAC 2004 presentation.

Of course, the best reference of all is the source code (version 1.1). The benchmarks used in the paper and talk are available if you want to try saucy out on some graphs arising in hardware verification. Running saucy is explained in its manual page.

Saucy is already in use in Shatter and GSymEx, a generalization of Shatter which extracts symmetries in a wide range of more general constraint satisfaction problems.

This work was funded in part by NSF ITR grant 0205288.