> < ^ From:

> ^ Subject:

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

> < [top]