Maximieren Sie die Tour des Sudoku-Königs

16

Hintergrund

Sudoku ist ein Zahlenrätsel, bei dem bei einem in Felder der Größe unterteilten Raster jede Zahl von bis in jeder Zeile, Spalte und jedem Feld genau einmal vorkommen sollte.n×nn1n

Im Schachspiel kann der König in einer Runde in eine von maximal 8 benachbarten Zellen ziehen. "Angrenzend" bedeutet hier horizontal, vertikal oder diagonal benachbart.

Die Königstour ist eine Analogie zur Rittertour; Es ist ein (möglicherweise offener) Pfad, der mit den Bewegungen von Chess King jede Zelle genau einmal auf dem angegebenen Brett besucht.

Aufgabe

Betrachten Sie ein 6-mal-6-Sudoku-Gitter:

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

und eine Königstour (von 01bis 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

Die Tour bildet die 36-stellige Nummer 654654564463215641325365231214123321.

Wenn Sie eine andere Königstour unternehmen, erhalten Sie eine größere Anzahl. Zum Beispiel kann ich einen Pfad finden, 65<6>56446556...der definitiv größer ist als der oben genannte. Sie können das Sudoku-Board ändern, um noch höhere Zahlen zu erhalten:

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

Diese unvollständige Tafel gibt die Startsequenz an, 666655546...deren optimale Sequenz aus 9 Startziffern besteht.

Ihre Aufgabe ist es , die größte solche Zahl für Standard-9-mal-9-Sudoku mit 3-mal-3-Boxen zu finden , dh

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

Beachten Sie, dass es sich bei dieser Herausforderung nicht um . Der Fokus liegt darauf, die Lösungen tatsächlich zu finden, anstatt ein kleines Programm zu schreiben, das theoretisch funktioniert.

Bewertungs & Gewinnkriterium

Das Ergebnis einer Einreichung ist die 81-stellige Zahl, die von Ihrem Programm gefunden wurde. Die Einsendung mit der höchsten Punktzahl gewinnt. Ihr Programm sollte auch das Sudoku-Raster und die Königstour in lesbarer Form ausgeben. Bitte fügen Sie sie Ihrer Einreichung bei.

Ihr Programm gibt möglicherweise mehrere Ergebnisse aus. Ihre Punktzahl ist das Maximum von ihnen.

Es gibt keine zeitliche Begrenzung für Ihr Programm. Wenn Ihr Programm weiterhin ausgeführt wird und danach eine höhere Zahl findet, können Sie die Bewertung der Einreichung aktualisieren, indem Sie den Beitrag bearbeiten. Tiebreaker ist der früheste Zeitpunkt, zu dem die Punktzahl erreicht wird, dh entweder der Zeitpunkt des Posts (falls er noch nicht bearbeitet wurde) oder der Zeitpunkt der Bearbeitung, zu dem die Punktzahl aktualisiert wurde (ansonsten).

Bubbler
quelle
2
Bei Ihrer Selbsternennung dieser Herausforderung für "Best of PPCG" erwähnen Sie Folgendes: "Dies ist wahrscheinlich die erste [Code-Herausforderung], die direkt nach der optimierten Lösung fragt, und nicht nach einer Punktzahl in Kombination mit der Codelänge oder dergleichen." Ich wollte Sie nur wissen lassen, dass das nicht stimmt - es gibt den kürzesten Universal Maze Exit String, der im Jahr 2015 veröffentlicht wurde.
Esolanging Fruit

Antworten:

19

Python + Z3 , 999899898789789787876789658767666545355432471632124566352413452143214125313214321, optimal

Läuft in einer halben Stunde und produziert

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
Anders Kaseorg
quelle
Sicher habe ich das Problem viel zu sehr überschätzt. Und ich habe die dunkle Magie von Z3 komplett vergessen ...
Bubbler
@Bubbler ist sich sicher, dass eine optimale Lösung nicht in Reichweite ist. Ich habe den gleichen Fehler selbst gemacht - und meine dauerte noch weniger Zeit , bis jemand eine optimale Lösung ... geschrieben codegolf.stackexchange.com/a/51974/20283
Trichoplax
Mine ist nicht zu retten, aber ich frage mich, ob diese Herausforderung als Variation mit einem größeren Brett und einer anderen Schachfigur (möglicherweise eine Folgeherausforderung, die auf diese zurückführt) funktionieren könnte
Trichoplax