Luận văn Thạc sĩ Công nghệ thông tin: Các kỹ thuật SAT solving

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, 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, 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.
Nội dung trích xuất từ tài liệu:
Luận văn Thạc sĩ Công nghệ thông tin: Các kỹ thuật SAT solvingĐẠI HỌC QUỐC GIA HÀ NỘITRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẶNG THỊ NHƯ HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINHà Nội - 2016ĐẠI HỌC QUỐC GIA HÀ NỘITRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẶNG THỊ NHƯ HOACÁC KỸ THUẬT SAT SOLVINGNgành: Công nghệ thông tinChuyên ngành: Kỹ thuật phần mềmMã số: 60480103LUẬN VĂN THẠC SĨ NGÀNH CÔNG NGHỆ THÔNG TINNGƯỜI HƯỚNG DẪN KHOA HỌC: TS. TÔ VĂN KHÁNHHà Nội - 2016LỜI CẢM ƠNLuậ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ọcQuố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ậnlợ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ờicảm ơn đến các thầy, cô trong Bộ môn Công nghệ phần mềm cũng như Khoa Côngnghệ Thông tin đã mang lại cho tôi những kiến thức vô cùng quý giá và bổ ích trongquá 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êngiú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ữngthiế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ô, đồngnghiệp và bạn bè.Hà Nội, tháng 12 năm 2016Học viênĐặng Thị Như HoaLỜI CAM ĐOANTôi xin cam đoan luận văn “Các kỹ thuật SAT Solving” là công trình nghiêncứ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ôngsao 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à đượctrí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 2016Học viênĐặng Thị Như HoaTÓM TẮTSAT Solving là bài toán chứng minh sự thỏa mãn (SAT / UNSAT) của một côngthức Lôgic mệnh đề (Propositional Lôgic) và các công cụ tự động SAT Solver đóngvai 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áccông cụ nền cho các SMT (SAT Module Theories) Solver, những công cụ tự độngchứ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ôgictrê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ácchủ đề có tính thời sự, bởi SMT Solver được ứng dụng trong các bài toán về kiểmchứ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 đã đượcnghiê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 solvertrong những năm gần đây thông qua các cuộc thi SAT Competition tổ chức hàng nămcho 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ựcnghiê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àngtriệ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 đặttrong các SAT solver, đồng thời đưa ra các ví dụ minh họa cụ thể nhằm làm rõ cáchthứ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 2kĩ 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 solvernà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ánSAT, 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 Watchedliterals, 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. ...