Luận văn Thạc sĩ Công nghệ thông tin: Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính

Mục tiêu nghiên cứu của đề tài "Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính" là đề xuất áp dụng phương pháp kiểm thử cặp đôi vào SMT Solver raSAT và đã cho kết quả cải tiến đáng kể hiệu quả của raSAT.
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: Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN QUÂNPHƯƠNG PHÁP TÍNH TOÁN KHOẢNG GIẢI CÁC RÀNG BUỘC KHÔNG TUYẾN TÍNH 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Ệ NGUYỄN VĂN QUÂNPHƯƠNG PHÁP TÍNH TOÁN KHOẢNG GIẢI CÁC RÀNG BUỘC KHÔNG TUYẾN TÍNH 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Ĩ 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 CAM ĐOAN Tôi xin cam đoan rằng, luận văn thạc sĩ công nghệ thông tin “Phươngpháp tính toán khoảng giải các ràng buộc không tuyến tính.” là sản phẩm nghiêncứu của riêng cá nhân tôi dưới sự giúp đỡ rất lớn của Giảng viên hướng dẫn làTS. Tô Văn Khánh, không sao chép lại của người khác. Những điều đã đượctrình bày trong toàn bộ nội dung của luận văn này hoặc là của chính cá nhân tôi,hoặc là được tổng hợp từ nhiều nguồn tài liệu. Tất cả các tài liệu tham khảo đềucó nguồn gốc rõ ràng và được trích dẫn hợp pháp. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quyđịnh cho lời cam đoan của mình. Hà nội, tháng 10 năm 2016 Học viên Nguyễn Văn Quân LỜI CẢM ƠN Trước tiên tôi xin bày tỏ lòng biết ơn chân thành và sâu sắc đến thầy giáo,TS. Tô Văn Khánh - người đã dành nhiều tâm huyết, tận tình chỉ bảo và giúp đỡtôi trong suốt quá trình bắt đầu thực hiện đề tài cho đến khi tôi hoàn thành đề tài. Tôi xin gửi lời cảm ơn chân thành tới các thầy cô giáo khoa Công nghệthông tin, trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội - nơi tôi đãtheo học trong thời gian qua. Các thầy cô đã cung cấp cho tôi những kiến thứcquý báu, tạo điều kiện tốt nhất cho tôi trong suốt quá trình học tập và nghiên cứutại trường. Cuối cùng tôi xin chân thành cảm ơn những người thân trong gia đình,đặc biệt là bố mẹ tôi là nguồn động viên và ủng hộ tôi. Xin cảm ơn bạn bè cùngkhóa, đồng nghiệp trong cơ quan đã giúp đỡ tôi trong quá trình học tập vànghiên cứu thực hiện luận văn này. Tuy rằng, tôi đã cố gắng hết sức trong quá trình làm luận văn nhưngkhông thể tránh khỏi thiếu sót, tôi rất mong nhận được những góp ý của thầy côvà các bạn. Hà nội, tháng 11 năm 2016 Học viên Nguyễn Văn Quân MỤC LỤCLỜI CAM ĐOANLỜI CẢM ƠNBẢNG CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮTDANH MỤC HÌNH VẼDANH MỤC BẢNGMỞ ĐẦU .........................................................................................................................1Chương 1. GIỚI THIỆU ...............................................................................................3 1.1. Giải các ràng buộc đa thức ....................................................................................3 1.2. Ứng dụng của giải các ràng buộc đa thức .............................................................4 1.3. Các SMT giải ràng buộc toán học .........................................................................5Chương 2. PHƯƠNG PHÁP TÍNH TOÁN KHOẢNG .............................................7 2.1. Giới thiệu về phương pháp tính toán khoảng ........................................................7 2.2. Phương pháp tính toán khoảng CI ........................................................................8 2.3. Phương pháp tính toán khoảng Affine Interval...................................................10 2.3.1. Dạng AF ...........................................................................................................11 2.3.2. Dạng AF1 .........................................................................................................13 2.3.2. Dạng AF2 .........................................................................................................15 2.4. Phương pháp tính toán khoảng C AI ...................................................................18Chương 3. SMT SOLVER VÀ SMT SOLVER raSAT ...........................................23 3.1. SAT Solver ..........................................................................................................23 3.2. SMT Solver .........................................................................................................24 3.3. Thủ tục DPLL .....................................................................................................26 3.3.1 Thủ tục DPLL cho SAT ....................................................................................26 3.3.1 Thủ tục DPLL cho SMT ...................................................................................30 3.4. SMT Solver raSAT .............................................................................................32Chương 4. CẢI TIẾN KỸ THUẬT KIỂM THỬ TRÊN SMT SOLVER raSAT ..41 4.1. Kiểm thử trên raSAT ...........................................................................................41 4.2. Kiểm thử cặp đôi .................................................................................................45 4.3 Kiểm thử cặp đôi trên raSAT ...............................................................................47 4.4 Thực nghiệm ................................................................................. ...