Luận văn: Các Kỹ Thuật SAT Solving

CÁC KỸ THUẬT SAT SOLVING

Tác giả: Đặng Thị Như Hoa

Lĩnh vực: Công nghệ thông tin

Nội dung tài liệu:

Luận văn này tập trung vào bài toán SAT (Satisfiability) và các công cụ tự động giải quyết bài toán này, gọi là SAT Solver. SAT Solver đóng vai trò là nền tảng cho SMT Solver, một công cụ tự động chứng minh sự thỏa mãn hay không thỏa mãn các công thức logic trên lý thuyết vị từ cấp I. Nghiên cứu về SMT Solver có tính thời sự cao do ứng dụng trong việc kiểm chứng và kiểm thử chương trình.

Bài toán SAT là một bài toán phức tạp thuộc lớp NP, đã được nghiên cứu và phát triển lâu đời. 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, được thể hiện qua các cuộc thi SAT Competition, cho thấy sự cải tiến liên tục trong việc cài đặt các thuật toán. Các SAT Solver hiện nay có khả năng giải quyết các công thức với hàng triệu biến và hàng trăm nghìn mệnh đề.

Luận văn đi sâu vào các kỹ thuật cơ bản và thuật toán được cài đặt trong các SAT Solver, minh họa bằng ví dụ cụ thể. Đặc biệt, nghiên cứu tập trung vào MiniSAT, một SAT Solver mã nguồn mở phổ biến, làm nền tảng cho nhiều SAT Solver mạnh mẽ khác. Ngoài ra, luận văn còn khám phá hai kỹ thuật tiên tiến là GlueMinisat và Glucose, được áp dụng trong các SAT Solver hiện đại. Cuối cùng, luận văn tiến hành thực nghiệm so sánh ba SAT Solver này trên các bộ dữ liệu chuẩn từ cuộc thi SAT Competition để đánh giá hiệu quả và tính nhanh nhạy của các kỹ thuật tiên tiến.

Mục lục chi tiết:

• 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
• Chương 2. Các kỹ thuật SAT Solving cơ bản
• Chương 3. Các kỹ thuật SAT Solving tiên tiến hiện nay
• Chương 4. Thực nghiệm
• Kết luận
• Tài liệu tham khảo