Futoshiki - Course Lab Book

1. Giới thiệu¶

Tên Futoshiki có nghĩa là bất đẳng thức trong tiếng Nhật. Đây là một trò chơi giải đố điền số dựa trên logic được xuất bản lần đầu tại Nhật Bản và phổ biến trên toàn thế giới. Trò chơi diễn ra trên một lưới kích thước $N \times N$ nơi người chơi phải điền các số từ 1 đến $N$ tuân theo một tập hợp các ràng buộc về cấu trúc và thứ tự. Khác với Sudoku, Futoshiki áp dụng rõ ràng các quan hệ bất đẳng thức, cụ thể là dấu nhỏ hơn < hoặc lớn hơn > giữa các ô liền kề, biến nó thành một miền lý tưởng cho việc rèn luyện tư duy Logic Mệnh đề.

Một câu đố Futoshiki kích thước 4 × 4 ở bên trái và một đáp án hợp lệ ở bên phải. Các
ký hiệu màu đỏ biểu thị các ràng buộc bất đẳng thức. — Figure 1:Một câu đố Futoshiki kích thước 4 × 4 ở bên trái và một đáp án hợp lệ ở bên phải. Các ký hiệu màu đỏ biểu thị các ràng buộc bất đẳng thức.

Trò chơi này cung cấp một bối cảnh tuyệt vời để nghiên cứu Logic Mệnh đề vì các quy tắc của nó hoạt động trên một miền hoàn toàn hữu hạn, cho phép mọi trạng thái và ràng buộc có thể được làm phẳng thành Dạng chuẩn Hội, được biết đến với tên gọi Conjunctive Normal Form. Bài thực hành yêu cầu sinh viên mô hình hóa trò chơi bằng các biến và mệnh đề logic, tự xây dựng các cơ chế mã hóa tự động và đánh giá hiệu suất của các bộ giải SAT solver trên các câu đố có kích thước tăng dần.

2. Mô tả bài toán¶

Một câu đố Futoshiki kích thước $N$ được chơi trên lưới $N \times N$ . Mỗi ô được xác định bởi chỉ số dòng $i$ và chỉ số cột $j$ đều chạy từ 1 đến $N$ . Một số ô đã được điền sẵn một con số được gọi là các gợi ý cho trước. Các dấu bất đẳng thức như < hoặc > có thể xuất hiện giữa các ô kề nhau theo chiều ngang hoặc chiều dọc. Chương trình giải cần gán một số từ 1 đến $N$ cho mỗi ô trống sao cho:

Mỗi dòng là một hoán vị: mỗi số từ 1 đến $N$ xuất hiện đúng một lần trên mỗi dòng.
Mỗi cột là một hoán vị: mỗi số từ 1 đến $N$ xuất hiện đúng một lần trên mỗi cột.
Các ràng buộc bất đẳng thức được thỏa mãn: nếu có một ràng buộc chỉ ra rằng ô $(i, j)$ nhỏ hơn ô $(i, j')$ , thì giá trị được gán cho ô $(i, j)$ phải tuân thủ nghiêm ngặt việc nhỏ hơn giá trị gán cho ô $(i, j')$ . Điều này áp dụng tương tự cho dấu > và cho các ràng buộc theo chiều dọc.
Các gợi ý cho trước được giữ nguyên: các ô đã có số điền sẵn phải giữ nguyên giá trị của chúng.

2.1 Mô hình hóa bằng Logic Mệnh đề¶

Trong bài thực hành này, sinh viên sẽ mô hình hóa và giải quyết Futoshiki bằng Logic Mệnh đề. Vì kích thước bảng và miền giá trị là hữu hạn, chúng ta có thể định nghĩa một biến boolean cho mọi trường hợp gán giá trị có thể xảy ra.

Gọi $P_{i,j,v}$ là một mệnh đề boolean nhận giá trị True nếu ô ở dòng $i$ và cột $j$ chứa giá trị $v$ , và nhận giá trị False trong trường hợp ngược lại. Các chỉ số $i$ , $j$ , $v$ đều chạy từ 1 đến $N$ . Mô hình này tạo ra chính xác $N^3$ biến boolean riêng biệt.

