Some minor fixes to the unfinished Pearl solver:

[sgt/puzzles] / unfinished / group.c

diff --git a/unfinished/group.c b/unfinished/group.c
index d2ff194..c82c40a 100644 (file)
--- a/unfinished/group.c
+++ b/unfinished/group.c
@@ -242,6 +242,17 @@ static char *validate_params(game_params *params, int full)
         */
        return "Trivial puzzles must have an identity";
     }
+    if (!params->id && params->w == 3) {
+       /*
+        * We can't have a 3x3 puzzle without an identity either,
+        * because 3x3 puzzles can't ever be harder than Trivial
+        * (there are no 3x3 latin squares which aren't also valid
+        * group tables, so enabling group-based deductions doesn't
+        * rule out any possible solutions) and - as above - Trivial
+        * puzzles can't not have an identity.
+        */
+       return "3x3 puzzles must have an identity";
+    }
     return NULL;
 }
 
@@ -602,7 +613,6 @@ done
      * _out_, so as to detect exceptions that should be removed as
      * well as those which should be added.
      */
-#if 0
     if (w < 5 && diff == DIFF_UNREASONABLE)
        diff--;
     if ((w < 5 || ((w == 6 || w == 8) && params->id)) && diff == DIFF_EXTREME)
@@ -611,7 +621,6 @@ done
        diff--;
     if ((w < 4 || (w == 4 && params->id)) && diff == DIFF_NORMAL)
        diff--;
-#endif
 
     grid = snewn(a, digit);
     soln = snewn(a, digit);
@@ -1047,6 +1056,34 @@ static int check_errors(game_state *state, long *errors)
     digit *grid = state->grid;
     int i, j, k, x, y, errs = FALSE;
 
+    /*
+     * To verify that we have a valid group table, it suffices to
+     * test latin-square-hood and associativity only. All the other
+     * group axioms follow from those two.
+     *
+     * Proof:
+     *
+     * Associativity is given; closure is obvious from latin-
+     * square-hood. We need to show that an identity exists and that
+     * every element has an inverse.
+     *
+     * Identity: take any element a. There will be some element e
+     * such that ea=a (in a latin square, every element occurs in
+     * every row and column, so a must occur somewhere in the a
+     * column, say on row e). For any other element b, there must
+     * exist x such that ax=b (same argument from latin-square-hood
+     * again), and then associativity gives us eb = e(ax) = (ea)x =
+     * ax = b. Hence eb=b for all b, i.e. e is a left-identity. A
+     * similar argument tells us that there must be some f which is
+     * a right-identity, and then we show they are the same element
+     * by observing that ef must simultaneously equal e and equal f.
+     *
+     * Inverses: given any a, by the latin-square argument again,
+     * there must exist p and q such that pa=e and aq=e (i.e. left-
+     * and right-inverses). We can show these are equal by
+     * associativity: p = pe = p(aq) = (pa)q = eq = q. []
+     */
+
     if (errors)
        for (i = 0; i < a; i++)
            errors[i] = 0;