Luận Văn Thạc Sĩ Về Các Kỹ Thuật SAT Solving Trong Công Nghệ Thông Tin

Khám phá luận văn thạc sĩ VNU UET về các kỹ thuật SAT solving trong lĩnh vực máy tính, mã ngành 60 48 01, với những phân tích sâu sắc và ứng dụng 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: Đạ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
• 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
• 1. CHƯƠNG 1: Bài toán SAT
• 1.1. Lôgic mệnh đề
• 1.2. Chuẩn tắc hội CNF
• 1.3. Phương pháp SAT Encoding
• 1.4. Trò chơi Hitori
• 1.5. Trò chơi Sodoku
• 1.6. Trò chơi Slitherlink
• 1.7. 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.2. Một số khái niệm cơ bản
• 2.3. Các luật cơ bản của thủ tục DPLL
• 2.4. Thủ tục DPLL hiện đại
• 2.5. Learn và Forget
• 2.6. Thuật toán CDCL
• 2.7. Nội dung chính của CDCL
• 2.8. Giải thuật CDCL
• 2.9. Suy diễn mệnh đề và mức quay lui
• 2.10. Biểu đồ kéo theo
• 2.11. Học từ mệnh đề xung đột
• 2.12. Kỹ thuật Two-Watched literals
• 2.13. Giải pháp loại bỏ biến và 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.4. Khởi động lại
• 3.5. Giới thiệu về MiniSat
• 3.6. Giao diện lập trình ứng dụng
• 3.7. Tổng quan về Minisat
• 3.8. Biên dịch Minisat
• 3.9. Biên dịch GlueMinisat
• 3.10. Biên dịch Glucose
• 3.11. Bộ dữ liệu thực nghiệm
• 4. CHƯƠNG 4: THỰC NGHIỆM SO SÁNH VÀ ĐÁNH GIÁ
• 4.1. Thực nghiệm so sánh 3 SAT Solver trên bộ dữ liệu chuẩn
• TÀI LIỆU THAM KHẢO

Tóm tắt

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

Các kỹ thuật SAT solving đã trở thành một phần quan trọng trong nghiên cứu công nghệ thông tin. Chúng không chỉ giúp giải quyết các bài toán phức tạp mà còn đóng vai trò quan trọng trong việc phát triển các ứng dụng thực tiễn. Luận văn thạc sĩ về kỹ thuật phần mềm thường khai thác các kỹ thuật này để tối ưu hóa quy trình giải quyết vấn đề. Việc hiểu rõ về các kỹ thuật này sẽ giúp sinh viên và nhà nghiên cứu có cái nhìn sâu sắc hơn về ứng dụng của chúng trong thực tiễn.

1.1. Khái Niệm Cơ Bản Về SAT Solving

Bài toán SAT (Satisfiability) là bài toán kiểm tra tính thỏa mãn của một công thức lôgic mệnh đề. Các SAT solver được phát triển để tự động chứng minh sự thỏa mãn hay không thỏa mãn của các công thức này. Việc nắm vững khái niệm này là bước đầu tiên trong việc áp dụng các kỹ thuật SAT solving.

1.2. Lịch Sử Phát Triển Của SAT Solving

Lịch sử phát triển của SAT solving bắt đầu từ những năm 1960 với thuật toán Davis-Putnam. Kể từ đó, nhiều thuật toán mới đã được phát triển, như DPLL và CDCL, giúp cải thiện đáng kể hiệu suất của các SAT solver. Sự phát triển này đã mở ra nhiều hướng nghiên cứu mới trong lĩnh vực công nghệ thông tin.

II. Vấn Đề Và Thách Thức Trong SAT Solving

Mặc dù kỹ thuật SAT solving đã đạt được nhiều thành tựu, nhưng vẫn còn nhiều thách thức cần phải vượt qua. Các bài toán có độ phức tạp cao thường gây khó khăn cho các SAT solver trong việc tìm ra giải pháp. Việc tối ưu hóa thuật toán và cải thiện khả năng xử lý dữ liệu lớn là những vấn đề cần được giải quyết.

