Group: hard-mode identity deduction.

This fills in the deduction feature I mentioned in commit 7acc554805,
of determining the identity by elimination, having ruled out all other
candidates.

In fact, it goes further: as soon as we know that an element can't be
the group identity, we rule out every possible entry in its row and
column which would involve it acting as a left- or right-identity for
any individual element.

This noticeably increases the number of puzzles that can be solved at
Hard mode without resorting to Unreasonable-level recursion. In a test
of 100 Hard puzzles generated with this change, 80 of them are
reported as Unreasonable by the previous solver.

(One of those puzzles is 12i:m12b9a1zd9i6d10c3y2l11q4r , the example
case that exposed the latin.c validation bug described by the previous
two commits. That was reported as ambiguous with the validation bug,
as Unreasonable with the validation bug fixed, and now it's merely
Hard, because this identity-based deduction eliminates the need for
recursion.)
This commit is contained in:
Simon Tatham
2020-05-22 18:57:15 +01:00
parent 31cb5227e6
commit 6285c44610

View File

@ -43,7 +43,7 @@
#define DIFFLIST(A) \ #define DIFFLIST(A) \
A(TRIVIAL,Trivial,NULL,t) \ A(TRIVIAL,Trivial,NULL,t) \
A(NORMAL,Normal,solver_normal,n) \ A(NORMAL,Normal,solver_normal,n) \
A(HARD,Hard,NULL,h) \ A(HARD,Hard,solver_hard,h) \
A(EXTREME,Extreme,NULL,x) \ A(EXTREME,Extreme,NULL,x) \
A(UNREASONABLE,Unreasonable,NULL,u) A(UNREASONABLE,Unreasonable,NULL,u)
#define ENUM(upper,title,func,lower) DIFF_ ## upper, #define ENUM(upper,title,func,lower) DIFF_ ## upper,
@ -445,6 +445,98 @@ static int solver_normal(struct latin_solver *solver, void *vctx)
return 0; return 0;
} }
static int solver_hard(struct latin_solver *solver, void *vctx)
{
bool done_something = false;
int w = solver->o;
#ifdef STANDALONE_SOLVER
char **names = solver->names;
#endif
int i, j;
/*
* In identity-hidden mode, systematically rule out possibilities
* for the group identity.
*
* In solver_normal, we used the fact that any filled square in
* the grid whose contents _does_ match one of the elements it's
* the product of - that is, ab=a or ab=b - tells you immediately
* that the other element is the identity.
*
* Here, we use the flip side of that: any filled square in the
* grid whose contents does _not_ match either its row or column -
* that is, if ab is neither a nor b - tells you immediately that
* _neither_ of those elements is the identity. And if that's
* true, then we can also immediately rule out the possibility
* that it acts as the identity on any element at all.
*/
for (i = 0; i < w; i++) {
bool i_can_be_id = true;
#ifdef STANDALONE_SOLVER
char title[80];
#endif
for (j = 0; j < w; j++) {
if (grid(i,j) && grid(i,j) != j+1) {
#ifdef STANDALONE_SOLVER
if (solver_show_working)
sprintf(title, "%s cannot be the identity: "
"%s%s = %s =/= %s", names[i], names[i], names[j],
names[grid(i,j)-1], names[j]);
#endif
i_can_be_id = false;
break;
}
if (grid(j,i) && grid(j,i) != j+1) {
#ifdef STANDALONE_SOLVER
if (solver_show_working)
sprintf(title, "%s cannot be the identity: "
"%s%s = %s =/= %s", names[i], names[j], names[i],
names[grid(j,i)-1], names[j]);
#endif
i_can_be_id = false;
break;
}
}
if (!i_can_be_id) {
/* Now rule out ij=j or ji=j for all j. */
for (j = 0; j < w; j++) {
if (cube(i, j, j+1)) {
#ifdef STANDALONE_SOLVER
if (solver_show_working) {
if (title[0]) {
printf("%*s%s\n", solver_recurse_depth*4, "",
title);
title[0] = '\0';
}
printf("%*s ruling out %s at (%d,%d)\n",
solver_recurse_depth*4, "", names[j], i, j);
}
#endif
cube(i, j, j+1) = false;
}
if (cube(j, i, j+1)) {
#ifdef STANDALONE_SOLVER
if (solver_show_working) {
if (title[0]) {
printf("%*s%s\n", solver_recurse_depth*4, "",
title);
title[0] = '\0';
}
printf("%*s ruling out %s at (%d,%d)\n",
solver_recurse_depth*4, "", names[j], j, i);
}
#endif
cube(j, i, j+1) = false;
}
}
}
}
return done_something;
}
#define SOLVER(upper,title,func,lower) func, #define SOLVER(upper,title,func,lower) func,
static usersolver_t const group_solvers[] = { DIFFLIST(SOLVER) }; static usersolver_t const group_solvers[] = { DIFFLIST(SOLVER) };