Luận văn Thạc sĩ: Nghiên cứu các kỹ thuật SAT Solving (ĐH Công Nghệ)

Luận văn thạc sĩ kỹ thuật nghiên cứu các kỹ thuật sat solving luận văn ths máy tính 60 48 01, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải thiện thực tiễn.

• Tác giả: Đặng Thị Như Hoa
• Người hướng dẫn: Ts. Tô Văn Khánh
• Trường học: Trường Đại Học Công Nghệ - Đại Học Quốc Gia Hà Nội
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: Các Kỹ Thuật Sat Solving
• Loại tài liệu: Luận Văn Thạc Sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• 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Ẽ
• 1. CHƢƠNG 1: Bài toán SAT
• 1.1. Bài toán SAT
• 1.2. Công thức Lôgic mệnh đề
• 1.3. Chuẩn tắc hội CNF
• 1.4. Phƣơng pháp SAT Encoding
• 1.4.1. Trò chơi Hitori
• 1.4.2. Trò chơi Sodoku
• 1.4.3. Trò chơi Slitherlink
• 1.4.4. Một số ứng dụng khác của SAT
• 2. CHƢƠNG 2: CÁC KỸ THUẬT SAT SOLVING CƠ BẢN
• 2.1. Thủ tục DPLL truyền thống
• 2.1.1. Một số khái niệm cơ bản
• 2.1.2. Các luật cơ bản của thủ tục DPLL
• 2.2. Thủ tục DPLL hiện đại
• 2.2.1. Learn và Forget
• 2.2.2. Thuật toán CDCL
• 2.2.2.1. Nội dung chính của CDCL
• 2.2.2.2. Giải thuật CDCL
• 2.2.2.3. Suy diễn mệnh đề và mức quay lui
• 2.3. Biểu đồ kéo theo
• 2.4. Học từ mệnh đề xung đột
• 2.5. Kỹ thuật Two -Watched literals
• 2.5.1. Two- Watched literal
• 2.6. Giải pháp loại bỏ biến và loại bỏ mệnh đề
• 2.6.1. Loại bỏ biến
• 2.6.2. Loại bỏ mệnh đề
• 3. CHƢƠNG 3: CÁC KỸ THUẬT SAT SOLVING TIÊN TIẾN HIỆN NAY
• 3.1. Tiêu chí đánh giá Learn Clause
• 3.2. Chiến lƣợc tự khởi động lại
• 3.3. Quản lý mệnh đề học
• 3.3.1. Khởi động lại
• 3.4. Giới thiệu về MiniSat
• 3.4.1. Giao diện lập trình ứng dụng
• 3.4.2. Tổng quan về Minisat
• 3.4.3. Biên dịch Minisat
• 3.4.4. Biên dịch GlueMinisat
• 3.4.5. Biên dịch Glucose
• 4. CHƢƠNG 4:
• 4.1. Bộ dữ liệu thực nghiệm
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Luận Văn Thạc Sĩ Về Kỹ Thuật SAT Solving

Luận văn thạc sĩ về kỹ thuật SAT Solving tập trung vào việc nghiên cứu và phân tích các phương pháp giải bài toán SAT (Satisfiability), một bài toán quan trọng trong lĩnh vực khoa học máy tính và trí tuệ nhân tạo. Bài toán SAT là bài toán xác định xem một công thức logic mệnh đề có tồn tại một phép gán giá trị cho các biến sao cho công thức đó có giá trị đúng hay không. Các công cụ tự động giải bài toán SAT, được gọi là SAT Solver, đóng vai trò quan trọng trong việc giải quyết các vấn đề thực tế phức tạp. Ngày nay, các SAT Solver không chỉ là công cụ độc lập mà còn là nền tảng cho các SMT (SAT Modulo Theories) Solver, giúp giải quyết các bài toán logic trên lý thuyết vị từ cấp I. Nghiên cứu về SMT Solver đang là một lĩnh vực phát triển mạnh mẽ, với ứng dụng rộng rãi trong kiểm chứng và kiểm thử chương trình. Bài toán SAT thuộc lớp NP-đầy đủ (NP-complete), và các kỹ thuật giải SAT đã được nghiên cứu và phát triển trong thời gian dài. Tuy nhiên, sự phát triển vượt bậc của các SAT Solver gần đây, thể hiện qua các cuộc thi SAT Competition hàng năm, cho thấy nhiều cải tiến đáng kể trong việc cài đặt và tối ưu hóa các SAT Solver. Các SAT Solver hiện đại có khả năng xử lý các công thức với hàng triệu biến và hàng trăm ngàn mệnh đề. Mục tiêu của luận văn là đi sâu vào các kỹ thuật cơ bản và thuật toán cốt lõi được sử dụng trong các SAT Solver, đồng thời đưa ra các ví dụ minh họa cụ thể để làm rõ cách thức hoạt động của chúng. Các kỹ thuật này được triển khai trong MiniSAT, một SAT Solver mã nguồn mở phổ biến, đóng vai trò là nền tảng cho nhiều SAT Solver mạnh mẽ khác. Bên cạnh đó, luận văn cũng khám phá các kỹ thuật tiên tiến như GlueMinisat và Glucose, đang được tích hợp trong các SAT Solver hàng đầu hiện nay. Luận văn sẽ tiến hành thực nghiệm so sánh hiệu năng của ba SAT Solver này trên các bộ dữ liệu chuẩn từ cuộc thi SAT Competition, nhằm đánh giá tính hiệu quả và khả năng giải quyết bài toán của các kỹ thuật tiên tiến. Luận văn này bao gồm các vấn đề cơ bản như lôgic mệnh đề, bài toán SAT, các SAT Solver và ứng dụng của phương pháp SAT Encoding. Luận văn bao gồm các kỹ thuật SAT solving cơ bản bao gồm thủ tục DPLL, và các kỹ thuật áp dụng trong DPLL nhƣ: CDCL, Back Jumping, 2 Watched literals, Clause Elimination.

