> < ^ From:

> ^ Subject:

Dear Forum,

Igor Markov writes:

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.

Sorry, what exactly is a "bi-coloured" symmetry?

Is it a symmetry that preserves parts of the the bipartition

setwise? (i.e. does not flip them?)

I looked at the graph in your 3rd example: http://www.eecs.umich.edu/~faloul/gap/ran-20_70-S3.gap If one lookes at it as an undirected graph (call the GRAPE function UnderlyingGraph), then is has the following bipartition: [ [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 ], [ 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90 ] ] Is this the bipartition that you study? If yes, then in principle you should use AutGroupGraph with two parameters, giving the bipartition as the second one. (although in this particular case it makes no difference, as the bipartition is preserved due to the fact that the vertices from different part have different (non-oriented) valencies).

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

>

I had a look at the 3rd example:

http://www.eecs.umich.edu/~faloul/gap/ran-20_70-S3.gap

Regarding your particular computation, IMHO it appears that you might have

hit a particular problem (3000 seconds is way too long for such a tiny

graph; I'd say few seconds at most should be the correct running time,

most of it consumed in exchange of information between GAP and Nauty)

in Nauty (the program that is used to compute the automorphism group,

see the documentation on Grape, see http://cs.anu.edu.au/~bdm/nauty/ ).

In fact, this is probably due to fact that you work with directed

graphs, that are not so commonly used. You might like to contact

Brendan McKay, the author of Nauty, to make him aware of this problem.

The graph in question in Nauty (dreadnaut format) is attached.

I converted the graph into undirected one (see above), and computed

the automorphism group of it (it took few seconds on an old Pentium,

as it ought to be).

It turned out to be Group( (21,41), (24,52) ). As none of these 2

generators are automorphims of the original graph, the latter does not

have automorphisms.

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.

The fact that little memory is used is no surprise, as Nauty

uses a very compact bitwise representation of graphs, and the

algorithm is not memory-hungry. (and the resources that GAP needs here

are minimal).

------------------------------------------------------------------

To make the long story short, we are not able to test

even medium-sized CNF formulas for symmetries because it

takes too long

[...]

Are these examples (on 70, 80, and 90 nodes) that you have at

http://www.eecs.umich.edu/~faloul/gap

what you call "medium-sized" ?

I would rather call them small, at least w.r.t. what programs

that compute automorphism groups of graphs can do for you.

In fact, a 1000 nodes is quite doable.

Perhaps, a small pre-processing, like finding

connected components first and checking for symmetries

within each component first, and then testing each pair of

components for isomorphism would help to speed your computations up.

Also, if you rather expect that your graphs have no automorphisms,

it is usually not so hard to come up with some invariants that

show so (like valencies of vertices, number of triangles on a fixed

edge, etc...)

Finally, as I said above, IMHO it appears to be a problem with Nauty

working with directed graphs. Using undirected graphs with the trick I

suggested above might be a temporary way out, at least allowing to do

experiments on instances with several hundred nodes.

HTH,

Dmitrii

http://ssor.twi.tudelft.nl/~dima/

----------------- cut here ---------------------- d $1n90g 39 51 53 60 64 70 81 83; 23 36 38 51 62 68 69; 36 59 62 89; 26 36 43 45 54 79 82 86; 33 34 61; 25 28 37 46 61 64 87; 21 41 58 82; 25 41 42 50 51 63 74; 26 47 52 90; 26 42 86; 33 58 75 83; 35 38 57 76 87; 22 35 43 59 70 78; 46 54 67 72 81 86; 40 49 53 62 87; 23 24 30 40 52 58 75 76 85; 35 39 56 63 68; 28 55 69 89; 25 44 64 69; 27 76 78; 8 18; 1 5; 4; 9 20; ; ; 4 15; 10; 5 14 16; 6 11; 7 14 20; 10 19 20; 14; 4 12; ; ; 2 20; 16; 12; 11; 18; 4; 5; 8 18; 2 13; 3; 6 11; 1 7 12; 8 11; 2 20; ; 20; 18; 19; 5 11; 7 19; 1 9; ; 4; 9 11; 9; ; 14; ; 8 17 18; 6 7 15; 5 9; 11; ; 9; 2 6 10; 9 20; 4 16 17; 1 12; 19; ; 2 3 13; 7; 8 12; 1 12 13; 13; 8; 19; 5 15 16; 9 19; ; ; 9 15 17; 6; 8 11.

> < [top]