Contexte

Le Sudoku est un puzzle numérique où, étant donné une grille $n \times n$ divisée en boîtes de taille $n$ , chaque nombre de $1$ à $n$ doit apparaître exactement une fois dans chaque ligne, colonne et boîte.

Dans le jeu d'échecs, le roi peut se déplacer vers n'importe laquelle (au plus) des 8 cellules adjacentes à la fois. "Adjacent" signifie ici horizontalement, verticalement ou diagonalement adjacent.

La tournée du roi est une analogie avec la tournée du chevalier; c'est un chemin (éventuellement ouvert) qui visite chaque cellule exactement une fois sur le plateau donné avec les mouvements de Chess King.

Tâche

Considérons une grille Sudoku 6 par 6:

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

et une visite du roi (du 01au 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

La visite constitue le numéro à 36 chiffres 654654564463215641325365231214123321.

Faire un tour du roi différent donne un plus grand nombre; par exemple, je peux trouver un chemin qui commence par 65<6>56446556...qui est nettement supérieur à ce qui précède. Vous pouvez changer la carte Sudoku pour obtenir des nombres encore plus élevés:

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

Cette carte incomplète donne la séquence de départ 666655546...qui est la séquence optimale de 9 chiffres de départ.

Votre tâche consiste à trouver le plus grand nombre de ce type pour le Sudoku 9 x 9 standard avec des boîtes 3 x 3 , c'est -à- dire

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

Notez que ce défi n'est pas du code-golf ; l'objectif est de trouver réellement les solutions plutôt que d'écrire un petit programme qui fonctionne théoriquement.

Critère de notation et de victoire

Le score d'une soumission est le nombre à 81 chiffres trouvé par votre programme. La soumission avec le score le plus élevé gagne. Votre programme devrait également produire la grille Sudoku et la visite du roi sous une forme lisible par l'homme; veuillez les inclure dans votre soumission.

Votre programme peut produire plusieurs résultats; votre score est le maximum d'entre eux.

Il n'y a pas de limite de temps pour votre programme. Si votre programme continue de fonctionner et trouve un nombre plus élevé par la suite, vous pouvez mettre à jour le score de la soumission en modifiant la publication. Tiebreaker est le moment le plus précoce pour atteindre le score, c'est-à-dire soit le moment de la publication (s'il n'est pas encore édité) ou le moment de l'édition lorsque le score a été mis à jour (sinon).

Python + Z3 , 999899898789789787876789658767666545355432471632124566352413452143214125313214321, optimal

Fonctionne en environ une demi-heure, produisant

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


def adj(a):
    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:
    for b in adj(a):
        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