-When one goes from a geometrical statement to an algebraic statement, the immediate translation is to replace every point by a pair of coordinates, if in the plane (or more as required). A statement with N points is then a statement with 2N (or 3N or more) variables, and the complexity of tools like cylindrical algebraic decomposition is doubly exponential in the number of variables. Hence one says “without loss of generality, A is at (0,0)” and so on. How might one automate this, or turn it into a procedure (and possibly even a formal proof)? Copyright c by the paper's authors. Copying permitted for private and academic purposes. In: E. Abraham, J. Davenport, P. Fontaine, (eds.): Proceedings of the 1st Workshop on Satis ability Checking and Symbolic Computation (SC2), Timisoara, Romania, 02-07-2016, published at http://ceur-ws.org
Symmetry is at once a familiar concept (we recognize it when we see it!) and a profoundly deep mathematical subject. At its most basic, a symmetry is some transformation of an object that leaves the object (or some aspect of the object) unchanged. [Sak09] That quotation comes from a major survey of symmetry in purely Boolean satisfiability problems, but our setting is “Satisfiability Modulo Theories” over the real numbers, and the desire to enhance this with techniques from Computer Algebra, notably Cylindrical Algebraic Decomposition. See [A´ 15], [ABB+16]. Here the situation is different in two, complementary, respects.
1) It is not legitimate to discard a part of the Boolean search space on the grounds that it is symmetric to another, already searched, space, unless we know that this symmetry carries through to the underlying theory. 2) Conversely, symmetries in the underlying theory may exist, which either do not appear directly in the Boolean formulation, or indeed are irrelevant to the Boolean formulation, but may greatly simplify the underlying theory. More specifically, it is the second kind of symmetry that this paper is concerned with.
Many proofs, particularly of the more computational kind, in mathematics contain a line of the form “without loss of generality, we may assume . . . ” (often abbreviated w.l.o.g). This is discussed in [Har09], who claims, we believe correctly, that this means one of two, rather different, things: A: non-degeneracy: for example “w.l.o.g. 6= 0”, really means1 “ = 0 is a special case, which you can easily see for yourself, so I am not going to bother with it here”; 1However, it may also mean C: “ = 0 renders the result meaningless, so we shall not consider it further”.
B: exploitation of symmetry: as in [Har09]’s opening example of Schur’s inequality 8a; b; c 2 R; k 2 N, 0 ak(a b)(a c) + bk(b a)(b c) + ck(c a)(c b); (1) where a typical proof might begin: “Without loss of generality, let a b c”.
This paper is essentially concerned with the second case, though, as we shall see, it is not possible to ignore the first, and indeed a given statement might combine both in practice.
This is a very powerful form of human reasoning. [Har09] asks, and substantially answers, the question of how it can be incorporated into formal proof: here we ask the same question for computation, notably in the context of Symboic Computation and Satisfiability Checking [ABB+16].
II. EXPLOITATION OF SYMMETRY — DISCRETE [Har09] explains the example above as follows.
If asked to spell this out in more detail, we might say something like: Since is a total order, the three numbers must be ordered somehow, i.e. we must have (at least) one of a b c, a c b, b a c, b c a, c a b or c b a. But the theorem is completely symmetric between a, b and c, so each of these cases is just a version of the other with a change of variables, and we may as well just consider one of them.
He then offers two possible formalisms:
The phrase may be an informal shorthand saying ‘we should really do 6 very similar proofs here, but if we do one, all the others are exactly analogous and can be left to the reader’.
The phrase may be asserting that ‘by a general logical principle, the apparently more general case and the special WLOG case are in fact equivalent (or at least the special case implies the general one)’.
He then argues that the second interpretation is closer to the informal mathematics, and shows how to implement this as a HOL-Light theorem, more precisely ` (8xyz:P xyz ) P yxz ^ P xzy)^ (8xyz:x <= y ^ y <= z ) P xyz)
) (8xyz:P xyz)
Note 1: There’s a subtlety here: in fact the statement is invariant under S3, the symmetric group on fx; y; zg, but the (2) c < 0 c = 0 c > 0 b < c b = c b < 0 b = 0 b < 0 b = 0 0 < b < c b = c
all a < c; a = c a < b; a = b a < 0; a = 0
all a < c
all a < 0; a = 0; 0 < a < c; a = c two permutations listed, xyz ! yxz and xyz ! xzy (in cycle notation (x; y) and (y; z)), generate S3.
Unfortunately (1) is not polynomial: we need to specialise k. If we feed (1)jk=2 into Cylindrical Algebraic Decomposition (the [CM14] implementation), we get 31 cells (as we do for any even k: odd k give us 59 cells, but the conclusions are similar): the major split is on how c compares with 0: c < 0 then splits on how b compares with c and 0 (five possibilities, with b = c splitting a into five possibilities, and b = 0 splitting on how a compares with c); c > 0 similarly, and c = 0 having a three-way split on b, each having a three-way split on a. Of these, the 14 listed in Table I satisfy a b c, either totally, or, where underlined, only partially. Not only is this ratio of 14=31 45% disappointing compared with the na¨ıve (not allowing for equality) 1/6 one might expect: if we split the underlined cells to get precisely the cells with a b c, the ratio would be 18=39 46%.
The most obvious generalisation of Note 1 is the following well-known result.
Proposition 1: The permutations (1; 2; : : : ; n) and (1; 2) generate Sn as a group acting on f1; 2; : : : ; ng.
Corollary 1: Hence, if a statement P (x1; x2; : : : ; xn) is given, and P (x1; x2; : : : ; xn) is logically equivalent to P (x2; x1; : : : ; xn) and to P (x2; : : : ; xn; x1), it is sufficient to prove
P (x1; x2; : : : ; xn) ^ x1 x2 ^ x2 x3 ^ : (3)
Note 2: We have said “logically equivalent to”, rather than just “equal to”, as we needed the laws of algebra (at least commutativity of addition and multiplication) to show that (1) was actually invariant.
III. EXPLOITATION OF SYMMETRY — CONTINUOUS One of the most important ways in which such invariances are used in proofs is to make a convenient choice of coordinate system. [Har09] If a problmis intrinsically geometric, then the precise coordinate system is irrelevant to the truth of the statement. It is this sort of symmetry that we will look for in this section.
Let us consider the following example yD 1 4D2
1 4D2 0 xD2 + yD2 =
yD xA2 (xB yD xA2yB 0 1 2
Theorem 1 (Simson’s Theorem, [Wan96], [Mou16]): Let D be on the circumcircle of the triangle ABC, let P , Q and R be the points of AB, AC and BC where the line to D is perpendicular. Then P , Q and R are collinear.
Let us consider just the first statement “Let D be on the circumcircle of the triangle ABC”. One possible coordinatisation2 of this is (4). xB yA + xB yC + xC yA (4) It is relatively easy (for a computer algebra system) to verify that (4) is invariant if we replace all variables z by z + c. Hence it is legitimate to choose yA = 0, which gives us (5). 2Obtained with Maple’s geometry[circumcircle] command.
Again, it is relatively easy (for a computer algebra system) to verify that (5) is invariant if we replace all variables z 2 fxA; xB; xC ; xDg by z + c. Hence it is legitimate to choose xA = 0, which gives us (6). (6) In fact, both [Wan96], [Mou16] coordinatise with A = (xA; 0) and B = ( xA; 0), taking (implicit) advantage of the fact that the problem is invariant under translation (so we can place the midpoint of AB at (0; 0)) and rotation (so we can place A and B on the x-axis). Then (4) becomes the simpler (7). One further step, which [Wan96], [Mou16] could have done, and a computer system could certainly spot, is that the equation is homogeneous, and hence we can pick, say, xA = 1. However, whilst appearing to be a type B w.l.o.g., exploiting symmetry under dilation, it is also asserting xA 6= 0, thus a type A, or even type C, w.l.o.g. as well.
The non-vanishing of the denominators in (4)–(7) essentially corresponds to the non-degeneracy of the triangle ABC, so it is legitimate to consider just the numerators. The resource consumptions of Cylindrical Algebraic Decomposition, computing a complete CAD of Rn on these are shown in Table II.
Let us consider first the [CM14] timings. These show, somewhat to the author’s surprise, that Cylindrical Algebraic Decomposition is, at least in this example, unaffected in terms of cell count by the translation w.l.o.g.s, though rotation ((7) rather than (6)) and scaling (the substitution lines) help, at least in terms of cell count.
We solved (6) with variable ordering x y xC yB yC (i.e. yC is the first variable to be eliminated). The different scalings were applied to (6) after (6)jxB=1 showed quite large denominators, e.g. cell (1,1,1,2,1) has 23079170135623 < yB < 74412904732054 , and hence the author hoped that rescaling would reduce this problem. The effect is in fact negligeable: in (6)jxB=16 the same cell has 133013007923 < yC < 21402448754736 , and in (6)jxB=256 we have 217054084517067 < yC < 13572542208583 . As can be seen, the overall effect on memory and time of changing the scaling was for the worse.
The second set of timings were produced using the software in [EWBD14], but with no special declarations, hence effectively the projection of [McC84]. In several cases, this warned that the projection was not well-oriented. Since the McCallum projection is a superset of the Lazard projection, and this has been recently [MPP16] been proved unconditionally correct, we can ignore these. We observe that detecting the rotational symmetry ((7) rather than (6)) had a much greater effect here than it did for the [CM14] method.
The really surprising effect was the difference between (6)) and (5)). As far as the author could tell, the code was still projecting when interrupted after 2 21 hours: at least is had produced no warnings about orientation. This needs further investigation.
The question of detection comes in several forms. 1D Invariance by translation by R can be detected, as we did in going from (4) to (5), by checking that adding c to all variables leaves the equation (or system of equations) invariant. This will fail, of course, if there are variables other than the results of coordinatisation. 2D Having detected invariance by translation by R, we can look for invariance by translation by R2 as we did in going from (5) to (6), by checking that adding c to a proper subset of the variables leaves the equation (or system of equations) invariant. Of course, the author “cheated” and translated all the x variables based on variable name, but in practice one would have to try all subsets (but not a subset and its complement) of the set of variables. 3+D Though not present in our example, we could then go on to detect invariance by translation by R3, and so on. As we see in the discussion of rotation, it is important to do so.
Scaling This is a consequence of homogeneity, and can easily be detected. The problem is that this is also a type A (or even C) w.l.o.g. as well as type B one, and, having chosen xi as our dehonogenising variable, we ought in principle to consider the two cases xi = 1 and xi = 0. The second case, if it does not collapse, is also homogeneous in the remaining variables, so we can recurse. 2D Rot. If we know that we have 2D translation symmetry, we might hope for 2D rotational symmetry as well. Let us call the set of variables translated by c in the search for 2D symmetry the “x” variables, and its complement the set of “y” variables, and assume that there are no more “x” variables than “y” variables, which will occur if we do a breadthfirst search for such a set. If the problem comes from coordinatisation of a 2D geometrical problem, there should be as many “x” as “y” variables — of couse whether these correspond to the original x and y or vice versa is a matter of chance, but from now on we shall drop the quotes, implicitly assuming the correspondence, not that it matters.
Then the question comes: which yj 2 fy1; : : : ; ymg corresponds to which xi 2 fx1; : : : ; xng? Here we know of no better answer than trying all m!=(m n)! possibilities for a complete assignment . We then replace all pairs (xi; y (i)) by (cxi sy (i); cy (i) + sxi) to practice a rotation3 by with c = cos , s = sin , and apply c2 + s2 = 1. For the correct assignment in our example, it is relatively easy to demonstrate equality (in particular the result is independent of c and s), and for incorrect examples we get results that still contain c and s. 3D Rot. We have no examples of this, but the principles are the same as above. Note that, if there really is 3D symmetry, we should identify it, and then choose triples (xi; y (i); z (i)), as assuming we have merely 2D symetry, and rotating the x and y but not the z, will fail.
We have only considered one example so far, but intend to study others. It is a “natural” example in that it comes from 2D geometry. It would be possible to build artificial examples that had, for example, rotational symmetry but no translational symmetry, but, in the spirit of [ABB+16], we have started with natural problems. From the basis of this limited analysis, we draw the following provisional conclusions.
It is possible to detect certain forms of symmetry simply from the equations (though it would clearly be better to detect them before coordinatisation if at all possible). For the method of [CM14], detecting translational symmetry has no effect on the cell count (and a modest effect on runtime and memory), but seems to be a pre-requisite to efficient detection of rotational symmetry, which is extremely helpful. The method of [McC84] seems much more susceptible to the number of variables, and hence all symmetry detection and “w.l.o.g.” specialisation are helpful.
Acknowledgements. The author is grateful to Julien Narboux for references, and to Matthew England and the referees and Programme Committee of the SC22016 workshop for useful comments. This work was performed as part of the H2020-FETOPEN-2016-2017-CSA project SC2(712689). The dataset supporting these computations is stored at http://doi. org/10.5281/zenodo.305441.
3The reader may object that this is a rotation about the origin. But we have already demonstrated 2D translational invariance, so one centre is as good as another.