On the Complexity of Extending Ground Resolution with Symmetry Rules

1 Introduction

Symmetries in theorems have long been recognized to induce symmetries in proofs, and used to avoid the bore­ dom of repetitive arguments. As such, this rule of meta­ reasoning can be considered as a useful trick for writing proofs, and hence for discovering them, but by no means is it accredited as a powerful method for gaining deep knowledge of the problem at hand (except when sym­ metries are the subject of the problem, but this is out of the scope of our concern). Indeed, when this argument is invoked (e.g. "case 2 is similar") , the symmetry is supposed to be self-evident, not deserving any proof.

However, the appearance of computers and their use to assist in rigorous proofs shed a new light on the sub­ ject . Experience shows that computers never get bored, even on repetitive work that could be avoided. But expe­ rience also shows that users often get bored when their computer spends more time than expected for solving seemingly trivial problems. Hence the necessity to help computers think twice before doing something, and allow them to conclude: case 2 is similar.

*This work has been partly supported by CNRS.

One way to do this is to reason in a highly expressive logic, in which symmetry arguments can naturally be expressed. This is usually the case when all non-logical symbols can be quantified. However, such higher order logics are seldom used in Artificial Intelligence. It should also be noted that specific calculi, or strategies, may not be able to reach such arguments. Hence the very natural idea to extend calculi with symmetry rules , and provide strategies for using them. Indeed, the idea appeared in the literature as early as 1959, in [Gelernter, 1959] 1 . Maybe this was too early: to our knowledge, this paper has had no lineage in the following decades. It is written in a setting that looks weird today, and makes it difficult to read. By the way, [Gelernter, 1959] is only concerned with symmetries as permutations of first-order variables, and gives a rather complicated algorithm for computing these, which may appear as a waste of computational time.

It is only 26 years later that Krishnamurty, in [Krish­ namurty, 1985], introduced his symmetry rules (without reference to [Gelernter, 1959]) to extend propositional resolution, and showed on difficult examples how these rules can be used to reproduce natural arguments. These rules, and the complexity of the problems they involve, are the main concern of the present work, and are defined below. Since 1985, little work has been devoted to this problem (the implementation of [Benhamou and Sais, 1994] is discussed below). This should be surprising to anyone sharing Slaney's opinion: "I consider symmetry to be one of the most important topics of current re­ search in ground theorem proving" (see [Slaney, 1994]).

In the sequel , we will refer to notions from computa­ tional complexity (see [Garey and Johnson, 1979]), graph and group theory (see [Hoffmann, 1981]) , which we will introduce when needed. A clause is a set of literals. A set S of clauses is on a set of literals L , or L is for S iff the literals occurring in S also occur in L. For l E L, zc is the complementary literal of l.

Given a resolution derivation of a clause C from a set of clauses St on L1 (noted S1 f- C), one can obtain a new derivation by substituting new literals to those in L1 , under the following conditions: the literals resolved upon should remain complements after the substitution, and they should occur in the clauses, which means that they shouldn't have been resolved away sooner in the resulting proof. Hence the conditions that a substitu­ tion (T , say a function from £ 1 to £ 2, should satisfy: first , (T should preserve complementarity (Vi E £ 1, if lc E £1 then (TW) = (T(ln , and second, it should be injective. We note Subst(L1, £ 2) the set of these func­ tions. Hence for all 51 on £ 1, (T E Subst(L1, L2), if 51 f- C then (T(Sl) f- cr(C) . While refuting 52, a set of clauses on £2 , and a clause C being derived from 51 c 52, it is therefore correct to infer (T(C) provided cr(Sl) C S2. This inference rule depends on the proof of C, or more precisely on the hypotheses used in this proof, and can therefore be formalized in sequent style. Let Syms2(Sl) = {(T E Subst(L1,L2)/(T(S!) c S2} be the set of symmetries of sl in 52, the general symmetry rule is:

1 We thank Ricardo Caferra for pointing us to this paper.

