# Maximize Sudoku King's tour

## Background

Sudoku is a number puzzle where, given an $$\ n \times n \$$ grid divided into boxes of size $$\ n \$$, each number of $$\ 1 \$$ to $$\ n \$$ should appear exactly once in each row, column and box.

In the game of Chess, the King can move to any of (at most) 8 adjacent cells in a turn. "Adjacent" here means horizontally, vertically or diagonally adjacent.

The King's tour is an analogy of the Knight's tour; it is a (possibly open) path that visits every cell exactly once on the given board with Chess King's movements.

Consider a 6-by-6 Sudoku grid:

654 | 321
123 | 654
----+----
462 | 135
315 | 246
----+----
536 | 412
241 | 563


and a King's tour (from 01 to 36):

01 02 03 | 34 35 36
31 32 33 | 04 05 06
---------+---------
30 23 28 | 27 26 07
22 29 24 | 25 09 08
---------+---------
21 19 16 | 10 14 13
20 17 18 | 15 11 12


The tour forms the 36-digit number 654654564463215641325365231214123321.

Taking a different King's tour gives larger numbers; for example, I can find a path that starts with 65<6>56446556... which is definitely greater than the above. You can change the Sudoku board to get even higher numbers:

... | ...
.6. | ...
----+----
..6 | ...
.5. | 6..
----+----
.45 | .6.
6.. | 5..


This incomplete board gives the starting sequence of 666655546... which is the optimal sequence of 9 starting digits.

Your task is to find the largest such number for standard 9-by-9 Sudoku with 3-by-3 boxes, i.e.

... | ... | ...
... | ... | ...
... | ... | ...
----+-----+----
... | ... | ...
... | ... | ...
... | ... | ...
----+-----+----
... | ... | ...
... | ... | ...
... | ... | ...


Note that this challenge is not ; the focus is to actually find the solutions rather than to write a small program that theoretically works.

## Scoring & winning criterion

The score of a submission is the 81-digit number found by your program. The submission with the highest score wins. Your program should also output the Sudoku grid and the King's tour in human-readable form; please include them in your submission.

Your program may output multiple results; your score is the maximum of them.

There's no time limit for your program. If your program continues to run and finds a higher number afterwards, you can update the submission's score by editing the post. Tiebreaker is the earliest time to achieve the score, i.e. either the time of post (if it's not edited yet) or the time of edit when the score was updated (otherwise).

• On your self-nomination of this challenge for Best of PPCG, you mention that "This is probably the first [code-challenge] to ask directly for the optimized solution, rather than some score combined with code length or such." I just wanted to let you know that that's not true - there's Shortest Universal Maze Exit String which was posted in 2015. – Esolanging Fruit Feb 8 '19 at 6:23

# Python + Z3, 999899898789789787876789658767666545355432471632124566352413452143214125313214321, optimal

Runs in about half an hour, producing

1 3 4 8 9 7 6 2 5
2 9 7 1 5 6 8 3 4
5 6 8 4 2 3 7 9 1
4 7 6 2 1 5 9 8 3
8 5 1 6 3 9 2 4 7
9 2 3 7 8 4 1 5 6
3 8 5 9 6 1 4 7 2
6 4 9 5 7 2 3 1 8
7 1 2 3 4 8 5 6 9
81 79 78 14 15 16 54 57 56
80 12 13 77 52 53 17 55 58
34 33 11 51 76 75 18  1 59
35 10 32 50 74 72  2 19 60
9 36 49 31 73  3 71 61 20
8 48 37 30  4 69 70 62 21
47  7 38  5 29 68 65 22 63
46 43  6 39 28 67 66 64 23
44 45 42 41 40 27 26 25 24
999899898789789787876789658767666545355432471632124566352413452143214125313214321


### Code

import z3

x, y = a
for x1 in range(max(0, x - 1), min(9, x + 2)):
for y1 in range(max(0, y - 1), min(9, y + 2)):
if (x1, y1) != a:
yield x1, y1

solver = z3.SolverFor("QF_FD")

squares = list((x, y) for x in range(9) for y in range(9))
num = {(x, y): z3.Int(f"num{x}_{y}") for x, y in squares}
for a in squares:
solver += 1 <= num[a], num[a] <= 9
for cells in (
[[(x, y) for y in range(9)] for x in range(9)]
+ [[(x, y) for x in range(9)] for y in range(9)]
+ [
[(x, y) for x in range(i, i + 3) for y in range(j, j + 3)]
for i in range(0, 9, 3)
for j in range(0, 9, 3)
]
):
solver += z3.Distinct([num[x, y] for x, y in cells])
for k in range(1, 10):
solver += z3.Or([num[x, y] == k for x, y in cells])

move = {
((x0, y0), (x1, y1)): z3.Bool(f"move{x0}_{y0}_{x1}_{y1}")
for x0, y0 in squares
for x1, y1 in adj((x0, y0))
}
tour = {(x, y): z3.Int(f"tour{x}_{y}") for x, y in squares}
for a in squares:
solver += 0 <= tour[a], tour[a] < 81
for a in squares:
solver += z3.PbEq([(move[a, b], 1) for b in adj(a)] + [(tour[a] == 80, 1)], 1)
for b in squares:
solver += z3.PbEq([(move[a, b], 1) for a in adj(b)] + [(tour[b] == 0, 1)], 1)
solver += z3.Distinct([tour[a] for a in squares])
for t in range(81):
solver += z3.Or([tour[a] == t for a in squares])
for a in squares:
solver += move[a, b] == (tour[a] + 1 == tour[b])

value = [z3.Int(f"value{t}") for t in range(81)]
for t in range(81):
solver += 1 <= value[t], value[t] <= 9
for a in squares:
for t in range(81):
solver += z3.Implies(tour[a] == t, num[a] == value[t])

assert solver.check() != z3.unsat
opt = 0
while opt < 81:
model = solver.model()
for y in range(9):
print(*(model[num[x, y]] for x in range(9)))
for y in range(9):
print(*(f"{model[tour[x, y]].as_long() + 1:2}" for x in range(9)))
best = [model[value[t]].as_long() for t in range(81)]
print(*best, sep="")
print()
while opt < 81:
improve = z3.Bool(f"improve{opt}_{best[opt]}")
solver += improve == (value[opt] > best[opt])
if solver.check(improve) != z3.unsat:
break
solver += value[opt] == best[opt]
opt += 1

• Surely I overestimated the problem way too much. And I completely forgot the dark magic of Z3... – Bubbler Oct 22 '18 at 0:34
• @Bubbler being certain an optimal solution is out of reach is difficult. I've made the same mistake myself - and mine lasted even less time before someone posted an optimal solution... codegolf.stackexchange.com/a/51974/20283 – trichoplax Feb 24 '19 at 13:38
• Mine's not salvageable, but I wonder if this challenge could work as a variation with a bigger board and a different chess piece (perhaps a follow on challenge linking back to this one) – trichoplax Feb 24 '19 at 13:41