Maksimalkan tur Sudoku King

16

Latar Belakang

Sudoku adalah teka-teki angka di mana, mengingat kotak n×n dibagi menjadi kotak-kotak berukuran n , setiap angka 1 hingga n harus muncul tepat satu kali di setiap baris, kolom, dan kotak.

Dalam permainan Catur, Raja dapat berpindah ke salah satu (paling banyak) 8 sel yang berdekatan secara bergantian. "Berdekatan" di sini berarti berdampingan secara horizontal, vertikal atau diagonal.

Tur The King adalah analogi dari tur Knight; itu adalah jalan (mungkin terbuka) yang mengunjungi setiap sel tepat sekali di papan yang diberikan dengan gerakan Catur King.

Tugas

Pertimbangkan kisi Sudoku 6-kali-6:

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

dan tur King (dari 01ke 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

Tur membentuk angka 36 digit 654654564463215641325365231214123321.

Mengambil tur King yang berbeda memberi jumlah yang lebih besar; misalnya, saya dapat menemukan jalur yang dimulai dengan 65<6>56446556...yang pasti lebih besar dari yang di atas. Anda dapat mengubah papan Sudoku untuk mendapatkan angka lebih tinggi:

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

Papan tidak lengkap ini memberikan urutan awal 666655546...yang merupakan urutan optimal dari 9 digit awal.

Tugas Anda adalah menemukan angka terbesar untuk standar 9-by-9 Sudoku dengan 3-oleh-3 kotak , yaitu

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

Perhatikan bahwa tantangan ini bukan ; fokusnya adalah untuk benar-benar menemukan solusi daripada menulis sebuah program kecil yang secara teori berfungsi.

Kriteria penilaian & menang

Skor pengiriman adalah angka 81 digit yang ditemukan oleh program Anda. Pengajuan dengan skor tertinggi akan menang. Program Anda juga harus menampilkan kisi Sudoku dan tur Raja dalam bentuk yang dapat dibaca manusia; harap sertakan mereka dalam kiriman Anda.

Program Anda dapat menampilkan beberapa hasil; skor Anda adalah maksimum dari mereka.

Tidak ada batasan waktu untuk program Anda. Jika program Anda terus berjalan dan menemukan angka yang lebih tinggi setelahnya, Anda dapat memperbarui skor pengiriman dengan mengedit posting. Tiebreaker adalah waktu paling awal untuk mencapai skor, yaitu waktu posting (jika belum diedit) atau waktu edit ketika skor diperbarui (jika tidak).

Bubbler
sumber
2
Pada penentuan sendiri tantangan ini untuk Best of PPCG, Anda menyebutkan bahwa "Ini mungkin [tantangan kode] pertama yang meminta langsung untuk solusi yang dioptimalkan, daripada beberapa skor yang dikombinasikan dengan panjang kode atau semacamnya." Saya hanya ingin memberi tahu Anda bahwa itu tidak benar - ada String Keluar Labirin Universal Terpendek yang diposting pada tahun 2015.
Esolanging Fruit

Jawaban:

19

Python + Z3 , 999899898789789787876789658767666545355432471632124566352413452143214125313214321, optimal

Berjalan sekitar setengah jam, menghasilkan

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

Kode

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
sumber
Tentunya saya terlalu melebih-lebihkan masalahnya. Dan saya benar-benar melupakan sihir gelap Z3 ...
Bubbler
@ Lubbler memastikan solusi optimal tidak terjangkau. Saya sendiri telah melakukan kesalahan yang sama - dan waktu saya bertahan lebih sedikit sebelum seseorang memposting solusi optimal ... codegolf.stackexchange.com/a/51974/20283
trichoplax
Milik saya tidak bisa diselamatkan, tapi saya ingin tahu apakah tantangan ini bisa berfungsi sebagai variasi dengan papan yang lebih besar dan bidak catur yang berbeda (mungkin tindak tantangan yang menghubungkan kembali ke yang satu ini)
trichoplax