To avoid this dependency, which is not quite in the "spirit" of resolution, we consider a restriction of this rule by requiring that S1 = S2 (and £1 = £2) . Let Syms = {cr E Subst(L, L)/(T(S) C S} be the set of S­ symmetries, then the S-symmetry rule is:

It is therefore correct to extend resolution with the general symmetry rule, which essentially yields Krishna­ murty's SR-11 symmetric resolution proof system. It is also correct Lo extend resolution (on a set of clauses S) by the S-symmetry rule, resulting in SR-I. It is doubt­ ful whether SR-I can polynomially simulate SR-11, but it has nice properties: the S-symmetry rule is simple, S-symmetries can be computed before drawing any in­ ference from S, and Syms forms a permutation group on the considered set of literals L for S (the identity is I dL; the trivial subgroup I is restricted to the identity) . This is obvious since Syms = {(T E Subst(L , L)/(T(S) = S}, which comes from the fact that the extension of (T to sets of literals (when confusion is possible, this exten­ sion will be noted u) is injective since (Tis injective, hence I(T(S)I =lSI , but cr(S) C Sis finite , hence (T(S) = S .

Dealing with complexity, we will refer to the length of particular objects (sets of clauses, sequences of permuta­ tions ... ), which means the length of the representation of this object in any reasonable (unspecified) encoding (see [Garey and Johnson, 1979]) . Given two problems P and Q, we note P cxp Q (P polynomially reduces to Q) when the existence of a polynomial time algorithm for Q implies the existence of a polynomial time algorithm for P. =:.p is the symmetric closure of cxp.

2 Detecting general symmetries

We address the problem of the amount of computa­ tion required in order to apply the general symmetry rule in a non trivial way. This means the search for a (T E Syms, (S!) such that (T(C) -::J C . The in­ put of this problem is £1, L2, S1, S2 and C , such that £1 C £2, S1 C S2, S1 is on £1 and 52, Care on £ 2. The output is a sequence of elements of £ 1 x £ 2 representing such a symmetry (T. This problem is obviously in NP: this sequence, which length is polynomia1 in l£11, can be guessed and checked in polynomial time.

2 As noted by a referee, the condition S1 C S2 is not neces­ sary to the correction of the rule, but elements of Syms 2 (S!) could not be considered as symmetries without it.

In the sequel, we consider the simpler decision prob­ lem 3(T E Syms, (S!) such that (T -::J I dL,, which poly­ nomially reduces to the previous one: such a (T exists iff 3l E L1 , ::J(T' E Syms 2 (S!) such that (T'({l}) -::J {l} .

2.1 The graph restriction

Let G = (V, E), G' = (V', E') be two graphs , a homo­ morphism from G to G' is a function a from V to V', such that a (E) C E'. Let M on ( G, G') be the set of in­ jective homomorphisms (monomorphisms) from G toG'. Also, a is an isomorphism from G to G' if a is bijective and a(E) = E', and Aut( G) is the set of isomorphisms from G to G ( automorphisms) . G is a subgraph of G' if V C V' and E C E'; this is noted G C G'.

It is clear that a set of edges E can be considered as a set of clauses on V, and conversely that any set S of clauses of length 2 (2-clauses) on L, without negation, can itself be considered as a set of edges on the vertex set L, yielding a graph (L , 5). Moreover, we have:

LEMMA 2.1 Let G = (V,E) C G' = (V',E') , then SymE'(E) = Mon(G,G').

Proof. (T E Mon(G,G') iff (T : V -tV' is injective and (T(E) c E', iff (T E 5ubst(V, V') and (T(E) c E', iff (T E SymE' (E). Q.E.D.

Hence, given any problem P on Syms' (S), with L, L', S, S' among the input, we can consider its restric­ tion to sets of 2-clauses without negation, and translate it as a problem on Mon(G ,G'), having as input G and G', and consequent restrictions of the rest of the input of P. This will be called the graph restriction of P .

As for sets of clauses, the finite nature of graphs im­ plies that M on(G, G) = Aut( G), thus lemma 2.1 on G = G' = (V, E) yields SymE =Aut( G). Hence graph restriction of problems on Syms translate on Aut (G).

2.2 Monomorphisms and rigid graphs

The graph restriction of our problem therefore consists in detecting the existence of a a EM on(G, G')\{Idv }, where G = (V, E) is a subgraph of G'. This problem will be simplified by further restricting it . A graph G is rigid if Aut( G) =I; it is connected if any two vertices are connected by a path (a sequence of adjacent edges). Any graph can be expressed as a disjoint union (noted +) of connected graphs, its connected components.

Given a homomorphism a from G to G', it is clear that if G is connected, then a (G) is connected, and is a subgraph of a connected component of G'. Also, the valence of vertices (noted vale ( v), the number of edges of G adjacent to v) increases by a: Vv E V, valc(v) ~ vafc,(a(v)). Moreover, if a is an isomorphism, Vv E V, va[c,(a(v)) = valc(v).

LEMMA 2.2 Let G = (V, E) , G' = (V', E') be two dis­ joint graphs (V n V' = 0), if G is connected, then Mon(G, G') = Mon(G, G + G')\Aut(G).

Proof. Let a E Mon(G,G'), then a E Mon(G ,G+G'), and also a (j. Aut( G) since a is into V'. Conversely, let a E M on(G, G + G') such that a (j. Aut(G) = Mon(G G) hence 3v E Vja(v) E V'. But a(G) is a ' ' G' h f subgraph of a connected component of G + , ence o G' alone , since G and G' are disjoint. Hence a(V) C V', and a E Mon(G, G'). Q.E.D.

We can now restrict our problem M on(G, G') #I to the input G, G + G' (G C G + G'), where G is rigid and connected: this restriction is equivalent to the problem Mon(G, G') # 0. We call it the Rigid Connected ~raph Monomorphism problem (RCGM for short), which we just proved to be polynomially reducible to the search for non trivial symmetries. RCGM is therefore NP, and we prove its NP-completeness by reducing CLIQUE to it.

2.3 Cliques and monomorphisms

The well-known NP-complete CLIQUE problem con­ sists in detecting in G a complete subgraph of k ver­ tices (a k-clique), where G = (V, E), ~ :S JVI are given . Since a clique is not rigid, we bmld the graph J{k = ({(i , j)/0:::; i:::; j:::; k, 1:::; j},KEk), where

If 1 :::; i < j :::; k, then valK.((i,j)) = 2 and valK.((j,j)) = 1. The subgraph of J{k generated by { (0 , 1) , .. . , (0, k)} is a k-clique (see figure 1) .

LEMMA 2.3 Vk > 2, f{k is rigid.

Proof. Let a E Aut(I<k), then Vj E {1. .. k}, valK.((O,j)) = k > 2, hence ~j' E {1: .. k},a.((?,,j)) = (O,j'), and then Vi E {1. .. J},a((z,J)) = (z,J ), but valK.((j,j')) = valK.(a((j,j))) = valK_.((j,j~) =.1, hence j = j' . This for all j, hence a IS the Identity on the vertex set of f{k· Q.E.D.

We are now going to embed a k-clique in a graph G = (V, E) by embedding f{k in an extension G_k of G, defined as follows : Gk = (Vk , Ek) where Vk = {(z, v)/ iE {O ... k},v E V} and

Vv E V, vala.((k,v)) = 1 and ViE {1 ... k-1}, vala.((i,v)) = 2. The subgraph of Gk generated by {(0 , v)jv E V} is isomorphic toG (see figure 1) .

THEOREM 2.4 Let G = (V, E) be a graph and k such that 2 < k < JVI, G contains a k-clique iff M on(Kk, Gk) # 0.

Proof. If G contains a k-clique v1 . .. Vk, it is triv­ ial to build a monomorphism a from Kk to Gk with a((O,j)) = (O,vj )· Conversely, let a E Mon(Kk ,Gk) , since Vj E {1 .. . k},vala.(a((O,j))) 2: k > 2, then 3v· E V,a((O,j)) = (O,vj) · Let G' be the subgraph of G Jgenerated by { v1 , ... , Vk}; since a is injective, it has k distinct vertices, and Vi, j E { 1 . .. k} , i # j , we have ((O, i) , (O, j)) E I<Ek, hence ((O,vi),(O, vj )) E Ek, and (vi, vj) E E, which proves that G' is a k-clique. Q.E.D.

CoROLLARY 2.5 RCGM, and all the intermediate pro­ blems up to the problem of computing a non trivial gen­ eral symmetry, are NP-complete.

3 Detecting S-symmetries

We now address the problem of the complexity of ap­ plying the S-symmetry rule in a non trivial way, which is a restriction of the previous one, and is therefore in NP. We first consider the simpler problem of detecting non trivial symmetries, i.e. let SYM be the problem Sym5 #I, having L and Son L as input. By lemma 2.1, the graph restriction of SYM is the problem of de­ tecting a non trivial automorphism of a graph, known as GA. Hence GA cxp SYM, and a polynomial algorithm for SYM would yield one for GA, which is very unlikely (GA is not even known to be in co-NP) .

Before attempting to prove the converse, we should mention that SYM is not exactly the problem we need to solve: we are more interested in the associated search problem S-SYM (to compute a non trivial symmetry if there is one). But the search problem associated toGA, say S-GA, may not be polynomially equivalent to GA. It will not be possible to reproduce the argument of the previous section, where the NP-completeness of the de­ cision problem made the associated search problem pol.y­ nomially equivalent to it . Hence we have to carefully dis­ tinguish the different problems we consider, beginni~g with CSYM: given L, S on L and a clause C on L, IS there a u E Sym5 such that u( C) # C? The associated search problem S-CSYM is the one needed for non trivial applications of the S-symmetry rule. The graph restric­ tion of CSYM will be noted CGA: given G = (V, E) and V' C V, is there a a E Aut(G) such that a(V') # V'?

We will frequently refer to the following problem, noted GI: given two graphs, are they isomorphic? This is a well-known NP problem that seems to be non NP­ complete (hence the same holds for GA, since GA. cxp G I) . There are quite a lot of problems polynomially equivalent to GI, called isomorphism-complete, am?ng which the associated counting problem (how many ISO­ morphisms between two graphs, see [Mathon, 1979]) , bringing evidence for the non-NP-completeness of Gl. For deeper evidence, see [Kobler et al., 1992]. Other isomorphism-complete problems of more direct interest to us refer to group-theoretic notions on graph auto­ morphisms, or more precisely on the permutation group Aut( G) , notions we therefore have to introduce.

Given a permutation group g on a permutation do­ main X, the orbit of x E X is x 9 = {y E X/3<p E 9, x<p = y} ( x<p is standard notation for <p( x), as well as <pl/J for 1/J o <p). The relation { (x, y) / x E y 9 } is an equiva­ lence relation, and the orbits form a partition of X, noted Part(9). Two literals l, l' are symmetric if l' E zsyms. To any problem P for which the set of solution forms a permutation group g, we associate the problem 0-P of computing Part(9).

We address the problem of establishing as precisely as possible the complexity classes of the problems associ­ ated with SYM. The graph restriction trivially yields S­ GA cxp S-SYM, 0-GA cxp 0-SYM and CGA cxp CSYM. Apart from SYM and S-SYM, we are going to show that GI polynomially reduces to all the other problems associ­ ated with SYM. First, it is proved in [Mathon, 1979] that GI cxp 0-GA, hence we directly obtain GI cxp 0-SYM.

Consider the problem 1R-GA (GA with one restric­ tion): given a graph G = (V, E) and v E V, is there a a E Aut( G) such that a(v) -::f v? It is proved in [Lubiw, 1981] that GI cxp 1R-GA. But it is trivial to see that 1R-GA cxp CGA, since 1R-GA is exactly the restriction of CGA to the case where IV' I= 1. Hence GI cxp CSYM CXp S-CSYM.

In order to prove these relations in the reverse direc­ tion, we need to establish a kind of converse to lemma 2.1 (restricted to G = G'). Let S be a set of clauses, we first consider the set of literals Ls defined as the smallest one for S that is complete for complementarity: Vl E Ls, zc E Ls. Clearly, Ls can be computed in poly­ nomial time in the length of S. For any liter all, z+ refers to l stripped of its possible negation, and z- to (l+ )c.

We now consider the graph 3 Gs = (Vs, Es) such that Vs = Ls USU N with N = {(i,l)/l E Lt,i E {1 ... 4}} and

We have Vl E L!,valc 5 ((1,l)) = 1, valc 5 ((2,l)) valc 5 ((3,l)) = 2, and valc 5 ((4,l)) = 3 (see figure 2).

LEMMA 3.1 Va E Aut(Gs), Vl E L!, we have a(l) E Ls and ViE {1 . .. 4}, a((i,l)) = (i,a(l)+).

Proof. Since valc 5 (a((1,l))) = 1, the first possibility is a((1,l)) = l' with l' E Ls and VC E S,l' ~C. Hence a( (2, l)) = (4, ['+),which is impossible since the valences of these vertices are different. The second possibility is a((1,l)) = C = {l'} E S, hence a((2,l)) = l', which therefore should not appear in any other clause, and hence a((3,l)) = (4,l'+), which is impossible.

3 We cannot use the graph construction from [Basin, 1994], although it has similarities with ours, since it is unable to take account of the double negation law.

The only possibility is therefore a((1,l)) = (1,l') (re­ alized by a= Idv 5 with l' = l), hence a((i,l)) = (i,l') for i = 1 ... 4, and either a(l) = l' or a(l) = l'c. In both cases l' = a(l)+. Q.E.D.

For all a E Aut ( G s), we note a· the restriction of o: on Ls. We then have:

LEMMA 3.2 Va E Aut(Gs), then Vl E Ls,a*W) = a*(l)c and VC E S, c;..-(C) = a(C).

Proof. Vl E Ls, let l' = a(l+) E Ls from lemma 3.1, and als? a(~_4,l:)) = (4,['+). Since a((3,t+)) = (3,l'+), and a IS biJective, then a(l+) E {t'+,z'-} = {l',l'c}, and a(l-) E {l',l'c}\{a(l+)}. Hence a*W) = aW) = a(W = a*(W.

Hence a(N) = N (lemma 3.1) and a(Ls) = Ls. Hence VC E S, a( C) E S, and Vl E Ls, a(l) E a( C)¢> (a(l),a(C)) E Es ¢? (l,C) E Es ¢? l E C, hence a(C) = {a(l)/l E C} = c;..-(C). Q.E.D.

THEOREM 3.3 The function · is an isomorphism from Aut(Gs) onto Syms.

Proof. By lemma 3.2, · i.s into Syms: Va E Aut(Gs), a· is~ complementarity preserving permutation of Ls, and c;..-(S) = a(S) = S.

· is onto Syms: for <T E Syms, let a : Vs -+ Vs such that Vl E Lt,Vi E {1 ... 4},a((i,l)) = (i,<T(l)+), and Vl E Ls, a(l) = <T(l) (hence a· = <T), and VC E S, a(C) = O'(C). Of course, a E Aut(G5 ): edges on N, Ls are trivially preserved, and Vl E Ls, VC E S, (l, C) E Es ¢? l E C ¢? <T(l) E O'(C) ¢? a(l) E a( C) ¢? (a(l), a( C)) E Es.

· is an homomorphism: Va,j3 E Aut(Gs), Vl E Ls , we have l(aj3)* = laj3 = la*j3 = la*j3* (since la* E Ls), hence (a j3) · = a· j3*.

· is an isomorphism: let a E Aut( G s) such that a· = ldLs, then V(i,l) E Vs,a((i,l)) = (i,a(l)) = (i,l), and VC -E S, by lemma 3.2, we have a(C) = c;..-(C) = C, hence a= Idv 5 . This proves Ker· =I. Q.E.D .

4 Generating S-symmetries

An immediate consequence of theorem 3.3 is SYM cxp G A, since the graph G s can be constructed in poly­ nomial time in the length of S, and Syms is triv­ ial iff Aut(Gs) is trivial. Hence SYM =.p GA. Fur­ thermore, we also have S-SYM cxp S-GA since for all a E Aut(Gs)\I, the non trivial S-symmetry a· can be computed in polynomial time. Hence S-SYM =.p S-GA.

Similarly, we could prove 0-SYM cxp 0-GA, and use 0-GA cxp GI from [Mathon, 1979]. However, the reduc­ tion in [Mathon, 1979] involves O(n 2 ) calls to GI (where n is the number of vertices), and therefore does not yield a tractable algorithm for 0-SYM. In this section we focus our attention on algorithmic issues, in order to provide realistic reductions from problems for which realistic al­ gorithms exist. We will especially consider the problem of generating the group Syms, in a particularly useful way to be defined below.

4.1 Elements of computational group theory

The material in this section is mainly taken from [Hoff­ mann, 1981], with almost the same notations. Let 9 be a group with identity e, and 1l a subgroup of 9, noted 1{ < 9 . For a E 9 , 1la = {ha/h E 1l} is a right coset of 1{ in 9. It is known that 11la I = 11ll, and that the right cosets of 1l in 9 form a partition of 9, which yields La­ grange's theorem: if9 is finite, then 3k E IN, 191 = kl1ll. Let a1 ... ak E 9 such that {1la;ji = 1 ... k} is the par­ tition of right cosets of 1l in 9 and i # j ~ 1la; # 1laj , then { a1 .. . ak} is a complete right transversal of 1l in (} . Since 1l = 1le is a right coset, then 3i/1la; = 1l, and { e} U { a1 ... ak} \ {a;} is also a complete right transversal of 1{ in 9: we can always choose to include the identity in complete right transversals.

Given a subset A C 9, the subgroup generated by A , noted <A>, is the smallest subgroup of 9 containing A; then A is a generator set for <A>. A matriochka in 9 is a finite sequence of subgroups 9r < . . . < 91 < 9o such that 9r = I and 9o = 9. For i E {1 . .. r}, if U; is a complete right transversal of 9; in 9;-1, then Va E 9;-1, 3!b; E U; such that a E 9;b;, hence such that abi 1 E 9;. By induction we see that Va E 9, 3!b1 E U1, ... , 3!br E Ur such that ab1 1 .. . b; 1 = e, hence a = br ... b1 . U~= 1 U; is therefore a computationally useful generator set for 9, provided r and the U; 's are small .

If 9 is a permutation group on X finite , and Y C X, the pointwise stabilizer of Y in 9 is 9[Y] = { <p E 9/ Vy E Y, y<p = y} . Y is a base of 9 if 9[Y] = I . It is not difficult to show that VY' C Y, 9[Y] < 9[Y']> 9[0] = 9 and 9[x] =I. Hence to any linear ordering (x1 , ... , Xn) of the elements of X we can associate the matriochka g (n) < .. . < 9 ( 0 ), where 9(i) = 9[{x,. xi}]· Let U; be a complete right transversal of 9(i) in 9(i- 1 ) for i = 1 ... n .

V<p , 1/J E 9 (i - 1), we have x;<p = x;'I/J {::} X;<p'I/J- 1 = x; <=> <p'I/J-1 E 9 (i) {::} <p E 9 (i)1/J. Hence if 1/J, 1/J' E U;, then 1/J ::f 1/J' {::} x;'I/J # x;'I/J'. Since x;'I/J E {x; . . . xn}, there are at most n- i + 1 possibilities, hence IU; I ~ n- i + 1, and IU7=1 U;l::; n(n 2 +1); we have at most O(n 2 ) generators for 9, and elements of 9 can be uniquely expressed as compositions of at most n generators.

A representation matrix is a n x n matrix M such that M[i , j] either is empty, or if i < j, M[i,j] is a permutation of X such that Vi' < i, x;,M[i, j] = x;' and x;M[i , j] = Xj, or if i = j, M[i , j] is Idx . Note that M is triangular. M then represents the set T(A , where Tf = {1/JM[k,j]/1/J E Tf:- 1 ,j E {k .. . n} ,M[k,j] # empty} and T;-t = {M[n, n]} = I; permutations are composed from the nth line to the first.

For any permutation <p of X , <p E T(A {::} 31/J E T.fi, 3j E {1. .. n} , <p = 1/JM[1,j] . But x1<p = x1 1/JM[1,j] = x1M[1,j] = Xj , hence <p E T(A {::} x1<p = Xj ,M[1 , j] # empty and <pM[1,j]- 1 E T.fi . Since <pM[1 , jr 1 can be computed in time O(n), then by iterating from T(A to T{' we have a membership test in time O(n 2 ) for the set of permutations represented by M .

Coming back to the matriochka 9(i) and the right transversals U;, we build the following n x n matrix M 9 :

From what precedes, one easily proves that Mg is a rep­ resentation matrix, and that it represents 9. Remember that M 9 depends on the order x1 ... Xn of X, and on the U; 's. It can also be proved that such a matrix can be computed in polynomial time from any generator set for 9 (see [Hoffmann, 1981]) .

4.2 Representation matrix for Sym5

We now consider the problem MG-SYM: given S, com­ pute a representation matrix for Syms . From the previ­ ous remark, such a matrix can be computed in polyno­ mial time once a generator set for Syms is available, if its length is polynomial in the length of S . Hence MG-SYM r:xp G-SYM, where G-SYM is the problem of computing such a polynomial length generator set for Syms. The graph restriction G-GA of G-SYM is well-known : it is proved in [Mathon, 1979] that G-GA r:xp GI , yielding a generator set of Aut((V, E)) of length O(IVI 3 ). Hence

Proof. Given a set of clauses S of length n , we build the graph Gs = (Vs, Es) in time O(n). G-GA yields a generator set A of Aut(Gs) oflength 0(1Vsl 3 ), hence A* has length O(n 3 ) and can be computed in time O(n 3 ) . Since · is an isomorphism from Aut(Gs) onto Syms (theorem 3.3), it is easily shown that A* is a generator set for Syms, hence G-SYM is solved in polynomial time with one call to G-GA. Q.E.D.

As a consequence, we have MG-SYM r:xp GI. In order to prove that 0-SYM and S-CSYM are isomorphism­ complete, there remains to show that 0-SYM r:xp MG­ SYM and S-CSYM r:xp MG-SYM, which will emphasize the usefulness of representation matrices.

4.3 Using the matrix

For sake of generality, we show how to compute Part(Q) for any permutation group 9 on X = { x1 ... Xn}, from a representation matrix M 9 (corresponding to the matri­ ochka 9(i)) . The algorithm is given in 4 steps; the input is X, M 9 , the output is a partition P of X .

1. initialize an x n boolean matrix B to false

1. P f- {{xl} ... {xn}}
2. Vp,q E {1 ... n}, if B[p, q], let 0,0' E P such that Xp E 0 , Xq E 0' in P +- P\{0, 0'} U {0 U 0'}

THEOREM 4.2 After step 4, P = Part(9) .

Proof. Notice that after step 2, Vp, q E { 1 .. . n}, B[p,q] {::} 3i,j E {1 ... n} such that xpM 9 [i,j] = Xq (which implies that Xp E x~).

We prove inductively that P is a refinement of Part(Q) : this is true for the initial value of P in step 3, and, in step 4, if 3x , x' E X/0 C x 9 , 0' C x' 9

(induction hypothesis), then 0 U 0' C x 9 = x' 9 since Xp E x 9 , Xq E x' 9 and B[p, q] holds.

Conversely, Part(Y) is a refinement of P: Vx E X, let 0 E P such that x E 0. Vy E x 9 , 3~ E 9/ y~ = x , and then 3!it . . . jn E {1 ... n} such that ~ = M 9 [n, jn] · . . M 9 [1, jt). Let Yn = Y and Yi-1 = y;M9[i,j;] fori= n .. . 1. Let 0; E P such that y; E 0; fori= n . . . 0. Then ViE {1 . . . n}, if y; = Xp, Yi-l = Xq then B[p, q] holds, hence 0; = Oi-l (by step 4). But Yo = x , hence On = 0 , and y E 0. We have proved that x 9 C 0. Q.E.D.

It is easily seen that the algorithm is in O(n 3 ), hence we can conclude that 0-SYM rx.p MG-SYM. We now give an algorithm for S-CSYM, in the same general set­ ting: given X and M9 as above, andY C X, it computes a 'ljJ E 9 such that Y'lj; # Y, if there is one.

1. b +-false

THEOREM 4.3 After step 2, if b then '1/J E 91\ Y'lj; ::j; Y , else V<p E 9, Y~ = Y.

Proof. The case b = true is trivial. If b = false, then Vi< j E {1 ... n}, Y M9[i,j] = Y, and we easily obtain V~ E 9, Y~ = Y . Q.E.D.

This algorithm is also in O(n 3 ), hence S-CSYM rx.p MG-SYM. As a consequence, the problems C­ SYM, S-CSYM, 0-SYM and MG-SYM are isomorphism­ complete. Remember that SYM =P GA and S-SYM =P S-GA, and of course GA rx.p S-GA rx.p Gl. In the sequel, we give some hints on solving MG-SYM as efficiently as possible, and then analyse the use ofthese different prob­ lems in automated deduction.

4.4 Algorithmic aspects

As shown previously, a representation matrix for Syms can be computed from a generator set for Aut(Gs). It is therefore possible to use known algorithms for general graphs, some of which can be found in [Hoffmann, 1981]. More precisely, [Hoffmann, 1981] contains an algorithm for generating the automorphisms of labelled graphs: i.e. graphs with labels attached to vertices, and only label­ preserving automorphisms are considered. Clearly, the labels of a labelled graph can be given as a partition of the vertices of an unlabelled graph. The orbit partition of label-preserving automorphisms is a refinement of this partition. Given any graph G = (V, E), and a partition P of V such that Part(Aut(G)) is a refinement of P (or , say, P is compatible with G) , then any a E Aut (G) is label-preserving (or, say, P-preserving), and we can therefore use the algorithm in lHoffmann, 1981] to gen­ erate Aut(G) .

A possible value for P is {V}. For Gs, we can take P = {N, Ls, S}. The interest of providing a P as fine as possible is to reduce the search space. In­ deed, the algorithm in [Hoffmann, 1981] has worst case complexity O(n 6 (k!) 6 (n + k 2 )), where n = !VI and k = max{IOI/0 E P} , producing a generator set K such that IKI :::; n 2 (k!) , which can be transformed in a representation matrix in time O(IKin 2 + n 6 ) . The num­ ber of lines of this matrix can be reduced by considering that L t is a base of Syms, hence any ordering of Ls where positive literals precede negative ones leads to a matrix where the lines corresponding to negative literals only contain I dLs, and can therefore be removed.

It should be mentioned that using labels makes it possible to simplify G s . Consider the initial partition Ps = {Ls, S} and the graph G's = (V8, E's) defined as Vs = Ls US and

Then · is an isomorphism from the group of Ps­ preserving automorphisms of �~ onto Syms (we leave this to the reader). We will therefore say that a par­ tition P' is P-compatible with G if the partition orbit of the group of P-preserving automorphisms of G is a refinement of P'.

One natural way of partitioning vertices is based on valences: since Va E Aut( G), Vv E V, valc(a(v)) = valc(v), the valences are labels, and any partition P can be refined by splitting any 0 E P into 0 1 .. . Op such that Vv E Oj, valc(v) = j, resulting in a partition P-compatible with G.

This way of combining vertex partitioning principles can be defined in a more formal way. A vertex classi­ fication into a set A is a function t mapping any graph G = (V, E) to a function tc : V -+ A. The partition of V induced by tc is {t(; 1 (a)/a E A}\{0}; if this par­ tition is compatible with G, for any graph G, then t is a v-invariant (from [Corneil and Kirkpatrick, 1980]). Hence two v-invariants t, v on A, B can be combined by defining t x v as tc x vc for any G = (V, E) and Vv E V, (tc x vc)(v) = (tc(v), vc(v)); the result is a v­ invariant into Ax B, and the corresponding partition is a refinement of both partitions for t and v .

It is also possible to build a new v-invariant from any v-invariant t into A, by counting how many adjacent vertices have the same value by tc: more formally, t 0 is defined by: Vv E V, tb(v) = .Xa E A.lt0 1 (v) n V, I, where V, is the set of vertices adjacent to v in G. t 0 is then a v­ invariant into A -+ IN. The corresponding partition may not be a refinement of the partition for t, but one can combinetXt 0 , tXt 0 Xt 00 , tXt 0 x (txt 0 ) 0 , etc. There are many other v-invariants (see [Corneil and Kirkpatrick, 1980]), related to distance information, connectivity, or number of small cycles (small cliques) through a ver­ tex (see also the star partition in [Weichsel, 1971]). It is sometimes meaningful to combine v-invariants on a graph and on its complement.

As an example, val is a v-invariant, and using vale, s (see [Read and Corneil, 1977]) corresponds to stating that two literals can only be symmetric if they appear an equal number of times in clauses of equal length, and that two clauses are in the same orbit only if they contain equal number of literals appearing in equal number of different clauses. This is a refinement of vale' . s

4.5 Symmetries in automated deduction

In this section, we will frequently refer to [Benhamou and Sais, 1994], which describes the only known imple­ mentation of Krishnamurty's rule. Although this is only a restriction of the S-symmetry rule (both on C and u), experimentations display drastic improvements on some examples.

This is not the place to describe precisely the prov­ ing methods used in [Benhamou and Sais, 1994]. First, we stress the fact that only symmetric literals are con­ sidered, which means that the S-symmetry rule is used with unit clauses . The advantage is that symmetry on literals can be easily tested once the orbit partition is known. However, the symmetry test performed in [Ben­ hamou and Sais, 1994] only corresponds to Part( <u> ), (since only one u E Syms is computed), which is are­ finement of Part(Syms); hence this test is correct but not complete. This is the second restriction of the S­ symmetry rule (on u); a useless one, as shown below.

It may be argued that computing a single non triv­ ial symmetry is simpler than computing Part(Syms ), but we show on an example that this is not relevant . Consider the famous pigeonhole problem with n pigeons (n 2: 2), it can be formalized with the following set of clauses PH n:

• fori E {1 ... n}, P;,l V ... V Pi,n-1
• fork E {1 ... n-1}, for 1 :S i < j :S n, ·P; ,kV·Pj,k

P;,j means "the pigeon i is in the hole j". It is easy to show that P Hn-symmetries correspond to permuta­ tions on pigeons and on holes (independently). Hence ISympHn I = n!(n -1)!, which shows that P Hn is highly symmetric, and is therefore a good example to illustrate the relevance of symmetry rules. Consequently, SympH n has only two orbits: the set of positive literals, and the set of negative ones .

The strategy in [Benhamou and Sais, 1994] consists in choosing a clause as long as possible and using sym­ metries inside that clause. In PH n, the longest clauses are the positive ones (if n 2:: 3). If the symmetry u ob­ tained by S-SYM is a permutation on pigeons, leaving holes unchanged, then no two literals in a positive clause are symmetric according to Part(<u>) , and there will be no application of the symmetry rule in this method (leading to an exponential proof!).

Hence one has to search for a symmetry satisfying a particular property, depending on the strategy for the symmetry rule. For example, one property required by the symmetry searching algorithm in [Benhamou and Sais, 1994] is that a cycle of the symmetry should con­ tain a given literal , and be as long as possible. It is easy to show that solving such a problem allows to solve 1R­ G A (by graph restriction) , and is therefore at least as difficult as G I (moreover, restrictions on u easily lead to NP-complete problems, see [Lubiw, 1981]) . Hence the problem of maximizing the length of a cycle is at least as difficult as 0-SYM, but yields only a refinement of Part(Syms). It should be mentioned that the algorithm in [Benhamou and Sais, 1994] uses a technique for reduc­ ing the search space which corresponds to the v-invariant vale' . But the reason of its apparent efficiency is that s it is allowed to backtrack only a fixed amount of time; it therefore has a polynomial time complexity (see [Read and Corneil , 1977]) , and hence cannot be expected to solve S-SYM.

0-SYM is only one example of relevant problems for implementing symmetry rules , that is solvable in poly­ nomial time from a representation matrix M for Syms. There is also S-CSYM, and others may exist. Hence rep­ resentation matrices are not only useful for proving com­ plexity results, as done above, but also for implementing extensions of resolution with the symmetry rule. Other symmetric resolution methods, less restricted than the one in [Benhamou and Sais, 1994], may be designed, and probably may involve problems which can efficiently be solved if the representation matrix is available, hence making good use of the nice group structure of Syms.