MỤC LỤC
LỜI CẢM ƠN …………………………………………………………………………………………………
LỜI CAM ĐOAN …………………………………………………………………………………………….
TÓM TẮT ………………………………………………………………………………………………………
BẢNG CÁC THUẬT NGỮ VÀ TỪ VIẾT TẮT ……………………………………………………
DANH MỤC CÁC BẢNG BIỂU ……………………………………………………………………….
DANH MỤC CÁC HÌNH VẼ …………………………………………………………………………….
CHƯƠNG 1. GIỚI THIỆU ……………………………………………………………………………… 1
1.1. Bài toán SAT …………………………………………………………………………………………. 1
1.2. Lôgic mệnh đề ……………………………………………………………………………………….. 1
1.2.1. Công thức Lôgic mệnh đề ………………………………………………………………… 1
1.2.2. Chuẩn tắc hội CNF …………………………………………………………………………. 4
1.3. SAT Solver …………………………………………………………………………………………….. 5
1.4. Phương pháp SAT Encoding ……………………………………………………………………… 5
1.4.1. Trò chơi Hitori ……………………………………………………………………………….. 5
1.4.2. Trò chơi Sodoku …………………………………………………………………………….. 7
1.4.3. Trò chơi Slitherlink …………………………………………………………………………. 8
1.5. Một số ứng dụng khác của SAT ……………………………………………………………….. 12
CHƯƠNG 2. CÁC KỸ THUẬT SAT SOLVING CƠ BẢN ……………………………….. 13
2.1. Thủ tục DPLL truyền thống …………………………………………………………………….. 13
2.1.1. Một số khái niệm cơ bản ………………………………………………………………… 13
2.1.2. Các luật cơ bản của thủ tục DPLL ……………………………………………………. 14
2.2. Thủ tục DPLL hiện đại ……………………………………………………………………………. 17
2.2.1. Backjumping ………………………………………………………………………………… 17
2.2.2. Learn và Forget …………………………………………………………………………….. 18
2.2.3. Mệnh đề Backjump ……………………………………………………………………….. 19
2.3. Thuật toán CDCL…………………………………………………………………………………… 26
2.3.1. Nội dung chính của CDCL ……………………………………………………………… 26
2.3.2. Giải thuật CDCL …………………………………………………………………………… 27
2.3.3. Suy diễn mệnh đề và mức quay lui …………………………………………………… 27
2.3.4. Biểu đồ kéo theo …………………………………………………………………………… 28
2.3.5. Học từ mệnh đề xung đột ……………………………………………………………….. 29
2.4. Kỹ thuật Two -Watched literals……………………………………………………………….. 34
2.4.1. Watched literal …………………………………………………………………………….. 34
2.4.2. Two- Watched literal …………………………………………………………………….. 35
2.5. Giải pháp loại bỏ biến và loại bỏ mệnh đề ………………………………………………….. 36
2.5.1. Loại bỏ biến …………………………………………………………………………………. 37
2.5.2. Loại bỏ mệnh đề …………………………………………………………………………… 39
CHƯƠNG 3. CÁC KỸ THUẬT SAT SOLVING TIÊN TIẾN HIỆN NAY …………… 42
3.1. GlueMiniSat …………………………………………………………………………………………. 42
3.1.1. Giới thiệu …………………………………………………………………………………….. 42
3.1.2. Tiêu chí đánh giá Learn Clause ……………………………………………………….. 42
3.1.3. Chiến lược tự khởi động lại ……………………………………………………………. 44
3.2. Glucose ………………………………………………………………………………………………… 44
3.2.1. Quản lý mệnh đề học …………………………………………………………………….. 44
3.2.2. Khởi động lại ……………………………………………………………………………….. 45
CHƯƠNG 4. THỰC NGHIỆM……………………………………………………………………… 46
4.1. Giới thiệu về MiniSat ……………………………………………………………………………… 46
4.2. Giao diện lập trình ứng dụng ……………………………………………………………………. 46
4.3. Tổng quan về Minisat …………………………………………………………………………….. 47
4.4. Thực nghiệm …………………………………………………………………………………………. 50
4.4.1. Biên dịch Minisat ………………………………………………………………………….. 50
4.4.2. Biên dịch GlueMinisat …………………………………………………………………… 51
4.4.3. Biên dịch Glucose …………………………………………………………………………. 51
4.4.4. Bộ dữ liệu thực nghiệm ………………………………………………………………….. 52
4.4.5. Thực nghiệm ………………………………………………………………………………… 52
KẾT LUẬN ………………………………………………………………………………………………… 56
TÀI LIỆU THAM KHẢO……………………………………………………………………………… 56
