Link tải luận văn miễn phí cho ae Kết Nối
CÔNG TRÌNH DỰ THI
GIẢI THƯỞNG “SINH VIÊN NGHIÊN CỨU KHOA HỌC”
NĂM 2015
Tên công trình: Phương pháp SAT Encoding hiệu quả giải quyết trò chơi
Logic Hitori
Họ và tên sinh viên:
Trần Trọng Tiệp Nam Lớp: K56CLC
Vũ Đình Thắng Nam Lớp: K56CLC
Đào Thị Thúy Nữ Lớp: K56CLC
Nguyễn Tuấn Anh Nam Lớp: K58CA
Nguyễn Thị Mai Hương Nữ Lớp: K58CA
Khoa: Công nghệ thông tin
Người hướng dẫn: TS. Tô Văn Khánh
MỞ ĐẦU
Bài toán SAT (Satisfiability) là bài toán chứng minh tính thỏa mãn hay không thỏa mãn (SAT/UNSAT) của một công thức logic mệnh đề. Các công cụ chứng minh tự động cho bài toán này được gọi là SAT Solver, chúng có nhiều ứng dụng trong trí tuệ nhân tạo hay trong các bài toán kiểm chứng, kiểm thử phần mềm. Các SAT Solver đóng vai trò như các công cụ nền (backend engine) cho các SMT (SAT Modulo Theories) Solver, là các công cụ chứng minh tính thỏa mãn của các công thức logic xây dựng trên lý thuyết logic vị từ cấp I (First Order Logic - FOL).
Một số bài toán có thể được giải bằng việc đưa về bài toán SAT, biểu diễn vấn đề bằng các công thức logic mệnh đề và áp dụng SAT Solver vào giải các công thức logic mệnh đề đó, cách tiếp cận đó được gọi là SAT Encoding.
Trong báo cáo này chúng tui trình bày các thuật toán giải Hitori bằng các giải thuật tìm kiếm kết hợp quay lui và SAT Encoding. Cũng trong báo cáo chúng tui đề xuất một phương pháp SAT Encoding mới để giải trò chơi Lôgic Hitori, được đặt tên là Connectivity Encoding. Chúng tui đã tiến hành thực nghiệm trên 120 bài toán dữ liệu đầu vào để đánh giá tính hiệu quả của phương pháp Connectivity Encoding so với các phương pháp đã đề xuất trước đấy. Connectivity Encoding cho kết quả vượt trội so với phương pháp Chains & Cycles Encoding (một phương pháp SAT Encoding được đề xuất trước đó) và kết quả cạnh tranh so với 2 giải thuật tìm kiếm kết hợp quay lui.
DANH MỤC CÁC THUẬT NGỮ VIẾT TẮT.
Thuật ngữ Tên đầy đủ
SAT Satisfiability
UNSAT Unsatisfiability
CNF Conjunctive Normal Form
NP Nondeterministic Polynomial
SMT SAT Modulo Theories
MỤC LỤC
MỞ ĐẦU ii
I. GIỚI THIỆU 1
I.1 Trò chơi logic Hitori 1
I.2 Luật chơi của Hitori 1
II. CÁC GIẢI THUẬT TÌM KIẾM ĐỂ GIẢI QUYẾT HITORI 4
II.1 Thuật toán tìm kiếm thứ nhất. 4
II.2 Thuật toán tìm kiếm thứ hai 5
III. PHƯƠNG PHÁP SAT ENCODING 7
III.1 Các khái niệm cơ bản về SAT Encoding 7
III.2 SAT Encoding giải Hitori. 10
III.2.1 SAT Encoding cho hai luật đầu của Hitori 10
III.2.2 Chains & Cycles Encoding 12
III.2.3 Phương pháp Connectivity Encoding. 15
III.2.4 Tối ưu dựa trên dữ liệu đầu vào 18
IV. THỰC NGHIỆM 21
IV.1 Môi trường thực nghiệm 21
IV.2 Kết quả thực nghiệm 21
IV.2.1 Kết quả so sánh hai thuật toán SAT Encoding 21
IV.2.2 So sánh 4 giải thuật của Hitori. 24
KẾT LUẬN……………………………………………………………………………..28
DANH MỤC CÁC HÌNH ẢNH
Hình 1.1: Ví dụ về câu đố Hitori 1
Hình 1.2: Ví dụ về luật 1 của Hitori 1
Hình 1.3: Ví dụ về vi phạm luật 2 Hitori 2
Hình 1.4: Cách giải đúng luật 2 Hitori 2
Hình 1.5: Ví dụ về vi phạm luật 3 2
Hình 1.6: Cách giải luật 3 không vi phạm 2
Hình 1.7: Đầu vào Hitori 3
Hình 1.8: Lời giải hoàn chỉnh Hitori 3
Hình 2.1: Một số mẫu điển hình 4
Hình 2.2: Một số mẫu cơ bản 5
Hình 2.3: Các mẫu nâng cao 6
Hình 3.1: Game Sudoku 8
Hình 3.2: Sơ đồ giải SAT 9
Hình 3.3: Các ô lân cận 12
Hình 3.4: Ví dụ về Chains 12
Hình 3.5: Ví dụ về Cycles 12
Hình 3.6: Áp dụng quy tắc loại bỏ Chains 13
Hình 3.7: Áp dụng luật loại bỏ Cycles 13
Hình 3.8: Ví dụ về liên kết trong Connectivity Encoding 15
Hình 3.9: Lân cận của một ô 16
Hình 3.10: Các ô biên đen ngăn cách ô trắng 17
Hình 3.11: Kết nối có hướng 17
Hình 3.12: Ví dụ về tập bội số trên ma trận 18
DANH MỤC BẢNG BIỂU VÀ BIỂU ĐỒ
Bảng 3.1: Số lượng Chains và Cycles 14
Bảng 3.2: So sánh số lượng mệnh đề, biến, thời gian khi đã tối ưu 20
Bảng 4.1: So sánh kết quả của hai phương pháp Encoding khi đã optimize. 22
Biểu đồ 4.1: Số lượng mệnh đề hai phương pháp Encoding 23
Biểu đồ 4.2: So sánh thời gian chạy của hai phương pháp Encoding 24
Bảng 4.2: So sánh kết quả 4 giải thuật 25
Biểu đồ 4.3: So sánh thời gian chạy 4 thuật toán 26
I. GIỚI THIỆU
I.1 Trò chơi logic Hitori
Hitori [4] (Hitori ni shite kure; nghĩa là "hãy để tui một mình") là một trò chơi logic từ Nhật Bản, được chơi trên một ma trận với kích thước n x n với và cho trước các số từ 1 đến n. Người chơi lần lượt phải bôi đen các ô số sao cho chúng thỏa mãn các luật của trò chơi. Nó lần đầu tiên xuất hiện trên Nikoli [4] (tháng 3 năm 1990).
Hình 1.1: Ví dụ về câu đố Hitori
I.2 Luật chơi của Hitori
Luật chơi của Hitori bao gồm 3 luật về bôi đen các ô trên hàng, trên cột được trình bày dưới đây:
• Luật 1: Giá trị của số trong mỗi ô không được xuất hiện nhiều hơn một lần ở mỗi hàng, mỗi cột
2 2 1 5 3
2 3 1 4 5
1 1 1 3 5
1 3 5 4 2
5 4 3 2 1
Hình 1.2: Ví dụ về luật 1 của Hitori
Trên cùng một hàng hay cột, các số xuất hiện nhiều hơn một lần sẽ phải bôi đen (xóa ô đó đi) để thỏa mãn luật 1. Hình 1.2 thể hiện cho ta thấy luật 1 của Hitori, trên cột thứ nhất giá trị 2, 1 không thể xuất hiện nhiều hơn một lần, bởi vậy một trong hai ô có giá trị 2, 1 trên cột 1 đã được xóa đi (bôi đen).
• Luật 2: Các ô được bôi đen không được nằm liền kề nhau trên hàng hay cột
Nếu ô có vị trí (i, j) (hàng i, cột j) được bôi đen thì 4 ô tại các vị trí liền kề của nó là (i+1,j), (i, j+1), (i-1, j), (i, j-1) sẽ không được bôi đen.
Như ta thấy trên hình 1.3. Tại hàng 3, hai ô có giá trị 1 cạnh nhau đều được bôi đen, điều này đã vi phạm luật 2 của Hitori. Hình 1.4 trình bày cách giải đúng với đầu vào tương tự hình 3.
• Luật 3: Mọi ô không bôi đen (ô trắng) phải kết nối được với nhau. Nói cách khác luôn tồn tại một đường đi từ mọi ô trắng đến các ô trắng còn lại.
Ở hình 1.5 hai ô có giá trị 5 được bôi đen đã tạo thành một đường ngăn cách ô trắng có giá trị 3 trong góc với các ô trắng khác (vi phạm luật 3 của Hitori). Hình 1.6 là cách giải đúng luật 3.
Trên đây là ba luật cơ bản của Hitori, với các luật trên, ta có thể đưa ra lời giải chính xác, đầy đủ ba luật Hitori như hình 1.8 với đầu vào là ma trận 1.7.
Lưu ý: Với một ma trận đầu vào Hitori có thể có nhiều hơn một đáp án lời giải. Phương pháp SAT Encoding có thể tìm ra tất cả các lời giải của Hitori.
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
CÔNG TRÌNH DỰ THI
GIẢI THƯỞNG “SINH VIÊN NGHIÊN CỨU KHOA HỌC”
NĂM 2015
Tên công trình: Phương pháp SAT Encoding hiệu quả giải quyết trò chơi
Logic Hitori
Họ và tên sinh viên:
Trần Trọng Tiệp Nam Lớp: K56CLC
Vũ Đình Thắng Nam Lớp: K56CLC
Đào Thị Thúy Nữ Lớp: K56CLC
Nguyễn Tuấn Anh Nam Lớp: K58CA
Nguyễn Thị Mai Hương Nữ Lớp: K58CA
Khoa: Công nghệ thông tin
Người hướng dẫn: TS. Tô Văn Khánh
MỞ ĐẦU
Bài toán SAT (Satisfiability) là bài toán chứng minh tính thỏa mãn hay không thỏa mãn (SAT/UNSAT) của một công thức logic mệnh đề. Các công cụ chứng minh tự động cho bài toán này được gọi là SAT Solver, chúng có nhiều ứng dụng trong trí tuệ nhân tạo hay trong các bài toán kiểm chứng, kiểm thử phần mềm. Các SAT Solver đóng vai trò như các công cụ nền (backend engine) cho các SMT (SAT Modulo Theories) Solver, là các công cụ chứng minh tính thỏa mãn của các công thức logic xây dựng trên lý thuyết logic vị từ cấp I (First Order Logic - FOL).
Một số bài toán có thể được giải bằng việc đưa về bài toán SAT, biểu diễn vấn đề bằng các công thức logic mệnh đề và áp dụng SAT Solver vào giải các công thức logic mệnh đề đó, cách tiếp cận đó được gọi là SAT Encoding.
Trong báo cáo này chúng tui trình bày các thuật toán giải Hitori bằng các giải thuật tìm kiếm kết hợp quay lui và SAT Encoding. Cũng trong báo cáo chúng tui đề xuất một phương pháp SAT Encoding mới để giải trò chơi Lôgic Hitori, được đặt tên là Connectivity Encoding. Chúng tui đã tiến hành thực nghiệm trên 120 bài toán dữ liệu đầu vào để đánh giá tính hiệu quả của phương pháp Connectivity Encoding so với các phương pháp đã đề xuất trước đấy. Connectivity Encoding cho kết quả vượt trội so với phương pháp Chains & Cycles Encoding (một phương pháp SAT Encoding được đề xuất trước đó) và kết quả cạnh tranh so với 2 giải thuật tìm kiếm kết hợp quay lui.
DANH MỤC CÁC THUẬT NGỮ VIẾT TẮT.
Thuật ngữ Tên đầy đủ
SAT Satisfiability
UNSAT Unsatisfiability
CNF Conjunctive Normal Form
NP Nondeterministic Polynomial
SMT SAT Modulo Theories
MỤC LỤC
MỞ ĐẦU ii
I. GIỚI THIỆU 1
I.1 Trò chơi logic Hitori 1
I.2 Luật chơi của Hitori 1
II. CÁC GIẢI THUẬT TÌM KIẾM ĐỂ GIẢI QUYẾT HITORI 4
II.1 Thuật toán tìm kiếm thứ nhất. 4
II.2 Thuật toán tìm kiếm thứ hai 5
III. PHƯƠNG PHÁP SAT ENCODING 7
III.1 Các khái niệm cơ bản về SAT Encoding 7
III.2 SAT Encoding giải Hitori. 10
III.2.1 SAT Encoding cho hai luật đầu của Hitori 10
III.2.2 Chains & Cycles Encoding 12
III.2.3 Phương pháp Connectivity Encoding. 15
III.2.4 Tối ưu dựa trên dữ liệu đầu vào 18
IV. THỰC NGHIỆM 21
IV.1 Môi trường thực nghiệm 21
IV.2 Kết quả thực nghiệm 21
IV.2.1 Kết quả so sánh hai thuật toán SAT Encoding 21
IV.2.2 So sánh 4 giải thuật của Hitori. 24
KẾT LUẬN……………………………………………………………………………..28
DANH MỤC CÁC HÌNH ẢNH
Hình 1.1: Ví dụ về câu đố Hitori 1
Hình 1.2: Ví dụ về luật 1 của Hitori 1
Hình 1.3: Ví dụ về vi phạm luật 2 Hitori 2
Hình 1.4: Cách giải đúng luật 2 Hitori 2
Hình 1.5: Ví dụ về vi phạm luật 3 2
Hình 1.6: Cách giải luật 3 không vi phạm 2
Hình 1.7: Đầu vào Hitori 3
Hình 1.8: Lời giải hoàn chỉnh Hitori 3
Hình 2.1: Một số mẫu điển hình 4
Hình 2.2: Một số mẫu cơ bản 5
Hình 2.3: Các mẫu nâng cao 6
Hình 3.1: Game Sudoku 8
Hình 3.2: Sơ đồ giải SAT 9
Hình 3.3: Các ô lân cận 12
Hình 3.4: Ví dụ về Chains 12
Hình 3.5: Ví dụ về Cycles 12
Hình 3.6: Áp dụng quy tắc loại bỏ Chains 13
Hình 3.7: Áp dụng luật loại bỏ Cycles 13
Hình 3.8: Ví dụ về liên kết trong Connectivity Encoding 15
Hình 3.9: Lân cận của một ô 16
Hình 3.10: Các ô biên đen ngăn cách ô trắng 17
Hình 3.11: Kết nối có hướng 17
Hình 3.12: Ví dụ về tập bội số trên ma trận 18
DANH MỤC BẢNG BIỂU VÀ BIỂU ĐỒ
Bảng 3.1: Số lượng Chains và Cycles 14
Bảng 3.2: So sánh số lượng mệnh đề, biến, thời gian khi đã tối ưu 20
Bảng 4.1: So sánh kết quả của hai phương pháp Encoding khi đã optimize. 22
Biểu đồ 4.1: Số lượng mệnh đề hai phương pháp Encoding 23
Biểu đồ 4.2: So sánh thời gian chạy của hai phương pháp Encoding 24
Bảng 4.2: So sánh kết quả 4 giải thuật 25
Biểu đồ 4.3: So sánh thời gian chạy 4 thuật toán 26
I. GIỚI THIỆU
I.1 Trò chơi logic Hitori
Hitori [4] (Hitori ni shite kure; nghĩa là "hãy để tui một mình") là một trò chơi logic từ Nhật Bản, được chơi trên một ma trận với kích thước n x n với và cho trước các số từ 1 đến n. Người chơi lần lượt phải bôi đen các ô số sao cho chúng thỏa mãn các luật của trò chơi. Nó lần đầu tiên xuất hiện trên Nikoli [4] (tháng 3 năm 1990).
Hình 1.1: Ví dụ về câu đố Hitori
I.2 Luật chơi của Hitori
Luật chơi của Hitori bao gồm 3 luật về bôi đen các ô trên hàng, trên cột được trình bày dưới đây:
• Luật 1: Giá trị của số trong mỗi ô không được xuất hiện nhiều hơn một lần ở mỗi hàng, mỗi cột
2 2 1 5 3
2 3 1 4 5
1 1 1 3 5
1 3 5 4 2
5 4 3 2 1
Hình 1.2: Ví dụ về luật 1 của Hitori
Trên cùng một hàng hay cột, các số xuất hiện nhiều hơn một lần sẽ phải bôi đen (xóa ô đó đi) để thỏa mãn luật 1. Hình 1.2 thể hiện cho ta thấy luật 1 của Hitori, trên cột thứ nhất giá trị 2, 1 không thể xuất hiện nhiều hơn một lần, bởi vậy một trong hai ô có giá trị 2, 1 trên cột 1 đã được xóa đi (bôi đen).
• Luật 2: Các ô được bôi đen không được nằm liền kề nhau trên hàng hay cột
Nếu ô có vị trí (i, j) (hàng i, cột j) được bôi đen thì 4 ô tại các vị trí liền kề của nó là (i+1,j), (i, j+1), (i-1, j), (i, j-1) sẽ không được bôi đen.
Như ta thấy trên hình 1.3. Tại hàng 3, hai ô có giá trị 1 cạnh nhau đều được bôi đen, điều này đã vi phạm luật 2 của Hitori. Hình 1.4 trình bày cách giải đúng với đầu vào tương tự hình 3.
• Luật 3: Mọi ô không bôi đen (ô trắng) phải kết nối được với nhau. Nói cách khác luôn tồn tại một đường đi từ mọi ô trắng đến các ô trắng còn lại.
Ở hình 1.5 hai ô có giá trị 5 được bôi đen đã tạo thành một đường ngăn cách ô trắng có giá trị 3 trong góc với các ô trắng khác (vi phạm luật 3 của Hitori). Hình 1.6 là cách giải đúng luật 3.
Trên đây là ba luật cơ bản của Hitori, với các luật trên, ta có thể đưa ra lời giải chính xác, đầy đủ ba luật Hitori như hình 1.8 với đầu vào là ma trận 1.7.
Lưu ý: Với một ma trận đầu vào Hitori có thể có nhiều hơn một đáp án lời giải. Phương pháp SAT Encoding có thể tìm ra tất cả các lời giải của Hitori.
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
You must be registered for see links