1.1. Bài Toán SAT và Độ Phức Tạp Tính Toán Liên Quan

Bài toán SAT là một bài toán thuộc lớp NP-đầy đủ, điều này có nghĩa là không có thuật toán nào có thể giải quyết nó trong thời gian đa thức nếu P ≠ NP. Độ phức tạp SAT là một vấn đề quan trọng trong khoa học máy tính, vì nhiều bài toán tối ưu hóa và quyết định có thể được chuyển đổi thành bài toán SAT. Do đó, việc phát triển các thuật toán SAT hiệu quả có ý nghĩa lớn trong việc giải quyết các vấn đề thực tế. Các nhà nghiên cứu đã nỗ lực rất nhiều để cải thiện hiệu suất của các SAT Solver, dẫn đến sự ra đời của nhiều kỹ thuật và phương pháp khác nhau. Theo tài liệu luận văn, bài toán SAT là bài toán chứng minh sự thỏa mãn (SAT / UNSAT) của một công thức Lôgic mệnh đề và các công cụ tự động SAT Solver đóng vai trò là các bộ giải công thức đó.

1.2. Tổng Quan Các Thành Phần Chính Của Một SAT Solver

Một SAT Solver điển hình bao gồm các thành phần chính như: lan truyền ràng buộc (Boolean Constraint Propagation - BCP), phân tích xung đột, học mệnh đề (clause learning), và quay lui (backtracking). BCP là một kỹ thuật quan trọng để giảm không gian tìm kiếm bằng cách suy diễn các giá trị cho các biến dựa trên các mệnh đề đã biết. Phân tích xung đột được sử dụng để xác định lý do gây ra xung đột và tạo ra các mệnh đề học mới để ngăn chặn các xung đột tương tự trong tương lai. Học mệnh đề là quá trình thêm các mệnh đề mới vào cơ sở tri thức của SAT Solver để cải thiện hiệu suất. Quay lui được sử dụng khi một xung đột được phát hiện và SAT Solver cần quay trở lại một trạng thái trước đó để thử một nhánh tìm kiếm khác. Giải thuật DPLL là giải thuật cơ bản được cài đặt trong các SAT Solver. Các kỹ thuật này đƣợc cài đặt trong một SAT solver phổ biến hiện nay đó là MiniSAT, một SAT solver mã nguồn mở mà rất nhiều SAT solver mạnh trên thế giới đƣợc mở rộng cải tiến từ SAT Solver này.

1.3. Ứng Dụng Thực Tiễn Của SAT Solving Trong CNTT

SAT Solving có nhiều ứng dụng thực tiễn trong lĩnh vực công nghệ thông tin, bao gồm kiểm chứng phần cứng và phần mềm, lập kế hoạch, tối ưu hóa, và trí tuệ nhân tạo. Trong kiểm chứng, SAT Solving được sử dụng để chứng minh rằng một hệ thống phần cứng hoặc phần mềm đáp ứng các yêu cầu kỹ thuật. Trong lập kế hoạch, SAT Solving được sử dụng để tìm kiếm một chuỗi các hành động để đạt được một mục tiêu nhất định. Trong tối ưu hóa, SAT Solving được sử dụng để tìm kiếm giải pháp tốt nhất cho một bài toán tối ưu hóa tổ hợp. Trong trí tuệ nhân tạo, SAT Solving được sử dụng để giải quyết các bài toán suy luận và lập luận. Ngoài ra, SAT Encoding là một phƣơng pháp mà trong đó một số bài toán có thể đƣợc giải quyết bằng việc đƣa về bài toán SAT: Biểu diễn các vấn đề bằng các công thức Lôgic mệnh đề và áp dụng SAT Solver vào để giải các công thức Lôgic mệnh đề. Các ví dụ điển hình như trò chơi Hitori, trò chơi Sodoku, trò chơi Slitherlink.

