Giải bài toán 8 quân hậu bằng Z3

by Pymier0

img

Bài toán 8 quân hậu: bàn cờ vua kích thước 8x8, có 8 quân hậu, tìm vị trí sao cho 8 con không ăn được nhau (không cùng hàng ngang, cột, chéo). Bài toán này được giải bằng thuật toán backtracking.

Backtracking giải bài này là thử đặt 1 quân hậu ở vị trí bất kỳ, và tiếp tục đặt quân tiếp theo sao cho không ăn được quân trước, cứ tiếp tục cho đến khi tìm ra 8 vị trí. Nếu sau một số bước, thấy không thể đặt được quân ở vị trí nào phù hợp thì quay trở lại để thay đổi vị trí của bước trước đó rồi tiếp tục - nên gọi là backtracking.

Khi biểu diễn bài toán, có 2 cách:

  • tìm 8 cặp điểm (16 biến), ứng với tọa độ của từng quân hậu
  • gọi q1,q2, … q8 là các quân hậu ở cột 1-8, việc còn lại là tìm vị trí hàng của mỗi quân. Ở đây dùng cách này.

Tạo 8 biến:

from z3 import *
queens = [Int(f'Q{i+1}') for i in range(8)]
pp(queens)
# [Q1, Q2, Q3, Q4, Q5, Q6, Q7, Q8]

Điều kiện để các quân hậu nằm trong bàn cờ:

rows = [And(1 <= q, q <=8) for q in queens]
pp(rows)

# output
[And(Q1 >= 1, Q1 <= 8),
 And(Q2 >= 1, Q2 <= 8),
 And(Q3 >= 1, Q3 <= 8),
 And(Q4 >= 1, Q4 <= 8),
 And(Q5 >= 1, Q5 <= 8),
 And(Q6 >= 1, Q6 <= 8),
 And(Q7 >= 1, Q7 <= 8),
 And(Q8 >= 1, Q8 <= 8)]

Thêm điều kiện để các quân ở các dòng riêng biệt “distinct”:

distinct = [Distinct(queens)]
pp(distinct)
# [Distinct(Q1, Q2, Q3, Q4, Q5, Q6, Q7, Q8)]

Cuối cùng, thêm điều kiện để mỗi quân sau không cùng hàng chéo với quân trước. Hai quân cùng hàng chéo khi giá trị truyệt đối: |x2-x1| == |y2-y1|. Do ta đã mô hình cột (y) vào tên các biến, điều kiện ở đây sẽ là: |q2 - q1| != 1, |q3-q1| != 2, |q3-q2| != 1, …

do Z3 không có function abs, có thể viết thành 2 điều kiện: q2 - q1 != 1 và q2 - q1 != -1.

diags = [And(queens[i] - queens[j] != i - j,
             queens[i] - queens[j] != j - i)
         for i in range(8) for j in range(i)]

Giải tìm 1 nghiệm của bài toán:

solver = Solver()
solver.add(columns+ distinct + diags)
solver.check()
m = solver.model()
pp(m)
# [Q2 = 4, Q8 = 3, Q5 = 5, Q6 = 7, Q4 = 8, Q7 = 1, Q1 = 6, Q3 = 2]

Vẽ lên để kiểm tra:

d = {i.name(): m[i].as_long() for i in m}

for row in range(8):
    for col in range(8):
        if row+1 == d[f'Q{col+1}']:
            print(f'Q{col+1}', end=" ")
        else:
            print("__", end=" ")
    print()

__ __ __ __ __ __ Q7 __
__ __ Q3 __ __ __ __ __
__ __ __ __ __ __ __ Q8
__ Q2 __ __ __ __ __ __
__ __ __ __ Q5 __ __ __
Q1 __ __ __ __ __ __ __
__ __ __ __ __ Q6 __ __
__ __ __ Q4 __ __ __ __

Toàn bộ code:

from z3 import *
queens = [Int(f'Q{i+1}') for i in range(8)]
pp(queens)

columns = [And(1 <= q, q <=8) for q in queens]
pp(columns)

distinct = [Distinct(queens)]
pp(distinct)

diags = [And(queens[i] - queens[j] != i - j,
             queens[i] - queens[j] != j - i)
         for i in range(8) for j in range(i)]

solver = Solver()
solver.add(columns+ distinct + diags)
solver.check()
m = solver.model()
pp(m)

Tham khảo: https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Đăng ký ngay tại PyMI.vn để học Python tại Hà Nội TP HCM (Sài Gòn), trở thành lập trình viên #python chuyên nghiệp ngay sau khóa học.

back to top