This puzzle from New Scientist’s Enigma series is solved here with the program from a published study of logic-programming solutions to it. The program searches over grids whose rows, rearranged, give back the columns, numbers the cells, and keeps the arrangement with the highest score in a single pass.
Run it in the playground · Source
In the program’s formulation: take an 8 × 8 grid of cells. Rearranging its rows by some permutation must give its transpose (rows become columns), and all rows must differ. Cells that the symmetry forces to be equal share a number. Numbers are handed out so that more frequent cells get larger numbers. Which permutation and grid give the largest total, the sum over all cells?
square(Size, M, Total, Frequencies, Permutation) :-
var_matrix(Size, M),
ad_partition(Size, Partition),
rep_perm(Size, Partition, Permutation),
list_permute(Permutation, M, P),
transpose_matrix(P, M),
distinct(M),
eval_matrix(M, Frequencies),
total(Frequencies, Total).
The grid starts as 64 unbound variables. Instead of trying all 8! row permutations, the program tries one representative for each cycle type, enumerated as integer partitions of 8. Unifying the permuted rows with the transpose then forces cells to share variables.
:- table generator/2.
enigma1225(Size, [Permutation, Board, Max]) :-
aggregate_max(Total, board(M, Perm),
square(Size, M, Total, _, Perm),
Max, board(Board, Permutation)).
aggregate_max/5 keeps only the best candidate as the search runs.
generator/2, which enumerates the partitions, is tabled.
eyeprolog examples/enigma1225.pl
enigma1225(8, [[2, 1, 4, 3, 6, 5, 8, 7], [[1, 1, 2, 3, 4, 5, 6, 7], [1, 1, 3, 2, 5, 4, 7, 6], [3, 2, 8, 8, 9, 10, 11, 12], [2, 3, 8, 8, 10, 9, 12, 11], [5, 4, 10, 9, 13, 13, 14, 15], [4, 5, 9, 10, 13, 13, 15, 14], [7, 6, 12, 11, 15, 14, 16, 16], [6, 7, 11, 12, 14, 15, 16, 16]], 544]).
The best permutation swaps rows in pairs: 2, 1, 4, 3, 6, 5, 8, 7. The grid then uses the numbers 1 to 16, each in exactly four cells, for a total of 4 × (1 + 2 + … + 16) = 544.
eyeprolog --proof examples/enigma1225.pl
step(enigma1225(8, [[2, 1, 4, 3, 6, 5, 8, 7], [[1, 1, 2, 3, 4, 5, 6, 7], [1, 1, 3, 2, 5, 4, 7, 6], [3, 2, 8, 8, 9, 10, 11, 12], [2, 3, 8, 8, 10, 9, 12, 11], [5, 4, 10, 9, 13, 13, 14, 15], [4, 5, 9, 10, 13, 13, 15, 14], [7, 6, 12, 11, 15, 14, 16, 16], [6, 7, 11, 12, 14, 15, 16, 16]], 544]),
rule(2),
The proof is short: the answer rests on clause 2 and a single
aggregate_max/5 step that chose this board as the maximum.
eyeprolog --proof examples/enigma1225.pl > enigma1225.why.pl
eyeprolog --check-proof enigma1225.why.pl examples/enigma1225.pl
condition('C1', resolution, ok, 1).
condition('C4', coverage, ok, 2).
condition('C7', relevance, ok, 3).
obligation(builtin, theory_scoped, aggregate_max(A, board(B, C), square(8, B, A, D, C), 544, board([[1, 1, 2, 3, 4, 5, 6, 7], [1, 1, 3, 2, 5, 4, 7, 6], [3, 2, 8, 8, 9, 10, 11, 12], [2, 3, 8, 8, 10, 9, 12, 11], [5, 4, 10, 9, 13, 13, 14, 15], [4, 5, 9, 10, 13, 13, 15, 14], [7, 6, 12, 11, 15, 14, 16, 16], [6, 7, 11, 12, 14, 15, 16, 16]], [2, 1, 4, 3, 6, 5, 8, 7]))).
verdict(checked_with_obligations).
The rule step replays, but “544 is the maximum” is a claim about the whole search, so it is an obligation: the checker records it as assumed rather than proved. Here, the arithmetic above gives an independent sanity check.
--goal 'enigma1225(4, R)' for a 4 × 4 grid and predict the total
first.--goal 'square(8, M, T, _, [2, 1, 4, 3, 6, 5, 8, 7])' to see the
winning permutation on its own.Learn more in The Art of EyeProlog, Chapter 28 (symmetry reduces search).