II. Phân Tích Chi Tiết Thủ Tục DPLL Và CDCL Trong SAT Solving

Thủ tục DPLL (Davis–Putnam–Logemann–Loveland) là một thuật toán cổ điển để giải bài toán SAT. Nó dựa trên việc tìm kiếm đệ quy và lan truyền ràng buộc. DPLL bao gồm các bước chính sau: chọn một biến chưa được gán giá trị, gán giá trị cho biến đó (thường là true hoặc false), lan truyền ràng buộc để suy diễn các giá trị cho các biến khác, và kiểm tra xem có xung đột hay không. Nếu có xung đột, thuật toán sẽ quay lui và thử một giá trị khác cho biến đã chọn. CDCL (Conflict-Driven Clause Learning) là một cải tiến quan trọng của DPLL, giúp cải thiện hiệu suất của SAT Solver bằng cách học các mệnh đề mới từ các xung đột. CDCL bao gồm các bước sau: phân tích xung đột để xác định lý do gây ra xung đột, tạo ra một mệnh đề học mới để ngăn chặn các xung đột tương tự trong tương lai, và thêm mệnh đề học mới vào cơ sở tri thức của SAT Solver. So với DPLL truyền thống thì CDCL có khả năng giải quyết bài toán nhanh hơn rất nhiều.

2.1. Tìm Hiểu Sâu Về Giải Thuật DPLL Truyền Thống Trong SAT Solving

Giải thuật DPLL là nền tảng cơ bản của nhiều SAT Solver hiện đại. Nó hoạt động bằng cách đệ quy tìm kiếm một phép gán giá trị cho các biến sao cho công thức logic trở nên đúng. DPLL sử dụng các quy tắc đơn giản như lan truyền đơn vị (unit propagation) và phân nhánh (branching) để giảm không gian tìm kiếm. Lan truyền đơn vị là quá trình suy diễn các giá trị cho các biến khi một mệnh đề chỉ còn một literal chưa được gán giá trị. Phân nhánh là quá trình chọn một biến chưa được gán giá trị và thử cả hai giá trị true và false cho biến đó. Thủ tục DPLL hiện đại Learn và Forget giúp các thuật toán tránh lặp lại các sai lầm trong quá khứ, giúp tăng tốc độ giải quyết bài toán. CDCL là một cải tiến quan trọng so với DPLL, cho phép học từ các xung đột và quay lui thông minh hơn.

2.2. Cách CDCL Cải Thiện Hiệu Năng Của SAT Solver Ra Sao

CDCL cải thiện hiệu năng của SAT Solver bằng cách học các mệnh đề mới từ các xung đột. Các mệnh đề học này biểu diễn các ràng buộc bổ sung mà không được thể hiện rõ ràng trong công thức đầu vào. Bằng cách thêm các mệnh đề học vào cơ sở tri thức của SAT Solver, nó có thể tránh lặp lại các xung đột tương tự trong tương lai và giảm không gian tìm kiếm. CDCL cũng sử dụng các kỹ thuật quay lui thông minh hơn, chẳng hạn như quay lui không theo thời gian (non-chronological backtracking), để quay trở lại một trạng thái trước đó mà không cần phải thử tất cả các giá trị trung gian. Giải thuật CDCL bao gồm suy diễn mệnh đề và mức quay lui. Kỹ thuật Two -Watched literals là một kỹ thuật khác giúp cải thiện hiệu suất của BCP trong CDCL. Giải pháp loại bỏ biến và loại bỏ mệnh đề cũng được sử dụng để giảm kích thước của công thức và đơn giản hóa quá trình tìm kiếm.

2.3. Phân Tích Kỹ Thuật Two Watched Literals Trong DPLL và CDCL

Kỹ thuật Two-Watched Literals là một phương pháp hiệu quả để thực hiện lan truyền ràng buộc trong SAT Solver. Ý tưởng chính là chọn hai literal trong mỗi mệnh đề và theo dõi chúng. Khi một trong hai literal này trở nên sai, thì một literal khác trong mệnh đề phải được gán giá trị để làm cho mệnh đề đúng. Nếu không có literal nào như vậy, thì mệnh đề là xung đột và SAT Solver cần quay lui. Kỹ thuật Two-Watched Literals giúp giảm số lượng phép toán cần thiết để thực hiện lan truyền ràng buộc, vì chỉ cần kiểm tra các mệnh đề có các literal đã được theo dõi. Kỹ thuật này đặc biệt hữu ích trong các SAT Solver hiện đại như MiniSAT, GlueMinisat và Glucose. Ví dụ Biểu đồ kéo theo cũng là một ví dụ để sử dụng giải thuật Two-Watched Literals, giúp giảm xung đột cũng như tìm kiếm các biến suy diễn.

III. Các Kỹ Thuật SAT Solving Tiên Tiến GlueMinisat Glucose