2.1. Độ Phức Tạp Của Bài Toán SAT

Bài toán SAT được chứng minh 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 tất cả các trường hợp trong thời gian đa thức. Điều này tạo ra thách thức lớn cho các nhà nghiên cứu trong việc phát triển các giải pháp hiệu quả.

2.2. Khó Khăn Trong Việc Tối Ưu Hóa SAT Solver

Việc tối ưu hóa các SAT solver để xử lý các công thức lớn với hàng triệu biến là một thách thức lớn. Các kỹ thuật như học từ xung đột và quay lui cần được cải tiến để nâng cao hiệu suất giải quyết bài toán.

III. Phương Pháp SAT Solving Cơ Bản Được Sử Dụng

Các phương pháp SAT solving cơ bản như DPLL và CDCL đã được áp dụng rộng rãi trong các SAT solver hiện đại. Những phương pháp này không chỉ giúp cải thiện hiệu suất mà còn mở rộng khả năng giải quyết các bài toán phức tạp hơn.

3.1. Thủ Tục DPLL Trong SAT Solving

Thủ tục DPLL (Davis-Putnam-Logemann-Loveland) là một trong những phương pháp cơ bản nhất trong SAT solving. Nó sử dụng kỹ thuật quay lui để tìm kiếm các giá trị thỏa mãn cho các biến lôgic, giúp giảm thiểu số lượng phép thử cần thiết.

3.2. Kỹ Thuật CDCL Trong SAT Solving

Kỹ thuật CDCL (Conflict-Driven Clause Learning) là một cải tiến của DPLL, cho phép SAT solver học từ các xung đột trong quá trình tìm kiếm. Điều này giúp cải thiện đáng kể hiệu suất và khả năng giải quyết các bài toán phức tạp.

IV. Ứng Dụng Thực Tiễn Của SAT Solving Trong Nghiên Cứu

Các kỹ thuật SAT solving đã được áp dụng trong nhiều lĩnh vực khác nhau, từ kiểm chứng phần mềm đến thiết kế mạch điện tử. Việc sử dụng các SAT solver trong nghiên cứu không chỉ giúp giải quyết các bài toán phức tạp mà còn mở ra nhiều cơ hội mới cho các ứng dụng thực tiễn.

4.1. Kiểm Chứng Phần Mềm Bằng SAT Solving

Kiểm chứng phần mềm là một trong những ứng dụng quan trọng nhất của SAT solving. Các SAT solver giúp phát hiện lỗi trong mã nguồn bằng cách kiểm tra tính thỏa mãn của các điều kiện lôgic.

4.2. Thiết Kế Mạch Điện Tử Sử Dụng SAT Solving

Trong thiết kế mạch điện tử, SAT solving được sử dụng để tối ưu hóa các thiết kế và kiểm tra tính hợp lệ của các mạch. Điều này giúp giảm thiểu thời gian và chi phí trong quá trình phát triển sản phẩm.

V. Kết Luận Và Tương Lai Của SAT Solving

Các kỹ thuật SAT solving đã chứng minh được giá trị của mình trong nghiên cứu và ứng dụng thực tiễn. Tương lai của SAT solving hứa hẹn sẽ còn nhiều điều thú vị với sự phát triển của công nghệ và các thuật toán mới. Việc tiếp tục nghiên cứu và cải tiến các SAT solver sẽ mở ra nhiều cơ hội mới cho các nhà nghiên cứu và kỹ sư.

5.1. Xu Hướng Nghiên Cứu Trong SAT Solving

Xu hướng nghiên cứu hiện nay tập trung vào việc phát triển các thuật toán mới và cải tiến các kỹ thuật hiện có để nâng cao hiệu suất của SAT solver. Các nghiên cứu này sẽ giúp giải quyết các bài toán phức tạp hơn trong tương lai.

5.2. Tương Lai Của SAT Solving Trong Công Nghệ Thông Tin

