tło

Sudoku to łamigłówka liczbowa, w której, biorąc pod uwagę siatkę $n \times n$ podzieloną na pola o rozmiarze $n$ , każda liczba od $1$ do $n$ powinna pojawić się dokładnie raz w każdym rzędzie, kolumnie i pudełku.

W grze w szachy król może przejść do dowolnej (maksymalnie) 8 sąsiednich komórek po kolei. „Przylegający” oznacza tutaj przyleganie w poziomie, w pionie lub po przekątnej.

Trasa króla jest analogią do trasy rycerza; jest to (prawdopodobnie otwarta) ścieżka, która odwiedza każdą komórkę dokładnie raz na danej planszy z ruchami Szachowego Króla.

Zadanie

Rozważ siatkę Sudoku 6 na 6:

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

oraz trasa króla (od 01do 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

Trasa składa się z 36 cyfr 654654564463215641325365231214123321.

Wzięcie innej trasy króla daje większe liczby; na przykład mogę znaleźć ścieżkę, która zaczyna się od, 65<6>56446556...która jest zdecydowanie większa od powyższej. Możesz zmienić planszę Sudoku, aby uzyskać jeszcze wyższe liczby:

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

Ta niekompletna tablica podaje sekwencję początkową, 666655546...która jest optymalną sekwencją 9 cyfr początkowych.

Twoim zadaniem jest znalezienie największej takiej liczby dla standardowego Sudoku 9 na 9 z polami 3 na 3 , tj

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

Pamiętaj, że to wyzwanie nie jest golfem kodowym ; skupiamy się raczej na znalezieniu rozwiązań niż na napisaniu małego programu, który teoretycznie działa.

Kryterium punktacji i wygranej

Wynik zgłoszenia to 81-cyfrowy numer znaleziony przez Twój program. Zgłoszenie z najwyższym wynikiem wygrywa. Twój program powinien także wypisać planszę Sudoku i trasę króla w czytelnej dla człowieka formie; dołącz je do swojego zgłoszenia.

Twój program może wyświetlać wiele wyników; Twój wynik to ich maksimum.

Twój program nie ma limitu czasu. Jeśli Twój program nadal działa, a następnie znajdzie wyższą liczbę, możesz zaktualizować wynik przesłania, edytując post. Tiebreaker to najwcześniejszy czas na osiągnięcie wyniku, tj. Albo czas wysłania (jeśli nie jest jeszcze edytowany), albo czas edycji, kiedy wynik został zaktualizowany (w przeciwnym razie).

Python + Z3 , 999899898789789787876789658767666545355432471632124566352413452143214125313214321, optymalny

Działa za około pół godziny, produkując

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

Kod

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