Các SAT Solver tiên tiến như GlueMinisat và Glucose sử dụng nhiều kỹ thuật để cải thiện hiệu suất so với DPLL và CDCL truyền thống. Một trong những kỹ thuật quan trọng nhất là quản lý mệnh đề học (clause learning management). Các SAT Solver này sử dụng các tiêu chí khác nhau để đánh giá độ quan trọng của các mệnh đề học và loại bỏ các mệnh đề ít quan trọng để giảm bộ nhớ sử dụng và cải thiện hiệu suất. Một kỹ thuật khác là chiến lược tự khởi động lại (restart strategy). Các SAT Solver này định kỳ khởi động lại quá trình tìm kiếm từ một trạng thái ngẫu nhiên để tránh bị mắc kẹt trong các vùng không gian tìm kiếm khó khăn. Khởi động lại thường được kết hợp với các kỹ thuật ngẫu nhiên hóa (randomization) để khám phá các vùng không gian tìm kiếm khác nhau. Theo luận văn, các kỹ thuật tiên tiến đang đƣợc cài đặt trong các SAT solver mạnh trên thế giới nhƣ GlueMinisat, Glucose.

3.1. Tiêu Chí Đánh Giá Learn Clause Trong Các SAT Solver Mạnh

Tiêu chí đánh giá Learn Clause là một yếu tố quan trọng trong việc quản lý mệnh đề học. Các SAT Solver sử dụng các tiêu chí khác nhau để đánh giá độ quan trọng của các mệnh đề học, chẳng hạn như độ dài của mệnh đề, tần suất sử dụng, và độ tuổi. Các mệnh đề học có độ dài ngắn hơn, tần suất sử dụng cao hơn, và độ tuổi gần đây hơn thường được coi là quan trọng hơn và được giữ lại trong cơ sở tri thức của SAT Solver. Ngược lại, các mệnh đề học có độ dài dài hơn, tần suất sử dụng thấp hơn, và độ tuổi lâu hơn thường được coi là ít quan trọng hơn và có thể bị loại bỏ. Giới thiệu về Minisat đây là một thuật toán cơ bản, Giao diện lập trình ứng dụng cũng rất dễ sử dụng. Tổng quan về Minisat, biên dịch Minisat cũng không quá phức tạp.

3.2. Tìm Hiểu Chiến Lược Tự Khởi Động Lại Trong SAT Solving

Chiến lược tự khởi động lại là một kỹ thuật quan trọng để tránh bị mắc kẹt trong các vùng không gian tìm kiếm khó khăn. Các SAT Solver sử dụng các thuật toán khác nhau để xác định khi nào cần khởi động lại quá trình tìm kiếm. Một trong những thuật toán phổ biến nhất là khởi động lại theo độ phức tạp (complexity-based restart). Thuật toán này khởi động lại quá trình tìm kiếm khi độ phức tạp của các mệnh đề học vượt quá một ngưỡng nhất định. Một thuật toán khác là khởi động lại theo thời gian (time-based restart). Thuật toán này khởi động lại quá trình tìm kiếm sau một khoảng thời gian nhất định. Quản lý mệnh đề học và Khởi động lại là các yếu tố quan trọng trong các SAT Solver hiện đại.

3.3. Ảnh Hưởng Của Quản Lý Mệnh Đề Học Đến Hiệu Suất SAT Solver

Quản lý mệnh đề học có ảnh hưởng lớn đến hiệu suất của SAT Solver. Bằng cách loại bỏ các mệnh đề ít quan trọng, SAT Solver có thể giảm bộ nhớ sử dụng và cải thiện tốc độ lan truyền ràng buộc. Tuy nhiên, việc loại bỏ quá nhiều mệnh đề học có thể làm giảm khả năng học hỏi của SAT Solver và dẫn đến hiệu suất kém hơn. Do đó, việc lựa chọn các tiêu chí đánh giá Learn Clause và thuật toán quản lý mệnh đề học phù hợp là rất quan trọng để đạt được hiệu suất tốt nhất. Luận văn tiến hành chạy thực nghiệm so sánh 3 SAT solver này trên các bộ dữ liệu thực nghiệm chuẩn (từ cuộc thi SAT competition) để thấy rõ tính hiệu quả, tính nhanh nhạy của các kỹ thuật tiên tiến đang đƣợc sử dụng.

IV. Thực Nghiệm So Sánh Các SAT Solver Minisat GlueMinisat Glucose

