Dear GAP forum,

My colleagues and I (and our students ;-) are studying
symmetries of boolean functions that arise in circuit design
and verification. For starters, we converted several SAT
instances in CNF into oriented bipartite graphs such that
a bi-colored symmetry of a graph corresponds to a symmetry
of the resp. CNF formula. We are using the GRAPE package
to compute symmetries.

To make the long story short, we are not able to test
even medium-sized CNF formulas for symmetries because it
takes too long. Of course, we are aware that non-trivial
symmetries are rare in random graphs, but expected that
at least the "no non-trivial symmetries" answer could be
produced quickly. In fact, we do not need *all* symmetries
(all generators of the group of symmetries), if *any* can
be found quickly that would be very good. However, it looks
like we can only hope for symmetries in medium-to-large
circuits, where component reuse is more common.

If anyone has time to look into possible speed-ups,
here is how to download sample instances (they are single-file
gap scripts):

Fadi Aloul wrote:
>
> http://www.eecs.umich.edu/~faloul/gap has three files with 70, 80, and 90
> nodes. They need 1, 50, and 3000 seconds respectively to be solved.
>
> They return no symmetries and they use very little memory (about 20MB
> only) although the machine has 256M and the -m & -o gap limits are set to
> 100M & 200M.
>
> Fadi

thanks for help,

Igor

P.S. I paper published several years ago at a formal verification
conference mentioned that the authors tried GAP but found it
way too slow for symmetry detection in circuits. They got away
with a very simple opportunistic algorithm that detected
2-vertex exchanges that preserved the graph. It should be possible
to detect larger classes of symmetries opportunistically, e.g., some
order-two symmetries.
--
Igor Markov (734) 936-7829 EECS 2211
http://www.eecs.umich.edu/~imarkov

Miles-Receive-Header: reply