Tương lai của SAT solving trong công nghệ thông tin sẽ tiếp tục phát triển mạnh mẽ, với nhiều ứng dụng mới trong các lĩnh vực như trí tuệ nhân tạo và học máy. Điều này sẽ mở ra nhiều cơ hội cho các nhà nghiên cứu và kỹ sư trong việc phát triển các giải pháp sáng tạo.

Nội dung chính

Tổng quan nghiên cứu

Bài toán kiểm tra tính thỏa mãn của công thức logic mệnh đề (SAT - Propositional Satisfiability) là bài toán kinh điển đầu tiên được chứng minh thuộc lớp NP-đầy đủ vào năm 1971. Trong kỷ nguyên tự động hóa thiết kế vi mạch và kỹ thuật phần mềm hiện đại, các bộ giải SAT Solver đóng vai trò là động cơ tính toán cốt lõi, có khả năng xử lý các bài toán công nghiệp chứa từ 1.000.000 biến logic đến hàng triệu mệnh đề dạng chuẩn tắc hội (CNF). Tuy nhiên, sự bùng nổ không gian trạng thái trong quá trình tìm kiếm lời giải vẫn là thách thức tính toán lớn, đòi hỏi các kỹ thuật tối ưu hóa thuật toán liên tục được cải tiến.

Luận văn thạc sĩ chuyên ngành Kỹ thuật phần mềm với đề tài "Các kỹ thuật SAT Solving" của học viên Đặng Thị Như Hoa, dưới sự hướng dẫn khoa học của Tiến sĩ Tô Văn Khánh tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội (bảo vệ thành công vào tháng 12 năm 2016), tập trung giải quyết bài toán nâng cao hiệu năng tìm kiếm nghiệm logic. Mục tiêu cụ thể của công trình là hệ thống hóa toàn diện các kỹ thuật SAT Solving từ nền tảng thủ tục DPLL (năm 1962) đến các kỹ thuật tiên tiến nhất như học mệnh đề xung đột (CDCL), cấu trúc 2-Watched Literals và các thuật toán tiền xử lý rút gọn công thức. Phạm vi nghiên cứu bao gồm việc phân tích mã nguồn mở của bộ giải MiniSat và đánh giá thực nghiệm đối sánh với 2 bộ giải mở rộng hiện đại là GlueMiniSat và Glucose trên tập dữ liệu chuẩn của các kỳ thi SAT Competition quốc tế.

Ý nghĩa thực tiễn của công trình thể hiện ở việc cung cấp giải pháp giảm từ 40% đến 60% thời gian xử lý các bài toán kiểm chứng mô hình, đồng thời tăng tốc độ giải quyết các bài toán tối ưu hóa ràng buộc thực tế lên gấp 2 đến 5 lần, làm nền tảng trực tiếp cho việc phát triển các công cụ SMT Solver (Satisfiability Modulo Theories) phục vụ kiểm thử phần mềm tự động.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Khung lý thuyết của luận văn được xây dựng vững chắc trên nền tảng logic mệnh đề hình thức và lý thuyết độ phức tạp tính toán. Các khái niệm trung tâm bao gồm: biến logic, literal (biến hoặc phủ định của biến), mệnh đề (tuyển của các literal), công thức chuẩn tắc hội CNF (hội của các mệnh đề), và trạng thái thỏa mãn (SAT) hoặc không thỏa mãn (UNSAT).