Luận văn tiến hành thực nghiệm so sánh ba SAT Solver: Minisat, GlueMinisat, và Glucose trên các bộ dữ liệu chuẩn từ cuộc thi SAT Competition. Mục tiêu là đánh giá tính hiệu quả của các kỹ thuật tiên tiến được sử dụng trong GlueMinisat và Glucose so với Minisat. Các kết quả thực nghiệm cho thấy rằng GlueMinisat và Glucose thường có hiệu suất tốt hơn Minisat trên các bài toán khó, đặc biệt là các bài toán có cấu trúc phức tạp. Điều này là do GlueMinisat và Glucose sử dụng các kỹ thuật quản lý mệnh đề học và chiến lược tự khởi động lại hiệu quả hơn. Bảng kết quả thực nghiệm Minisat, Glueminisat, Glucose trên Slitherlink thể hiện rõ. Bộ dữ liệu thực nghiệm được lấy từ các cuộc thi SAT, đây là bộ dữ liệu lớn và đáng tin cậy.

4.1. Thiết Lập Thực Nghiệm Để So Sánh Hiệu Năng Các SAT Solver

Thiết lập thực nghiệm bao gồm việc lựa chọn các bộ dữ liệu chuẩn từ cuộc thi SAT Competition, xác định các tham số cấu hình cho các SAT Solver, và thiết lập môi trường phần cứng và phần mềm để chạy các thực nghiệm. Các bộ dữ liệu được chọn phải đại diện cho các loại bài toán SAT khác nhau, bao gồm các bài toán ngẫu nhiên, các bài toán từ các ứng dụng thực tế, và các bài toán có cấu trúc đặc biệt. Các tham số cấu hình cho các SAT Solver phải được điều chỉnh cẩn thận để đảm bảo rằng các SAT Solver đang chạy với hiệu suất tốt nhất. Môi trường phần cứng và phần mềm phải được kiểm soát chặt chẽ để đảm bảo rằng các kết quả thực nghiệm là chính xác và có thể tái lập.

4.2. Đánh Giá Kết Quả Thực Nghiệm Trên Bộ Dữ Liệu Chuẩn

Việc đánh giá kết quả thực nghiệm bao gồm việc đo thời gian chạy, số lượng mệnh đề học được tạo ra, số lượng lần khởi động lại, và số lượng xung đột. Các kết quả này được sử dụng để so sánh hiệu suất của các SAT Solver và xác định các yếu tố ảnh hưởng đến hiệu suất. Các kết quả cũng được sử dụng để xác định các điểm mạnh và điểm yếu của các kỹ thuật khác nhau và đề xuất các hướng nghiên cứu trong tương lai. Các kết quả thực nghiệm cho thấy Glueminisat, Glucose trên Aprove 09 có tốc độ nhanh hơn so với Minisat.

4.3. Phân Tích Ưu Điểm và Nhược Điểm Của Từng SAT Solver

Minisat là một SAT Solver đơn giản và hiệu quả, nhưng nó có thể gặp khó khăn trên các bài toán khó. GlueMinisat và Glucose sử dụng các kỹ thuật tiên tiến hơn để cải thiện hiệu suất trên các bài toán khó, nhưng chúng có thể phức tạp hơn và yêu cầu nhiều bộ nhớ hơn. GlueMinisat tập trung vào việc học các mệnh đề học quan trọng, trong khi Glucose tập trung vào việc khởi động lại quá trình tìm kiếm. Việc lựa chọn SAT Solver phù hợp phụ thuộc vào đặc điểm của bài toán cần giải quyết và các tài nguyên có sẵn.

V. Kết Luận Và Hướng Phát Triển Luận Văn Thạc Sĩ SAT Solving

Luận văn đã trình bày một cái nhìn tổng quan về các kỹ thuật SAT Solving cơ bản và tiên tiến. Luận văn đã phân tích chi tiết các thuật toán DPLL và CDCL, cũng như các kỹ thuật quản lý mệnh đề học và chiến lược tự khởi động lại. Các kết quả thực nghiệm đã chứng minh rằng các SAT Solver tiên tiến như GlueMinisat và Glucose có hiệu suất tốt hơn Minisat trên các bài toán khó. Hướng phát triển trong tương lai có thể tập trung vào việc cải thiện các kỹ thuật quản lý mệnh đề học, phát triển các chiến lược tự khởi động lại thông minh hơn, và khám phá các ứng dụng mới của SAT Solving trong các lĩnh vực khác nhau.

5.1. Tóm Tắt Các Kết Quả Nghiên Cứu Chính Đạt Được

Luận văn đã đạt được các kết quả nghiên cứu chính sau: Trình bày một cái nhìn tổng quan về các kỹ thuật SAT Solving cơ bản và tiên tiến. Phân tích chi tiết các thuật toán DPLL và CDCL. Đánh giá hiệu suất của các SAT Solver khác nhau trên các bộ dữ liệu chuẩn. Đề xuất các hướng nghiên cứu trong tương lai. Luận văn này góp phần vào sự hiểu biết sâu sắc hơn về các kỹ thuật SAT Solving và cung cấp một nền tảng cho các nghiên cứu trong tương lai.

5.2. Các Vấn Đề Còn Tồn Đọng Và Hướng Giải Quyết