Sinh viên phải biểu diễn từng quy tắc của câu đố thành một tập hợp các mệnh đề logic. Các hạng mục ràng buộc mẫu cần được hoàn thiện và lập trình trong mã nguồn của bạn được liệt kê dưới đây nhằm định hướng quá trình mô hình hóa.

Tri thức A1, Mỗi ô có ít nhất một giá trị: Đối với mỗi dòng $i$ và cột $j$ , ô tương ứng phải chứa ít nhất một giá trị từ miền khả thi:

\bigwedge_{i=1}^{N} \bigwedge_{j=1}^{N} \bigvee_{v=1}^{N} P_{i,j,v}

(1)

Tri thức A2, Mỗi ô có nhiều nhất một giá trị: Đối với mỗi dòng $i$ và cột $j$ , ô tương ứng không thể chứa hai giá trị phân biệt $v_1$ và $v_2$ :

\bigwedge_{i=1}^{N} \bigwedge_{j=1}^{N} \bigwedge_{v_1=1}^{N-1} \bigwedge_{v_2=v_1+1}^{N} \neg\left(P_{i,j,v_1} \land P_{i,j,v_2}\right)

(2)

Tri thức A3, Tính duy nhất trên mỗi dòng: Đối với mỗi dòng $i$ và giá trị $v$ , giá trị này không thể xuất hiện tại hai cột phân biệt $j_1$ và $j_2$ :

\bigwedge_{i=1}^{N} \bigwedge_{v=1}^{N} \bigwedge_{j_1=1}^{N-1} \bigwedge_{j_2=j_1+1}^{N} \neg\left(P_{i,j_1,v} \land P_{i,j_2,v}\right)

(3)

Tri thức A4, Ràng buộc nhỏ hơn theo chiều ngang: Nếu câu đố chỉ định rằng ô $(i, j)$ nhỏ hơn ô $(i, j+1)$ , chúng ta phải cấm tất cả các phép gán mà giá trị $v_1$ ở ô bên trái lớn hơn hoặc bằng giá trị $v_2$ ở ô bên phải:

\bigwedge_{v_1=1}^{N} \bigwedge_{v_2=v_1}^{N} \neg\left(P_{i,j,v_1} \land P_{i,j+1,v_2}\right)

(4)

Tri thức A5, Tuân thủ gợi ý cho trước: Nếu ô $(i, j)$ được điền sẵn giá trị $v$ , chúng ta khẳng định mệnh đề tương ứng là một mệnh đề đơn vị, còn gọi là unit clause:

P_{i,j,v}

(5)

Sinh viên phải tự suy luận và xây dựng các ràng buộc còn lại bao gồm: tính duy nhất trên mỗi cột, cùng toàn bộ các ràng buộc bất đẳng thức theo chiều dọc hoặc ràng buộc lớn hơn theo cùng một phong cách Logic Mệnh đề như trên.

2.2 Giải quyết bằng SAT Solver¶

Việc giải bài toán Futoshiki có thể được quy đổi hoàn toàn thành Bài toán Thỏa mãn Boolean, thường được biết đến với tên gọi là SAT. Để giải quyết câu đố bằng máy tính, các ràng buộc mệnh đề đã nêu ở trên phải được chuyển đổi thành Dạng chuẩn Hội.

Dạng chuẩn Hội yêu cầu toàn bộ công thức logic phải là một phép hội lớn của các mệnh đề, trong đó mỗi mệnh đề là một phép tuyển của các literal. Lấy ví dụ, ràng buộc quy định một ô có nhiều nhất một giá trị vốn dĩ đã được định nghĩa là một phép hội bị phủ định. Bằng cách sử dụng các định lý De Morgan, công thức này dễ dàng biến đổi thành phép tuyển của các literal bị phủ định, giúp nó tương thích hoàn toàn với Dạng chuẩn Hội.

Sau khi các ràng buộc được tạo ra và định dạng thành các mệnh đề chuẩn bởi chương trình Python của bạn, tập hợp này sẽ được nạp vào thư viện pysat. Các bộ giải SAT hiện đại sử dụng các thuật toán dựa nhiều vào phép phân giải mệnh đề đơn vị (unit propagation) cùng kỹ thuật học mệnh đề dựa trên xung đột để tìm kiếm nhanh chóng trong không gian boolean và trả về một phép gán giá trị chân lý thỏa mãn bài toán. Chương trình của bạn sau đó phải ánh xạ các mệnh đề mang giá trị True trở lại thành các con số gán cho lưới.