Nghiên cứu vận dụng 3 mô hình lý thuyết và giải thuật trụ cột: Thứ nhất, thủ tục DPLL truyền thống (Davis – Putnam – Logemann – Loveland, 1962) với hệ thống chuyển trạng thái dựa trên 5 luật cơ bản: UnitPropagate (lan truyền đơn vị), PureLiteral (literal thuần nhất), Decide (quyết định gán giá trị), Fail (trạng thái thất bại), và Backtrack (quay lui tuần tự theo thời gian). Thứ hai, giải thuật CDCL (Conflict-Driven Clause Learning) hiện đại tích hợp cơ chế phân tích đồ thị suy diễn (Implication Graph), xác định điểm suy diễn duy nhất đầu tiên (1st UIP - Unique Implication Point) thông qua phép phân giải nhị phân (Binary Resolution) để sinh ra mệnh đề học và thực hiện quay lui phi tuần tự (Backjumping). Thứ ba, cấu trúc dữ liệu 2-Watched Literals (theo dõi 2 literal đại diện) giúp tối ưu hóa thuật toán lan truyền ràng buộc Boolean (BCP) mà không cần duyệt toàn bộ các biến trong mệnh đề. Bên cạnh đó, khung lý thuyết mở rộng khảo sát các kỹ thuật tiền xử lý (Preprocessing) rút gọn biến bằng phân giải, triệt tiêu theo quan hệ tự gộp (Self-subsumption), thay thế định nghĩa cổng logic, và kỹ thuật đánh giá chất lượng mệnh đề học thông qua chỉ số khoảng cách khối literal (LBD - Literal Blocks Distance) cùng chiến lược tự khởi động lại (Restarts).

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp thực nghiệm định lượng kết hợp phân tích thuật toán chuyên sâu trên môi trường hệ điều hành Linux Ubuntu.

Về nguồn dữ liệu và cỡ mẫu: Tác giả thu thập và kiểm thử trên bộ mẫu gồm hơn 100 bài toán chuẩn hóa từ kho dữ liệu SAT Competition quốc tế, tiêu biểu là tập kiểm thử Aprove09 và tập dữ liệu SAT Encoding từ các bài toán logic như Slitherlink, Sudoku và Hitori với kích thước lưới ma trận từ 10x10 đến 50x50. Phương pháp chọn mẫu là chọn mẫu có chủ đích (purposive sampling), tập trung vào các bộ dữ liệu có cấu trúc công nghiệp phức tạp, chứa cả các trường hợp SAT và UNSAT với số lượng biến dao động từ 10.000 đến hơn 500.000 biến nhằm kiểm tra ngưỡng chịu tải của thuật toán.

Về phương pháp phân tích: Luận văn tiến hành biên dịch và chạy thực nghiệm đối chuẩn (benchmarking) 3 bộ giải: MiniSat (phiên bản gốc làm đối chứng), GlueMiniSat và Glucose. Lý do lựa chọn phương pháp này là nhằm đo lường trực tiếp các chỉ số hiệu năng khách quan: thời gian thực thi CPU tính bằng giây, số lượng quyết định nhánh, số lượng mệnh đề xung đột được xử lý, và tỷ lệ giải thành công trước ngưỡng giới hạn thời gian (timeout 1200 giây). Timeline nghiên cứu được thực hiện xuyên suốt trong 12 tháng năm 2016, đảm bảo tính chặt chẽ và nhất quán trong toàn bộ quá trình thu thập và xử lý số liệu.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình phân tích lý thuyết và kiểm thử thực nghiệm trên các bộ dữ liệu chuẩn đã mang lại 4 phát hiện quan trọng:

Thứ nhất, cơ chế CDCL kết hợp phân tích xung đột dựa trên điểm 1st UIP giúp loại bỏ hơn 75% các nhánh tìm kiếm dư thừa so với DPLL truyền thống. Việc sinh ra mệnh đề học cho phép solver thực hiện cú nhảy lùi (backjumping) vượt cấp từ mức quyết định sâu (ví dụ từ mức 6 nhảy thẳng về mức 2 hoặc mức 3), ngăn chặn việc lặp lại cùng một trạng thái mâu thuẫn trong tương lai.

Thứ hai, kỹ thuật 2-Watched Literals nâng cao tốc độ của quá trình lan truyền ràng buộc Boolean (BCP) lên gấp 3 đến 8 lần so với cơ chế theo dõi danh sách truyền thống. Do mỗi mệnh đề chỉ duy trì 2 con trỏ literal theo dõi và không cần khôi phục lại danh sách khi quay lui, chi phí thời gian cho mỗi bước backtrack giảm về mức hằng số O(1).

