From faloul@eecs.umich.edu Wed Feb 13 05:16:16 2002
Date: Wed, 13 Feb 2002 00:15:07 -0500 (EST)
From: Fadi Aloul <faloul@eecs.umich.edu>
To: gap@dcs.st-and.ac.uk
cc: Fadi Aloul <faloul@eecs.umich.edu>, Igor Markov <imarkov@eecs.umich.edu>
Subject: Symmetries

Dear GAP forum,

We are currently working on identifying symmetries of Boolean functions
using GAP/GRAPE/NAUTY.

We converted a few CNF-SAT instances to undirected bipartite graphs such
that a bi-colored symmetry (color1 for variables, color2 for clauses) of a
graph corresponds to a symmetry of the respective CNF formula. However,
when we have over 5000 vertices in the bipartite graph, GAP/GRAPE/NAUTY
are slow.

Therefore, by analyzing the structure of the original SAT problem, we
colored some variables differently (variables which can't be mapped to
each other by symmetries)

The number of different colors was in the hundreds. We thought this would
help speedup GAP/GRAPE, but it actually slowed GAP down.

Is there a good explanation for this? Any suggestions for speed
improvements would be appreciated (esp. those using functionalities in
NAUTY 2.0).

Thanks,
Fadi