Xem trước tài liệu

Đang tải tài liệu...

Thông tin chi tiết tài liệu

Định dạng: PDF
Số trang: 65 trang
Dung lượng: 845 KB

Giới thiệu nội dung

Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính

Tác giả: Nguyễn Văn Quân

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 nghiên cứu các kỹ thuật giải ràng buộc phi tuyến tính bằng phương pháp tính toán xấp xỉ. Cụ thể, luận văn nghiên cứu các phương pháp tính toán khoảng để giải ràng buộc phi tuyến tính, đồng thời đề xuất áp dụng phương pháp kiểm thử cặp đôi vào SMT Solver raSAT, cho kết quả cải tiến đáng kể hiệu quả của raSAT.

Mục lục chi tiết:

  • Lời cam đoan
  • Lời cảm ơn
  • Bảng các ký hiệu và chữ viết tắt
  • Danh mục hình vẽ
  • Danh mục bảng
  • Mở đầu
  • Chương 1. Giới thiệu
    • 1.1. Giải các ràng buộc đa thức
    • 1.2. Ứng dụng của giải các ràng buộc đa thức
    • 1.3. Các SMT giải ràng buộc toán học
  • Chương 2. Phương pháp tính toán khoảng
    • 2.1. Giới thiệu về phương pháp tính toán khoảng
    • 2.2. Phương pháp tính toán khoảng CI
    • 2.3. Phương pháp tính toán khoảng Affine Interval
      • 2.3.1. Dạng AF
      • 2.3.2. Dạng AF1
      • 2.3.2. Dạng AF2
    • 2.4. Phương pháp tính toán khoảng C AI
  • Chương 3. SMT Solver và SMT Solver raSAT
    • 3.1. SAT Solver
    • 3.2. SMT Solver
    • 3.3. Thủ tục DPLL
      • 3.3.1 Thủ tục DPLL cho SAT
      • 3.3.1 Thủ tục DPLL cho SMT
    • 3.4. SMT Solver raSAT
  • Chương 4. Cải tiến kỹ thuật kiểm thử trên SMT Solver raSAT
    • 4.1. Kiểm thử trên raSAT
    • 4.2. Kiểm thử cặp đôi
    • 4.3 Kiểm thử cặp đôi trên raSAT
    • 4.4 Thực nghiệm
      • 4.4.1 Kết quả raSAT tại các cuộc thi SMT – COMP
      • 4.4.2 raSAT 0.2
      • 4.4.3 Benchmarks
      • 4.4.4 Kết quả thực nghiệm
  • Kết luận
  • Tài liệu tham khảo