This is an investigation in the tradition of Fujita et al (IJCAI 1993), Zhang et al (JSC 1996), Dubois and Dequen (CP 2001) in which CP or SAT techniques are used to answer existence questions concerning small algebras. In this paper, we open the attack on IP loops, an interesting and underinvestigated variety intermediate between loops and groups.
1.1
A quasigroup is a groupoid with left and right division operators = and n. That is, it satisfies the laws: In the finite case, this amounts simply to satisfying the left and right cancellation laws: That is, its “multiplication table” is a Latin square, each row and each column being a permutation of the elements. A quasigroup is a loop iff it has a (right and left) identity: an element e such that for all x. Loops in general are so numerous that almost all work on them has concerned special cases. One of the earliest classes of loops to be investigated was that of Steiner loops, which satisfy the additional postulates Clearly, in any loop, each element x has a left inverse—an element y such that yx = e—and a right inverse xx 1 = e = x 1x x 1(xy) = y = (yx)x 1 x(z(yz)) = ((xz)y)z Note that (x 1) 1 = x.
A loop is said to have the inverse property, and is called an IP loop, iff it is a loop with inverse such that for all elements x and y It is not hard to see that IP loops also satisfy the principle (xy) 1 = y 1x 1. A Steiner loop is an IP loop of exponent 2 (i.e. such that x2 = e for all x) and a group is simply an associative IP loop. Moufang loops, which have been studied intensively, are IP loops satisfying the identity IP loops are of interest as a strong and natural generalisation of both groups and Steiner loops. Moreover, they correspond exactly to semiassociative relation algebras [Mad82] in the same sense that groups correspond to (associative) relation algebras.1 It is therefore a little surprising that they have attracted comparatively slight attention from algebraists.
The smallest IP loop that is not a group is of order 7: This structure has proper subalgebras f1; 2; 3g, f1; 4; 5g and f1; 6; 7g. Note that the order of these subloops does not divide the order of the loop, marking a significant difference between IP loops and groups.2 Associativity fails in that, for instance, (2 2) 4 = 3 4 = 7 while 2 (2 4) = 2 6 = 5. 2
It is frequently useful to enumerate small examples of a class of algebraic structures, so that by examining what exists, and observing places where no such structures exist, the mathematician can gain a “feel” for the objects in question. At the simplest, the spectrum (the set of numbers n for which such algebras of order n exist) can have its initial segment settled by enumeration. In some cases, this suffices to allow the entire spectrum to be determined; in others, it merely dispposes of some awkward questions and suggests a conjecture concerning the rest. In many cases, “off the shelf” reasoning systems suffice for the enumeration, making this an attractive application domain for automated reasoning. 1Let G = hS; i be a groupoid. The field of sets consisting of the power set of L, with raised to sets in the obvious pointwise manner, is a relation algebra iff G is a group, and a semiassociative relation algebra iff G is an IP loop. 2A loop in which the order of every subloop divides the order of the loop is said to have the weak Lagrange property. It has the strong Lagrange property if every subloop has the weak property. solve satisfy; int N; type element = 1..N; array[element,element] of var element: star; constraint
forall (x,y in element) (star[star[star[y,x],y],y] = x);
N = 3; 2.1
Fujita et al [FSB93] used the ICOT group’s ‘Model Generation Theorem Prover’, a propositional reasoner in the style of SATCHMO [MB88], and other tools including FINDER to solve open problems in the theory of quasigroups by proving the existence or nonexistence of quasigroup models of certain equations. During the 1990s, this work was taken up and extended, notably by Hantao Zhang and his collaborators through the SATO system [ZBH96] and by McCune, Stickel and others [McC, ZS00]. In the constraint programming community, there were interesting developments concerning efficient encodings [DD01] and in the SAT community concerning symmetry avoidance [Zha96, AH01]. Recently, it has been shown [APSS05] that preprocessing of SAT encodings using restricted variants of resolution can simplify some of the quasigroup existence problems to the point that stochastic local search (SLS) solvers can successfully prove existence (though not nonexistence, of course). Meanwhile, the related problem of quasigroup completion [GS97] has become a well-established benchmark constraint satisfaction problem, offering as it does a nice balance between the highly structured and the random. Benchmark collections of SAT, CSP and SMT problems now routinely contain problems about quasigroups. 2.2
The simplest way to represent existence problems about quasigroups, loops, groups or other groupoids for automated reasoning purposes is to cast them as finite domain CSPs where each entry hx; yi in the “multiplication table” of the groupoid is a CSP variable whose domain consists of the elements of the algebra. Take for example the problem QG5(3). This requires the matrix to be filled with nine entries chosen from the values 1 : : : 3, in such a way that they form a Latin square and that the equation (yx:y)y = x holds for all x and y. In fact, if they satisfy the equation, the cancellation properties follow. In the CSP modelling language Zinc [dlBMRW06] for instance, this is directly expressible (see Figure 1). Other such languages for constraint programming make it similarly easy to state the problem.
The equation flattens to 8x8y8w8z((yx = w ^ wy = z) ) zy = x) which has 4 variables and therefore 34 = 81 domain-grounded instances obtained by substituting the three possible values 1, 2, 3 for the variables. Each of those instances relates a triple (possibly with repetition) of entries in the table, and correspondingly imposes a constraint of cardinality at most 3 on the variables of the CSP. In the straightforward SAT recension, each possible value assignment a b = c is represented by a propositional variable pabc, and each domain-grounded instance of the flattened equation becomes a 3-clause on these variables. Other encodings are possible, of course, but the suggested one is standard. Once the problem is so encoded, any FD or SAT solver can be used to solve it. Theorem provers, whether based on resolution and its variants or on term rewriting, can also be used to make inferences on either the first order or propositional levels.
To generate IP loops, we need another array of decision variables representing the inverse function, and of course the appropriate equations. It is useful to add a few redundant constraints, to strengthen propagation. We added the fact that inverse is of period 2 and the duality equation (xy) 1 = y 1x 1. Since we wish to enumerate isomorphism classes, it is important to avoid generating too many isomorphic copies of the solutions, which means we need to break symmetries. In order to break some of the many symmetries in a simple way, we required the identity e to be the lowest-valued element and x 1 to be in the range x 1 : : : x + 1, with self-inverse elements coming first in the order. 2.3
For our work, we used FINDER, which stands somewhere between the FD and SAT solver families. It represents the problem in the FD manner rather than explicitly rendering it into SAT, so for example its variable selection heuristic looks at the FD variables, not at specific values for them—typically it looks for the smallest available domain—but it reasons somewhat like a SAT solver rather than in typical FD style. In particular, it uses unit resolution on the ground constraints together with forward-checking as its notion of local consistency, and it learns nogoods.
FINDER is far from representing the state of the art in finite model building: we expect that similar results could be produced faster using more recent technology such as Paradox, which is based on the much more efficient SAT solver Minisat. It suffices for our purpose, however, as it can find the solutions faster than they can be checked for isomorphism and has completed the order 13 search in reasonable time.
To count the isomorphism classes, it is necessary either to reason in a sophisticated way about symmetries during the search3 or to remove redundant solutions from the output in a postprocessing phase. We chose the latter: our postprocessor takes each generated IP loop in turn and tries to generate from it an isomorphic copy that comes earlier in the (row-major) lexicographic order. If it succeeds, the generated loop is discarded; if it fails, the loop in question is the canonical one of its class and is output. This isomorphism removal method is rather slow, but requires little memory. Indicated future research includes incorporating isomorphism detection into the search.
Generating the IP loops of orders up to 11 is easy. We confirmed our results by obtaining the same numbers with MACE [McC]. Order 12 caused more difficulties, taking unreasonably long for both FINDER and MACE with their default settings. With a small change to make FINDER more aggressive about deleting old nogoods, however, we were able to solve the order 12 problem in a matter of hours.
Order 13 was more challenging. Our first partially successful run took over a week without exhausting the search space. On closer examination, we found that almost all of this time was taken up by the postprocessor eliminating isomorphic copies. We therefore somewhat strengthened the symmetrybreaking constraints, in order to reduce the number of copies to be treated, and rewrote the postprocessor to search less na¨ıvely for dominating copies. The result is that the order 13 problem can now be completed in less than a day on a fairly ordinary desktop machine. 3The GAP-ECLiPSe hybrid of Gent et al [GHKL03] does this, and, given a suitably efficient underlying solver, may be the preferred method if the present investigations are to be pressed beyond order 13.
Basic size time (sec) solutions 7 0.00 10 8 0.03 128 9 0.11 488 10 2.51 8856 11 39.30 128488 12 3026.31 8956032
The most signficant part of the speedup was that due to the extra symmetry breaking constraints added by hand to the encoding. These reduced the domains of possible values for the cells in the second row of the table of the loop operation—the first row is fixed as it lists the elements of the form e x, which of course is x in every case. The canonical representative of each isomorphism class is first in the lexicographic order in which this second row is most significant, so clearly we lose nothing by constraining the numbers early in the row to be as low as possible. Since e is the first (lowest-numbered) element, we can conveniently represent all elements as (e + x) where x is an integer in the range 0 : : : N 1.4 We are concerned to add constraints limiting the values of elements of the form (e + 1) (e + x) where 0 < x < N.
Where N is odd, this is simple. There are no fixed points for the inverse operation, so (e + 1) 1 = (e + 2), so there are two possibilities for the value of (e + 1) (e + 1): it could be (e + 2) or it could be something else, where “something else” might as well be (e + 3) since all choices are symmetric. By similar reasoning, for x > 1, the canonical member of each isomorphism class has (e + 1) (e + x) < (e + 2x).
Where N is even, there is an additional complication. It is possible that some elements other than e are fixed points for inverse, and it can happen that for all of these fixed points a, the element (e + 1) a is not a fixed point. In that case, the usual upper bound does not apply, but instead the values of such (e + 1) a can be assigned arbitrarily. We choose to assign them in ascending order. We introduce a boolean flag (another decision variable) which will be set just in case the first 6 elements are all fixed points for inverse and (e + 1) (e + 2) is not a fixed point. Provided the flag is not set, a constraint similar to that for odd values of N applies. That is, using f(j) to abbreviate (e + 1) (e + j): Basic symmetry breakers: e x x 1 < (x + 2) (x 1 = x ^ y < x) ) y 1 = y For odd values of N: x 1 < x + 2 x 1 = x , x = e f(1) < (e + 4) (x > 1 ^ 2x < N) ) f(x) < (e + 2x) 4Naturally, we could let the elements be the integers 0 : : : N 1 or 1 : : : N, as in the Zinc encoding suggested in Figure 1, in which case the notation would be simplified. FINDER, however, is picky about types and complains if we confuse “element” with “int”, so we keep the long-winded version for present purposes. size quasigroups 1 1 2 1 3 5 4 35 5 1411 6 1130531 7 1:21 1010 8 2:70 1015 9 1:52 1022 10 2:75 1030 11 — ? — 12 — ? — 13 — ? — loops f(1) = e (:FLAG ^ 0 < x < N=2) ) f(x) < (e + 2x + 1) FLAG ) (e + 5) 1 = (e + 5) (FLAG ^ x > 1 ^ (e + x) 1 = (e + x)) ) (f(x)) 1 6= f(x) (FLAG ^ 1 < x < y ^ (e + y) 1 = (e + y)) ) f(x) < f(y) The enhanced symmetry breaking pays handsomely, as shown in Figure 2 where the runtimes and numbers of solutions (before postprocessing) with and without the extra symmetry breakers are compared. It is worth noting that in generating 626,888 solutions to the order 12 problem, for example, FINDER backtracks only 202,549 times. That means that three quarters of the branches in the search tree end in solutions, so it is unlikely that significant improvement to the efficiency of the search is possible. Any future advance will need to involve better symmetry removal, to cut down still further the number of solutions generated. 2.4
5The numbers of quasigroups and loops are taken from the paper of McKay et al [MMM07] which also contains an account of the many errors making up the history of counting these objects. to observe that the smallest such loop which is not a group is of order 10. It seems that commutativity tends to enforce associativity, at least at small sizes: only one of the 48 non-associative IP loops of order 11, for instance, is commutative. 3
In abstract algebra, the effect of generating the structures of small sizes is often to provide a supply of data rather than a supply of theorems. This means that model searches function more like experiments in an empirical science than like proof searches in mathematics as standardly conceived. The roˆle of diagrams in traditional geometry is somewhat similar: a diagram is not a proof, but it can supply a disproof, and inspection of diagrams can suggest conjectures to the mathematician with an eye for regularities. In the same way, identifying patterns in the numbers or distribution of small structures is a good way of formulating conjectures in abstract algebra.
In the present case, we have been able to use the “data” provided by FINDER to arrive at several new results concerning IP loops. These are not necessarily very deep mathematics, and their proofs, once the regularities have been observed, are not especially hard. The trick is to formulate the conjecture in the first place, and for this purpose access to the quasi-empirical data is invaluable. 3.1
Steiner loops satisfy the condition 8x(x2 = e) or equivalently 8x(x 1 = x). We wondered whether there was anything to say about the distribution of elements satisfying the self-inverse condition in IP loops which are not Steiner loops in general. Fortunately, in generating the algebras, as explained in x2 above, part of our technique was to set the inverse operation before generating the loop operation. Thus we were presented immediately with the numbers of IP loops of each order with each possible choice of inverse, where the difference between two inverse operations is just in the number of self-inverse elements. Hence our generation method itself resulted in a study of the distribution of self-inverse elements among IP loops of each size. To our initial surprise, there appeared to be no such elements at all (other than the identity) in IP loops of odd order. We knew, of course, that Steiner loops are always of even order, but expected that IP loops of any cardinality would typically contain at least some fixed points for inverse.
They do not, however, as can be shown by a simple counting argument: Theorem 1. Let L = hS; i be a finite IP loop. Then the cardinality of S is even iff L has an element of order 2—that is, an element a such that a 6= e but a2 = e.
Proof. Left to right, the result is trivial: since the inverse operation is of period 2, the set of elements of L which are not fixed points for it must be of even cardinality. If the order of L is even, therefore, there must also be an even number of self-inverse elements, so e cannot be the only such element.
For the converse, suppose a is self-inverse and distinct from e. Let the operation La be defined on S by the equation La(x) = a x. Then La is of period 2, as La(La(x)) = a (a x) = a 1 (a x) = x. Moreover, La has no fixed point, as if La(x) = x then a x = x so a = e contrary to the supposition of the theorem. Therefore La partitions S into pairs, so jSj is even.
Corollary 2. No IP loop of odd order has a subloop of even order. 3.2
Following on from this theorem, we examined the spectra of the equations xk = e for small values of k. The observations up to order 13 are summarised in Table 3.6
The spectrum of Steiner loops (the column k = 2 in the table) is well known to consist of 1 and all integers congruent to 2 or 4 (mod 6). The argument that all Steiner loops fall into that spectrum is nice enough to be worth rehearsing here. First note that Steiner loops are commutative, because for any elements x and y, (x:xy)(yx) = y(yx) = x = (x:xy)(xy) so xy = yx. Next, if xy = z then xz = x(xy) = y, so such loops are “fully commutative” in that for any triple x, y and z, the six equations obtained by permuting the variables in “xy = z” are all equivalent. Steiner loops thus correspond directly to Steiner triple systems, or sets of triples of elements from a set such that every pair of elements from the set occurs in exactly one triple. The identity of the loop is added to allow for the case where x and y are the same. Evidently, there are three pairs in every triple, so the number of triples in a Steiner triple system is one 6As usual, we assume association to the left, defining x0 = e and xk+1 = xk x. third of the number of pairs of elements in the set. Thus, where the set has n elements, n2 n must be divisible by 6. Expressing n as 6k + i for some i in 0::5, we see immediately that i2 i must be divisible by 6, requiring i to be either 0, 1, 3 or 4. Hence n + 1, the order of the Steiner loop, must be congruent to 1, 2, 4 or 5 (mod 6). But odd orders greater than 1 are impossible by Theorem 1, so except for the degenerate case n = 1 the order of the loop must be congruent to 2 or 4 (mod 6).
The core of this argument, divisibility by 6, can be generalised.
Theorem 3. Let L be an IP loop of order 3n. Then L contains an element x distinct from e such that x2 = x 1.
Proof. Consider any elements a, b and c, all distinct from e, such that ab = c in L. Then the following all hold: ab = c cb 1 = a a 1c = b b 1a 1 = c 1 bc 1 = a 1 c 1a = b 1 Moreover, the six table entries represented by these equations are all distinct unless one of them is of the form xx = x 1. If L contains no such x, therefore, the table entries not involving e are partitioned into blocks of 6. There are (3n 1)2 (3n 1) such entries, so (3n 1)2 (3n 1) is a multiple of 6. That is, 9n2 9n + 2 is a multiple of 6. Let 3n = 6k + i where 0 i < 6. Then 9(6k + i)2 9(6k + i) + 2 is divisible by 6, so 9(36k + 12ki + i2) 56k 9i + 2 is divisible by 6, so 9(i2 i) + 2 is divisible by 6. But it is not.
Theorem 4. Let L be an IP loop of exponent 5. Let n be the order of L. Then either n n 5 (mod 12). 1 (mod 12) or Proof. For any element x of L, x4 = x 1 and it is not hard to show that x3 = (x2) 1. It is left as a satisfying exercise to show that for all x, i and j, xi x j = xi+ j (mod 5). It follows that L is composed of a number of subloops of order 5, each of course of the form fe; x; x2; x3; x4g. That is, they are disjoint except for e. Therefore n 1 (mod 4).
Clearly, L contains no element x distinct from e such that x2 = x 1, so by Theorem 3 its order is not a multiple of 3 and therefore n 6 9 (mod 12).
Theorem 5. Let L be an IP loop of exponent 3. Let n be the order of L. Then either n n 3 (mod 6). 1 (mod 6) or Proof. For every element x of L, x3 = e or equivalently x2 = x 1. It follows that n is odd, and also that Theorem 3 is not directly useful. We can adapt the argument, however. If we ignore the first row and column of the table, we are left with (n 1)2 entries. Each row contains two “anomalous” entries: e in the x 1 column and x 1 on the diagonal. Removing those two entries from each row, that leaves (n 1)2 2(n 1) to be filled with blocks of 6 as before. Thus (n 1)2 2(n 1) is divisible by 6. Expressing n as 6k + i, we find that i2 4i + 3 is divisible by 6, which is to say i = 1 or i = 3. 3.3
A groupoid has the square property iff (xy)2 = x2y2 for all x and y. It is well known that a group is commutative iff it has the square property. This is not true of IP loops, however. The smallest counterexample is of order 10: This IP loop is commutative, but lacks the square property as (3 5)2 = 4 but 32 52 = 2. The converse is also not valid for IP loops: there are 3 non-commutative IP loops of order 12 with the square property, and 2 more of order 13.
Another property which suffices for a group to be abelian is that it is of order p2 where p is a prime. IP loops of such orders are not in general commutative, as for example there are 5 non-commutative ones of order 9. However, both commutative IP loops of order 9 are groups, leading us to wonder whether all commutative IP loops of order p2 are groups. The answer is negative: there is a commutative non-associative IP loop of order 11, so its direct product with any IP loop also of order 11 is a noncommutative IP loop of order 121 which is not a group. 3.4
A loop is said to be flexible iff it satisfies and alternative iff x(yx) = (xy)x x(xy) = (xx)y (xy)y = (xy)y Steiner loops and groups are flexible and alternative. It turns out that the smallest IP loop which is flexible and alternative but neither a group nor a Steiner loop is of order 12, and there are, up to isomorphism, only two such loops of order 12 and none of order 13.
Steiner loops and groups are also C-loops, meaning they satisfy
x(y(yz)) = ((xy)y)z All C-loops are known to be IP loops and alternative. Up to order 13, there is only one non-associative, non-Steiner C-loop. Again it is of order 12. 4
This paper has added to the store of known “small” examples of core algebraic structures. IP loops inhabit the space between very tightly constrained varieties (groups, Steiner loops) and very loose ones (quasigroups). They are closely related to an interesting generalisation of relation algebras. We have detailed the IP loops up to the orders at which the number becomes too big for a mathematician to know them all. The most obvious extensions of our work are: 1. Complete the account of the spectrum of IP loops of exponent k, for all k. We have the impression that it is not very difficult, but settling this issue properly would be satisfying. 2. Extend the investigation to particular classes of IP loops. For example, enumerate the small Cloops. Since these are comparatively rare, it will be necessary to go to larger sizes before enumeration ceases to be worthwhile. Phillips and Vojteˇchovsky´ [PV06] report very small numbers of C-loops up to order 14, for which they used MACE-4. It is possible that significantly extending the search may raise different challenges for automated reasoning. 3. Investigate the use of GAP-ECLiPSe or a similar hybrid which brings computational group theory to bear on the problem of symmetries in search spaces. Since this detects many symmetries and avoids them early, it is potentially an important tool for getting further with the enumeration of IP loops or species of them. 4. Experiment with more systematic symmetry breakers such as the “least number” heuristic of Jian Zhang and its extensions. Dealing with symmetry, rather than with search inefficiency, is the main bottleneck in the algebra generation process at present. 5. Pick out some new benchmark problems from our work, for finite domain constraint solvers, for
SAT solvers or for SMT systems.7 [McC] [MMM07] [PV06] [SA07] [Sla94] [ZBH96] [Zha96] [ZS00]