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.