3. Định dạng dữ liệu¶

3.1 Dữ liệu đầu vào¶

Sinh viên cần truy cập các trang web cung cấp trò chơi Futoshiki để thu thập các đầu vào mẫu dùng cho việc kiểm thử và định hướng phát triển giải pháp. Việc thu thập đa dạng các bố cục câu đố từ những tài nguyên trực tuyến này sẽ đảm bảo mô hình logic của bạn hoạt động ổn định trên nhiều mức độ khó khác nhau. Khi kiểm thử cục bộ trên máy tính cá nhân, sinh viên phải định dạng các dữ liệu mẫu đã thu thập theo cấu trúc cụ thể được định nghĩa dưới đây để khớp với chuẩn đầu vào mà môi trường chấm điểm tự động sẽ cung cấp.

Mỗi dữ liệu đầu vào sử dụng định dạng sau, trong đó toạ độ được đánh số từ 0:

N                    # kích thước lưới N×N
# Lưới: N dòng, mỗi dòng N giá trị cách nhau bởi khoảng trắng.
# Số 0 biểu thị ô trống; từ 1 đến N biểu thị số được điền sẵn.
<giá trị ô (0,0)> <giá trị ô (0,1)> ... <giá trị ô (0,N-1)>
...
M                    # số dòng bất đẳng thức
# M dòng bất đẳng thức: r1 c1 r2 c2 rel
# rel là ký tự '<' hoặc '>', mô tả quan hệ giữa ô (r1,c1) và ô (r2,c2)
<r1> <c1> <r2> <c2> <rel>
...

3.2 Dữ liệu đầu ra¶

Dữ liệu đầu ra biểu diễn lưới đã được giải hoàn chỉnh và in ra chuẩn stdout. Chương trình phải in ra chính xác $N$ dòng, mỗi dòng chứa $N$ số nguyên cách nhau bởi khoảng trắng, đại diện cho các giá trị cuối cùng được gán từ 1 đến $N$ .

Ví dụ đầu ra cho câu đố kích thước 4 × 4:

4. Ví dụ minh họa¶

Hãy xem xét ví dụ lưới 3 × 3 sau đây để định hướng quá trình mô hình hóa của bạn:

Figure 2:Ví dụ lưới 3 × 3 với một gợi ý cho trước và hai ràng buộc bất đẳng thức theo chiều ngang.

Các dữ kiện đã biết cho ví dụ này bao gồm: một gợi ý cho trước tại ô $(1, 2)$ là số 2, một ràng buộc nhỏ hơn theo chiều ngang giữa ô $(1, 1)$ và ô $(1, 2)$ , cùng một ràng buộc lớn hơn theo chiều ngang giữa ô $(3, 2)$ và ô $(3, 3)$ .

Biên dịch các dữ kiện này thành các mệnh đề đơn vị và ràng buộc trong logic mệnh đề ta có:

$P_{1,2,2}$ mang giá trị True do đây là mệnh đề đơn vị cho trước.
$\neg\left(P_{1,1,v_1} \land P_{1,2,v_2}\right)$ với mọi $v_1 \geq v_2$ , dựa trên ràng buộc nhỏ hơn.

Khi được nạp vào một SAT solver, thuật toán lan truyền mệnh đề đơn vị sẽ ngay lập tức đơn giản hóa công thức. Vì $P_{1,2,2}$ là True, bất kỳ phép gán nào có $v_2 = 2$ đều kích hoạt ràng buộc bất đẳng thức. Do đó, bộ giải sẽ đánh giá $\neg\left(P_{1,1,v_1} \land \text{True}\right)$ đối với các giá trị $v_1 \geq 2$ , buộc các mệnh đề $\neg P_{1,1,2}$ và $\neg P_{1,1,3}$ phải nhận giá trị True.