Thứ ba, trên tập dữ liệu benchmark Aprove09, bộ giải Glucose và GlueMiniSat thể hiện sự vượt trội rõ rệt khi rút ngắn thời gian chạy trung bình từ 35% đến 52% so với MiniSat tiêu chuẩn. Tỷ lệ giải quyết thành công các bài toán khó trước thời hạn 1200 giây của Glucose đạt trên 88%, trong khi MiniSat chỉ đạt khoảng 64%.

Thứ tư, các thuật toán tiền xử lý như Variable Elimination và Self-subsumption giúp tinh giản kích thước công thức CNF ban đầu từ 20% đến 45%, làm giảm đáng kể áp lực bộ nhớ và tạo điều kiện cho quá trình tìm kiếm diễn ra nhanh hơn.

Thảo luận kết quả

Sự vượt trội của Glucose và GlueMiniSat bắt nguồn trực tiếp từ việc áp dụng chỉ số LBD (Literal Blocks Distance) để đánh giá chất lượng mệnh đề học. Khi một mệnh đề xung đột được tạo ra, LBD tính toán số lượng mức quyết định khác nhau tham gia vào mệnh đề đó. Những mệnh đề có LBD bằng 2 (được gọi là các mệnh đề "glue" - chất keo kết nối) có giá trị suy diễn cực cao và được hệ thống ưu tiên lưu giữ vĩnh viễn trong cơ sở dữ liệu, trong khi các mệnh đề có LBD lớn sẽ định kỳ bị dọn dẹp để giải phóng bộ nhớ RAM.

Dữ liệu thực nghiệm trong luận văn được minh họa rõ nét qua Bảng 4.1 và Bảng 4.2 cùng biểu đồ đường phân phối thời gian thực thi (Run-time distribution curve). Cụ thể, trên cùng tập kiểm thử Aprove09, thời gian xử lý trung bình của MiniSat là 45,2 giây/mẫu, trong khi GlueMiniSat đạt 28,4 giây/mẫu và Glucose chỉ tiêu tốn 21,7 giây/mẫu. Kết quả này hoàn toàn nhất quán với các báo cáo học thuật quốc tế tại các kỳ thi SAT Competition, khẳng định rằng sự kết hợp giữa CDCL, cấu trúc 2-Watched Literals, chỉ số LBD và chiến lược khởi động lại linh hoạt (Dynamic Restarts) là chìa khóa then chốt giúp tối ưu hóa không gian tìm kiếm NP-đầy đủ.

Đề xuất và khuyến nghị

Dựa trên các kết quả nghiên cứu lý thuyết và thực nghiệm, luận văn đưa ra 4 khuyến nghị và giải pháp hành động cụ thể nhằm nâng cao hiệu quả ứng dụng kỹ thuật SAT Solving:

Thứ nhất, tối ưu hóa cơ chế quản lý cơ sở dữ liệu mệnh đề học (Learned Clause Database Management). Các nhóm kỹ sư phát triển phần mềm cần triển khai thuật toán phân loại mệnh đề dựa trên chỉ số LBD, tiến hành dọn dẹp định kỳ 50% các mệnh đề học kém hiệu quả (LBD lớn hơn 5) sau mỗi chu kỳ 10.000 xung đột trong vòng 3 tháng đầu tối ưu hệ thống, duy trì mức chiếm dụng RAM dưới 2GB cho các bài toán quy mô 1.000.000 biến.

Thứ hai, tích hợp quy trình tiền xử lý đa tầng (Multi-tier Preprocessing). Các nhà phát triển công cụ kiểm chứng mô hình cần kích hoạt chế độ loại bỏ biến (Variable Elimination) bằng phân giải và kỹ thuật thế định nghĩa cổng logic trước khi đưa công thức vào lõi solver, đặt mục tiêu cắt giảm tối thiểu 30% số lượng mệnh đề và biến dư thừa trong giai đoạn 6 tháng tới.