Một số vấn đề còn tồn đọng và hướng giải quyết trong tương lai bao gồm: Làm thế nào để cải thiện các kỹ thuật quản lý mệnh đề học? Làm thế nào để phát triển các chiến lược tự khởi động lại thông minh hơn? Làm thế nào để khám phá các ứng dụng mới của SAT Solving trong các lĩnh vực khác nhau? Các nghiên cứu trong tương lai có thể tập trung vào việc giải quyết các vấn đề này để cải thiện hiệu suất và khả năng ứng dụng của SAT Solving.

5.3. Triển Vọng Ứng Dụng Của SAT Solving Trong Tương Lai

SAT Solving có triển vọng ứng dụng rộng rãi trong tương lai, đặc biệt là trong các lĩnh vực như trí tuệ nhân tạo, kiểm chứng phần cứng và phần mềm, lập kế hoạch, và tối ưu hóa. Với sự phát triển của các kỹ thuật SAT Solving mới và các công cụ phần cứng mạnh mẽ hơn, SAT Solving có thể được sử dụng để giải quyết các bài toán phức tạp hơn và có quy mô lớn hơn. Đồng thời, SAT Solving có thể được tích hợp với các kỹ thuật khác, chẳng hạn như học máy, để tạo ra các hệ thống thông minh hơn. Các kỹ thuật tiên tiến đang được sử dụng và phát triển, hứa hẹn nhiều ứng dụng thực tiễn trong tương lai.

Trích đoạn nội dung tài liệu

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ ĐẶNG THỊ NHƢ HOA CÁC KỸ THUẬT SAT SOLVING LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 2016 TIEU LUAN MOI download : [e-mail] ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ ĐẶNG THỊ NHƢ HOA CÁC KỸ THUẬT SAT SOLVING Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: TS. TÔ VĂN KHÁNH Hà Nội - 2016 TIEU LUAN MOI download : [e-mail] LỜI CẢM ƠN Luận văn Thạc sĩ này đƣợc thực hiện tại Trƣờng Đại học Công nghệ - Đại học Quốc gia Hà Nội dƣới sự hƣớng dẫn của TS. Tô Văn Khánh. Xin đƣợc gửi lời cảm ơn sâu sắc đến Thầy về định hƣớng khoa học, liên tục quan tâm, tạo điều kiện thuận lợi trong suốt quá trình nghiên cứu hoàn thành luận văn này.

Tôi xin đƣợc gửi lời cảm ơn đến các thầy, cô trong Bộ môn Công nghệ phần mềm cũng nhƣ Khoa Công nghệ Thông tin đã mang lại cho tôi những kiến thức vô cùng quý giá và bổ ích trong quá trình theo học tại trƣờng. Tôi cũng xin chân thành cảm ơn đến gia đình, bạn bè đã quan tâm và động viên giúp tôi có thêm nghị lực, cố gắng để hoàn thành luận văn này. Do thời gian và kiến thức có hạn nên luận văn chắc chắn không tránh khỏi những thiếu sót nhất định. Tôi rất mong nhận đƣợc những sự góp ý quý báu của thầy cô, đồng nghiệp và bạn bè.

Hà Nội, tháng 12 năm 2016 Học viên Đặng Thị Nhƣ Hoa TIEU LUAN MOI download : [e-mail] LỜI CAM ĐOAN Tôi xin cam đoan luận văn “Các kỹ thuật SAT Solving” là công trình nghiên cứu của cá nhân tôi dƣới sự hƣớng dẫn của TS. Tô Văn Khánh, trung thực và không sao chép của tác giả khác. Trong toàn bộ nội dung nghiên cứu của luận văn, các vấn đề đƣợc trình bày đều là những tìm hiểu và nghiên cứu của chính cá nhân tôi hoặc là đƣợc trích dẫn từ các nguồn tài liệu có ghi tham khảo rõ ràng, hợp pháp. Tôi xin chịu mọi trách nhiệm cho lời cam đoan này.

Hà Nội, tháng 12 năm 2016 Học viên Đặng Thị Nhƣ Hoa TIEU LUAN MOI download : [e-mail] TÓM TẮT SAT Solving là bài toán chứng minh sự thỏa mãn (SAT / UNSAT) của một công thức Lôgic mệnh đề (Propositional Lôgic) và các công cụ tự động SAT Solver đóng vai trò là các bộ giải công thức đó. Ngày nay các SAT Solver cũng đóng vai trò là các công cụ nền cho các SMT (SAT Module Theories) Solver, những công cụ tự động chứng minh sự thỏa mãn hay không thỏa mãn (SAT/UNSAT) của các công thức lôgic trên lý thuyết vị từ cấp I (FOL I). Các nghiên cứu về SMT Solver hiện nay đang là các chủ đề có tính thời sự, bởi SMT Solver đƣợc ứng dụng trong các bài toán về kiểm chứng, kiểm thử chƣơng trình. Bài toán SAT là bài toán có độ phức NP và các kỹ thuật SAT Solving đã đƣợc nghiên cứu, phát triển đã lâu.

