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. | ĐẠ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 ĐẠ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 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 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 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ò