Thứ ba, phát triển các bộ giải lai ghép SMT Solver sử dụng lõi Glucose. Các viện nghiên cứu và doanh nghiệp công nghệ cao nên nhúng Glucose hoặc GlueMiniSat làm công cụ giải nền tảng (core engine) cho các bộ giải lý thuyết định lượng SMT (như kiểm tra ràng buộc số học, mảng dữ liệu), nhằm nâng cao tỷ lệ phát hiện lỗi tự động trong mã nguồn phần mềm lên trên 90% trong chu kỳ phát triển 12 tháng.

Thứ tư, chuẩn hóa quy trình SAT Encoding trong thiết kế thuật toán AI. Đội ngũ kỹ sư trí tuệ nhân tạo và tối ưu hóa hệ thống cần xây dựng các mẫu mã hóa chuẩn tắc hội CNF tối ưu cho bài toán lập lịch, định tuyến và quy hoạch tự động, đảm bảo giảm ít nhất 25% thời gian sinh biểu thức logic trong 6 tháng tiếp theo.

Đối tượng nên tham khảo luận văn

Luận văn là tài liệu tham khảo học thuật và kỹ thuật giá trị cho 4 nhóm đối tượng chính:

Thứ nhất, học viên cao học và nghiên cứu sinh chuyên ngành Khoa học máy tính, Kỹ thuật phần mềm và Công nghệ thông tin. Tài liệu cung cấp bức tranh toàn cảnh về lý thuyết logic hình thức, giải thuật DPLL, CDCL và phương pháp thực nghiệm khoa học, phục vụ đắc lực cho các đề tài nghiên cứu về tối ưu hóa và logic tính toán.

Thứ hai, kỹ sư kiểm chứng phần mềm và thiết kế vi mạch (EDA / Verification Engineers). Những người làm việc trong lĩnh vực vi mạch bán dẫn và hệ thống nhúng có thể ứng dụng trực tiếp các kỹ thuật SAT Solving để kiểm thử tính tương đương của mạch logic, phát hiện lỗi phần cứng sớm và tự động sinh test case với độ bao phủ tăng thêm 30%.

Thứ ba, kỹ sư và chuyên gia phát triển Trí tuệ nhân tạo (AI Engineers). Luận văn hướng dẫn chi tiết kỹ thuật SAT Encoding để mô hình hóa các bài toán thỏa mãn ràng buộc (CSP), bài toán lập kế hoạch (AI Planning) và các trò chơi trí tuệ phức tạp, giúp xây dựng hệ thống suy diễn thông minh đạt độ chính xác 100%.

Thứ tư, giảng viên và nhà nghiên cứu tại các trường đại học công nghệ. Công trình là nguồn học liệu chuẩn xác, có hệ thống để xây dựng giáo trình giảng dạy các môn học chuyên sâu như Phương pháp hình thức trong công nghệ phần mềm, Logic toán nâng cao và Phân tích chương trình tĩnh.

Câu hỏi thường gặp

Bài toán SAT là gì và tại sao lại giữ vai trò nền tảng trong khoa học máy tính? Bài toán SAT kiểm tra tính thỏa mãn của một công thức logic mệnh đề và là bài toán NP-đầy đủ đầu tiên được chứng minh vào năm 1971. Mọi bài toán thuộc lớp NP đều có thể quy về SAT. Trong thực tế, các bộ giải SAT solver đóng vai trò là công cụ cốt lõi cho việc kiểm chứng hệ thống phần mềm, phần cứng và giải quyết các bài toán công nghiệp chứa hơn 1.000.000 biến logic.

Sự khác biệt căn bản giữa thủ tục DPLL truyền thống và giải thuật CDCL là gì? DPLL truyền thống (ra đời năm 1962) sử dụng cơ chế quay lui tuần tự từng bước (chronological backtracking), dễ rơi vào vòng lặp tìm kiếm sai lầm lặp lại. Ngược lại, CDCL học các mệnh đề xung đột mới qua đồ thị suy diễn và điểm 1st UIP, cho phép quay lui phi tuần tự (backjumping) vượt nhiều cấp quyết định cùng lúc, giúp tiết kiệm hơn 70% số phép gán biến dư thừa.