Tuy nhiên, sự phát triển mạnh mẽ của các SAT solver trong những năm gần đây thông qua các cuộc thi SAT Competition tổ chức hàng năm cho thấy nhiều kỹ thuật cải tiến trong cài đặt các SAT solver đã đƣợc tiến hành thực nghiêm. Ngày nay các SAT solver có khả năng giải quyết các công thức lên đến hàng triệu biến với hàng trăm ngàn mệnh đề. Luận văn đi sâu tìm hiểu các kỹ thuật cơ bản, các thuật toán cơ bản đƣợc cài đặt trong các SAT solver, đồng thời đƣa ra các ví dụ minh họa cụ thể nhằm làm rõ cách thức hoạt động. Các kỹ thuật này đƣợc cài đặt trong một SAT solver phổ biến hiện nay đó là MiniSAT, một SAT solver mã nguồn mở mà rất nhiều SAT solver mạnh trên thế giới đƣợc mở rộng cải tiến từ SAT Solver này.

Bên cạnh đó, luận văn cũng tìm hiểu 2 kĩ thuật tiên tiến đang đƣợc cài đặt trong các SAT Solver mạnh hiện nay là GlueMinisat, Glucose. Luận văn tiến hành chạy thực nghiệm so sánh 3 SAT solver này trên các bộ dữ liệu thực nghiệm chuẩn (từ cuộc thi SAT competition) để thấy rõ tính hiệu quả, tính nhanh nhạy của các kỹ thuật tiên tiến đang đƣợc sử dụng. Nội dung luận văn này đƣợc chia thành 4 chƣơng nhƣ sau: - Chƣơng 1 sẽ đƣợc giới thiệu về các vấn đề cơ bản nhƣ Lôgic mệnh đề, bài toán SAT, các SAT Solver và ứng dụng của phƣơng pháp SAT Encoding. - Chƣơng 2 sẽ trình các kỹ thuật SAT solving cơ bản bao gồm thủ tục DPLL, và các kỹ thuật áp dụng trong DPLL nhƣ: CDCL, Back Jumping, 2 Watched literals, Clause Elimination.

- Chƣơng 3 trình bày các kỹ thuật SAT Solving tiên tiến hiện nay, những kỹ thuật đang đƣợc cài đặt trong các SAT solver mạnh trên thế giới nhƣ GlueMinisat, Glucose. - Chƣơng 4 tiến hành thực nghiệm so sánh và đánh giá 3 SAT Solver trên bộ dữ liệu chuẩn của cuộc thi SAT competition hàng năm. TIEU LUAN MOI download : [e-mail] MỤC LỤC LỜI CẢM ƠN. LỜI CAM ĐOAN.

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Ẽ. Bài toán SAT.

Công thức Lôgic mệnh đề. Chuẩn tắc hội CNF. Phƣơng pháp SAT Encoding. Trò chơi Hitori.

Trò chơi Sodoku. Trò chơi Slitherlink. Một số ứng dụng khác của SAT. CÁC KỸ THUẬT SAT SOLVING CƠ BẢN.

Thủ tục DPLL truyền thống. Một số khái niệm cơ bản. Các luật cơ bản của thủ tục DPLL. Thủ tục DPLL hiện đại.

Learn và Forget. Thuật toán CDCL. Nội dung chính của CDCL. Giải thuật CDCL.

Suy diễn mệnh đề và mức quay lui .27 TIEU LUAN MOI download : skknchat@gmail. Biểu đồ kéo theo. Học từ mệnh đề xung đột. Kỹ thuật Two -Watched literals.

Two- Watched literal. Giải pháp loại bỏ biến và loại bỏ mệnh đề. Loại bỏ biến. Loại bỏ mệnh đề.

CÁC KỸ THUẬT SAT SOLVING TIÊN TIẾN HIỆN NAY. Tiêu chí đánh giá Learn Clause. Chiến lƣợc tự khởi động lại. Quản lý mệnh đề học.

Khởi động lại. Giới thiệu về MiniSat. Giao diện lập trình ứng dụng. Tổng quan về Minisat.

