Please use this identifier to cite or link to this item: https://lib.uet.vnu.edu.vn/jspui/handle/123456789/2268
Title: PHƯƠNG PHÁP TÍNH TOÁN KHOẢNG GIẢI CÁC RÀNG BUỘC KHÔNG TUYẾN TÍNH
Authors: Nguyễn Văn, Quân
Issue Date: 11-Jan-2017
Abstract: Luận văn này tập chung vào nghiên cứu phương pháp tính toán khoảng để giải tự động cho các ràng buộc phi tuyến tính, trong đó trình bày các kĩ thuật trong phương pháp tính toán khoảng gồm CI, AF, AF1, AF2, C IA và so sánh hiệu quả của các kĩ thuật tính toán khoảng. SMT Solver raSAT là một SMT Solver cho phép giải tự động các ràng buộc toán học trên tập số thực và số nguyên bằng phương pháp tính xấp xỉ trên sử dụng các kĩ thuật tính toán khoảng (Interval Arithmetic) và kiểm thử dựa trên lý thuyết xấp xỉ dưới. Chúng tôi đề xuất áp dụng kĩ thuật kiểm thử đôi một vào bước kiểm thử của SMT Solver raSAT. Kiểm thử đôi một cho phép SMT Solver raSAT chọn nhiều giá trị cho mỗi biến để tạo ra bộ ca kiểm thử không quá lớn. Sau khi cài đặt và thực nghiệm, kết quả đạt được cho thấy phương pháp đề ra tốt hơn cả về số lượng bài toán giải được và thời gian giải các ràng buộc. raSAT thực nghiệm trên bộ các ràng buộc “SMT- LIB 2015 - 06-01” với timeout là 2500s , bộ vi xử lý Intel Xeon E5-4655v3 , ram 8GB .
URI: https://lib.uet.vnu.edu.vn/jspui/handle/123456789/2268
Appears in Collections:Khóa luận Khoa Công nghệ thông tin

Files in This Item:
File Description SizeFormat 
NguyenVanQuan_K20_KTPM.pdf1.47 MBAdobe PDFView/Open
NguyenVanQuan_TomTatLuanVan.pdf917.44 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.