Giải bài toán 8 hậu trên Pygame với Z3

by Pymier0

img

Pygame vốn để làm game, nhưng cũng là một công cụ tiện lợi để hiển thị các vấn đề. Tải pygame pip install pygame rồi viết code:

Hiện 1 cửa sổ vuông tương ứng với bàn cờ, kích thước 800x800 pixel:

import time
import pygame
pygame.init()

display = pygame.display.set_mode((800, 800))
pygame.display.set_caption("Z3 8 queens - pymi.vn")
running = True
while running:
    time.sleep(1)

Tạo bề mặt để vẽ, là 1 object Surface, đổ nền trắng, và tính toán để tô đen các ô đan xen. Hệ màu được sử dụng là RGB (Red, Green, Blue), mỗi màu được thể hiện bằng 3 con số trong khoảng 0-255, viết bằng hệ 16 (hexadecimal) sẽ có dạng 0x00 -> 0xff.

white = (0xff, 0xff, 0xff)
black = (0x00, 0x00, 0x00)

cell_size = 100
board = pygame.Surface((cell_size * 8, cell_size * 8))
board.fill(white)

cntr = 0
for x in range(8):
    for y in range(8):
        if cntr % 2 == 0:
            pygame.draw.rect(board, black,
(x*cell_size, y*cell_size, cell_size, cell_size))
        cntr += 1
    cntr += 1

while running:
    display.blit(board, board.get_rect())
    pygame.display.flip()
    time.sleep(1)

Đã được bàn cờ với các ô đen và trắng.

Mang code bài giải 8 hậu trước ghép vào, dùng 1 bức ảnh bên ngoài để đại diện cho quân hậu:

def find_queens():
    from z3 import Int, And, Distinct, Solver
    queens = [Int(f'Q{i+1}') for i in range(8)]
    columns = [And(1 <= q, q <=8) for q in queens]
    distinct = [Distinct(queens)]
    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()
    return m

#...
m = find_queens()
d = {i.name(): m[i].as_long() for i in m}
image = pygame.image.load("beerqueen.PNG")

while running:
    display.blit(board, board.get_rect())

    for row in range(8):
        for col in range(8):
            if row+1 == d[f'Q{col+1}']:
                board.blit(image, (row*cell_size, col * cell_size))

    pygame.display.flip()

Kết quả:

8queenpygame

full code tại đây

Đă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.