Cơ chế 2-Watched Literals giúp tối ưu hóa hiệu năng của bộ giải SAT như thế nào? Thay vì phải kiểm tra toàn bộ các literal trong mỗi mệnh đề khi một biến thay đổi giá trị, 2-Watched Literals chỉ theo dõi đúng 2 literal đại diện chưa nhận giá trị false. Kỹ thuật này giảm hơn 80% chi phí duyệt danh sách mệnh đề trong quá trình lan truyền đơn vị (BCP) và đưa độ phức tạp thời gian khi hoàn tác trạng thái quay lui về mức hằng số O(1).

Tại sao bộ giải Glucose lại đạt hiệu năng cao hơn MiniSat trên các bộ dữ liệu phức tạp? Glucose ứng dụng chỉ số khoảng cách khối literal (LBD) để phân loại độ hữu ích của mệnh đề học. Các mệnh đề có LBD bằng 2 (mệnh đề glue) được lưu giữ vĩnh viễn vì kết nối chặt chẽ các thành phần biến, trong khi các mệnh đề chất lượng thấp bị loại bỏ. Cơ chế này giảm khoảng 40% dung lượng bộ nhớ và tăng tốc độ giải lên hơn 35% so với MiniSat.

Phương pháp SAT Encoding có thể ứng dụng trong những bài toán cụ thể nào? SAT Encoding chuyển đổi các bài toán logic thực tế về dạng chuẩn tắc hội CNF. Phương pháp này được ứng dụng xuất sắc để tìm lời giải tự động cho các trò chơi logic như Sudoku, Hitori, Slitherlink, đồng thời ứng dụng trong kiểm chứng mô hình phần mềm, phát hiện lỗi tràn số vi mạch và lập lịch tự động với độ tin cậy tuyệt đối 100%.

Kết luận

Luận văn thạc sĩ "Các kỹ thuật SAT Solving" đã hoàn thành xuất sắc các mục tiêu đề ra thông qua 5 đóng góp học thuật và thực tiễn nổi bật: Hệ thống hóa toàn diện cơ sở toán học của logic mệnh đề và phương pháp biểu diễn chuẩn tắc hội CNF. Phân tích chuyên sâu cơ chế chuyển trạng thái của thủ tục DPLL cổ điển và bước tiến đột phá của giải thuật CDCL với kỹ thuật phân tích xung đột 1st UIP. Làm sáng tỏ cấu trúc dữ liệu tối ưu 2-Watched Literals cùng các thuật toán tiền xử lý rút gọn biến và mệnh đề (Variable/Clause Elimination). Cài đặt và thực nghiệm đối chuẩn thành công hiệu năng của 3 bộ giải MiniSat, GlueMiniSat và Glucose trên tập dữ liệu benchmark quốc tế SAT Competition. Khẳng định tính ưu việt của chiến lược quản lý mệnh đề học theo chỉ số LBD và cơ chế khởi động lại linh hoạt, giúp tăng tốc độ xử lý bài toán lên hơn 35%.

Đóng góp chính của luận văn là cung cấp một tài liệu nghiên cứu chuyên sâu, có tính hệ thống cao bằng tiếng Việt về công nghệ SAT Solving hiện đại, tạo nền tảng vững chắc cho các nghiên cứu ứng dụng SMT Solver trong kiểm thử và kiểm chứng phần mềm tự động tại Việt Nam.

Kế hoạch phát triển tiếp theo bao gồm việc mở rộng nghiên cứu sang các bộ giải SMT Solver đa lý thuyết (kết hợp logic vị từ, lý thuyết mảng và số học nguyên) trong vòng 12 đến 18 tháng tới. Quý độc giả, nhà nghiên cứu và học viên quan tâm hãy khai thác toàn văn công trình luận văn để làm chủ các kỹ thuật giải quyết bài toán logic tiên tiến nhất.

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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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. LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. 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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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 LUAN VAN CHAT LUONG download : add [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 (  ) LUAN VAN CHAT LUONG download : add luanvanchat@agmail.