Kết hợp với ràng buộc quy định ô $(1, 1)$ phải có ít nhất một giá trị từ miền khả thi là $\{1, 2, 3\}$ , mệnh đề duy nhất còn lại không bị làm sai là $P_{1,1,1}$ . Bộ giải suy luận logic một cách triệt để rằng ô $(1, 1)$ phải chứa giá trị 1. Sinh viên cần lập trình một cơ chế mã hóa tổng quát cho phép bộ giải pysat thực hiện các suy luận chính xác này một cách có hệ thống.

5. Quy cách chấm điểm và Môi trường¶

5.1 Yêu cầu cài đặt¶

Sinh viên phải viết một chương trình Python để phân tích các đầu vào câu đố Futoshiki từ chuẩn stdin, chuyển đổi các quy tắc cấu trúc và gợi ý cho trước thành một cơ sở tri thức Logic Mệnh đề, đồng thời giải quyết mô hình này bằng thư viện pysat. Khi bộ giải tìm thấy một phép gán thỏa mãn, chương trình phải giải mã các biến mệnh đề ngược lại thành các giá trị trên lưới và in lưới đã được giải ra chuẩn stdout theo đúng định dạng đã quy định ở phần trước.

5.2 Giới hạn hệ thống¶

Kích thước dữ liệu: giới hạn trên của bảng kích thước $N$ là 40.
Bộ nhớ RAM: tối đa 2GB cho mỗi mã nguồn thực thi.
Thời gian chạy tối đa: 10 giây cho mỗi test case. Nếu một bài nộp vượt quá giới hạn thời gian này, bị lỗi dừng đột ngột hoặc xuất ra trạng thái bảng không hợp lệ, bài làm sẽ nhận điểm 0 cho test case cụ thể đó.
Môi trường chấm điểm: hệ thống chạy mô phỏng trên một Google Colab CPU instance, cấu hình cố định nhằm đảm bảo môi trường ổn định và tái lập kết quả tốt nhất, sử dụng Ubuntu và Python từ phiên bản 3.10 trở đi.
Giới hạn thư viện: môi trường thực thi bị hạn chế nghiêm ngặt. Các thư viện bên ngoài duy nhất mà sinh viên được phép sử dụng là numpy, scipy, pandas và pysat. Sinh viên được phép dùng bất kỳ thư viện built-in có sẵn trong Python của phiên bản tương ứng. Bất kỳ engine giải toán, giao diện lập trình toán học hoặc công cụ bên ngoài nào khác đều không được cung cấp và không được phép sử dụng.

5.3 Tiêu chí tính điểm¶

Việc chấm điểm được thực hiện hoàn toàn thông qua một hệ thống tự động dựa trên từng test case riêng biệt. Điểm của sinh viên trong từng test case được tính dựa trên thứ hạng cạnh tranh với các bạn trong lớp. Các bài nộp xuất ra đáp án đúng trong giới hạn thời gian sẽ được xếp hạng dựa trên tổng thời gian chạy của thuật toán. Hệ thống thưởng điểm cao hơn cho các mô hình logic được tối ưu hóa tốt và xử lý nhanh chóng. Điểm tổng kết của toàn bài là trung bình cộng điểm quy đổi từ thứ hạng của tất cả các test case đã được đánh giá.

6. Nộp bài¶

Sinh viên nộp duy nhất một file mã nguồn Python với định dạng tên <MSSV>.py, trong đó thay thế cụm MSSV bằng Mã số sinh viên thực tế của bạn, lên hệ thống Moodle trước thời hạn quy định. Không cần nộp kèm requirements.txt: các thư viện được phép, gồm numpy, scipy, pandas và pysat, đã được cài sẵn trên môi trường chấm điểm.

7. Các lưu ý khác¶

Đây là một bài tập cá nhân. Mỗi sinh viên phải hoàn thành phần cài đặt mã nguồn một cách độc lập.
Thời lượng thực hiện dự kiến khoảng 2 tuần.
Mọi hành vi đạo văn, sử dụng tiểu xảo gian lận hoặc thiếu trung thực sẽ dẫn đến điểm 0 cho toàn bộ khóa học. Hệ thống tự động sẽ được triển khai để phát hiện sự tương đồng trong mã nguồn.

Hết.