Biên dịch Minisat. Biên dịch GlueMinisat. Biên dịch Glucose. Bộ dữ liệu thực nghiệm .56 TÀI LIỆU THAM KHẢO .56 TIEU LUAN MOI download : [e-mail] BẢNG CÁC THUẬT NGỮ VÀ TỪ VIẾT TẮT STT Thuật ngữ Từ viết tắt / Diễn giải 1 SAT Satisfiability 2 UNSAT Unsatisfiability Một công cụ chứng minh tự động các công 3 SAT Solver thức Lôgic mệnh đề 4 CNF Conjunctive Normal Form 5 BCP Boolean Constraint Propagation 6 DPLL Davis–Putnam–Logemann–Loveland 7 CDCL Conflict Driven Clause Learning 8 UIP Unique Implication Point 9 LBD Literal Blocks Distance TIEU LUAN MOI download : [e-mail] DANH MỤC CÁC BẢNG BIỂU Bảng 4.1: Kết quả thực nghiệm Minisat, Glueminisat, Glucose trên Slitherlink .2: Kết quả thực nghiệm Minisat, Glueminisat, Glucose trên Aprove 09 .53 TIEU LUAN MOI download : [e-mail] DANH MỤC CÁC HÌNH VẼ Hình 1.1: Trò chơi Logic Hitori .2: Trò chơi Logic Sodoku và lời giải .3: Trò chơi Logic Slitherlink và lời giải .4: Mã hóa Luật 1 trò chơi Slitherlink .5: Mã hóa Luật 2 của Slitherlink .1: Đồ thị xung đột để tìm backjump clause .2: Một phần của đồ thị suy diễn quyết định mức 6, thỏa mãn các mệnh đề trong ví dụ, sau khi quyết định x1=1(trái).

Đồ thị tƣơng tự sau khi học đƣợc xung đột từ mệnh đề C9 = (x5 V ⌐x1) và quay trở lại mức quyết định 3(phải) .3: Ví dụ về đồ thị xung đột với 2 UIPs .4: Đồ thị suy diễn của ví dụ 2. UIP đầu tiên là x4 và tƣơng ứng với các khẳng định literal là ⌐x4 .5: Quá trình minh họa sử dụng Binary Resolution để đƣa ra mệnh đề Backjump Clause .6: Ví dụ về biểu đồ kéo theo .7: Xây dựng biểu đồ kéo theo .8: Xác định mệnh đề xung đột .9: Tìm kiếm các biến suy diễn lần 1 .10: Tìm kiếm các biến suy diễn lần 2 .11: Tìm kiếm các suy diễn lần 3 .12: Tìm kiếm các biến suy diễn lần 4 .13: Kết luận mệnh đề học đƣợc và trả về mức quyết định backtrack .14: BCP sử dụng 2 watched literals. 1: Giao diện ứng dụng của Minisat .2: Kết quả thực nghiệm trên Slithelink.3: Kết quả thực nghiệm thời gian chạy trên Aprove09 .54 TIEU LUAN MOI download : [e-mail] 1 CHƢƠNG 1. Bài toán SAT Bài toán SAT là một bài toán trong khoa học máy tính nhằm kiểm tra tính thỏa mãn (SAT - Satisfiability) hay không thỏa mãn (UNSAT – Unsatisfiability) của một công thức Lôgic mệnh đề.

Bài toán SAT là bài toán đƣợc chứng minh thuộc lớp NP - đầy đủ (NP - Complete), các bài toán khác muốn chứng minh thuộc lớp NP – đầy đủ có thể giản lƣợc vấn đề về bài toán SAT. Một công thức Lôgic mệnh đề là SAT khi tồn tại một bộ giá trị true hoặc false trên các biến Lôgic mệnh đề làm cho công thức nhận giá trị true. Ngƣợc lại công thức đó là UNSAT khi và chỉ khi mọi bộ giá trị true hoặc false của biến Lôgic mệnh đề luôn làm cho công thức có giá trị là false.1: Ví dụ về công thức SAT: Cho công thức Lôgic mệnh đề: F = (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ x3) trong đó x1, x2, x3 là các biến Lôgic mệnh đề. Công thức F là SAT vì với bộ giá trị x1 = true, x2 = false và x3 = true thì F cho kết quả true.2: Ví dụ về công thức UNSAT: Cho công thức Lôgic mệnh đề: F = (¬x1∨ x1 ∨ ¬x2) ∧ (x1 ∨¬ x3) ∧ (x1 ∨ x2) trong đó x1, x2, x3 là các biến Lôgic mệnh đề.

Công thức F là UNSAT vì với mọi bộ giá trị thì F luôn cho kết quả false. Lôgic mệnh đề Đầu vào của bài toán SAT là một công thức Lôgic mệnh đề thƣờng đƣợc biểu diễn dƣới dạng chuẩn tắc hội (CNF) hoặc chuẩn tắc tuyển (DNF). Dƣới đây sẽ định nghĩa một công thức Lôgic mệnh đề và các dạng chuẩn tắc tƣơng ứng. Công thức Lôgic mệnh đề Một công thức Lôgic mệnh đề đƣợc xây dựng từ các biến và các phép toán lôgic bao gồm: AND (phép hội), OR (phép tuyển), NOT (phủ định), IMPLICATION (phép kéo theo).

Dƣới đây là các khái niệm cơ bản [1]: a. Mệnh đề Định nghĩa: Mỗi câu được phát biểu là đúng hay sai được gọi là một mệnh đề. Các phép toán trên mệnh đề bao gồm:  Phép phủ định (  ) TIEU LUAN MOI download : skknchat@gmail.