(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
➤ Gửi thông báo lỗi ⚠️ Báo cáo tài liệu vi phạmNội dung chi tiết: (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
ĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01 GIA HA NỘI TRƯỜNG DẠI HỌC CÔNG NGHỆDẠNG 111Ị NHL HOACÁC KỸ THUẬT SAT SOLVINGNgành: Công nghệ thông tin Chuyên ngành: Kỳ thuật phan mềm Mã SỔ: 60480103Ll Ậ.N VÃN THẠC sì NGÀNH CÔNG NGHỆ ỉ HÔNG TIN • • •NGƯỜI HƯỞNG DẤN KHOA HỌC: IS. 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 (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01 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 cua TS. Tò Vãn Khánh. Xin được gưi lời cam ơn sâu sắc đến Thầy về đinh hướng(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
khoa học. liên tục quan tâm. tạo điều kiện thuận lợi trong suốt quá trinh nghiên cứu hoàn thành luận văn này. Tòi xin được gửi lời cam ơn đến các thầĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01theo học tại trường.Tôi cùng xin chân thành cam ơ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 chac chan không tránh khỏi nhừng thiếu sót nhất đinh. Tôi rất mong nhận được nhùng sự góp ý quv (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01 báu cua thầy cô. đồng nghiệp và bạn bè.Hà Nội. tháng 12 nâm 2016Học viênĐặng Thị Như HoaLÕI CAM i)OAN'l ôi xin cam đoan luận vân “Các kỳ thuật SAT So(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
lving” là công trình nghiên cứu của cá nhàn lôi dưới sự hưởng dan cùa TS. Tô Vãn Khánh, trung thực và không sao chép cua tác già khác. Trong toàn bộ nĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01ồn tài liệu có ghi tham khao rõ ràng, hợp pháp.Tôi xin chịu mọi trách nhiệm cho lời cam doan nãy.Ilà 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òng thức Logic mệnh đề (Propositional Logic) và các công cụ tự đông SAT Solv (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01er đóng vai trò là các bô giai 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ù(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
ng còng cụ tự động chứng minh sự thoa màn hay không thòa màn (SAT/ƯNSAT) cua các công thức logic trên lý thuyết vị từ cấp I (FOL I). Các nghiên cửu vềĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01 SAT lã bãi toán có độ phức NP và các kỳ thuật SAT Solving dà được nghiên cứu. phát triển đà Lâu Tuy nhiên, sư phát triên mạnh mè cua 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 cai tiến trong cài đặt các SAT solver đà được t (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01iến hành thực nghiêm Ngày nay các SAT solver có khà nãng giai 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(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
im hiểu các kỳ thuật cơ bân. các thuật toán cơ băn dược cãi đặt trong các SAT solver, đồng thời đưa ra các vi dụ minh hoa cụ thể nhẩm làm rò cách thứcĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01nh 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 tim 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 (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01 thi SAT competition) đê thay rõ tính hiệu qua. tinh nhanh nhạy cua các kỳ thuật tiên tiến đang được sư dungNội dung luận văn này được chia thành 4 ch(LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01
ương như sau:-Chương 1 sè dược giới thiệu về các van đê cơ bân như Logic mệnh đề. bài toán SAT. các SAT Solver và ứng dụng cùa phương pháp SAT EncodinĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01rals. Clause Elimination.■Chương 3 trinh bày các kỳ thuật SA T Solving tiên tiến hiện nay. nhưng kỳ thuật đang được cài dặt trong các SAT solver mạnh trên the 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 competi (LUẬN văn THẠC sĩ) các kỹ thuật SAT solving luận văn ths máy tính 60 48 01tion háng năm.ĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎC ĐẠI HỌC QƯÓC GIA HÀ NÓI TRƯỜNG ĐẠI HỌC CÔNG NGHỆĐẢNG THỊ NHI'HOACÁC KỸ THUẬT SAT SOLVINGLUẬN VĂN THẠC sĩ CÔNG NGHỆ THÔNG TINHà Nội - 2016DẠI HỌC QVỎCGọi ngay
Chat zalo
Facebook