Luận Văn Xây dựng hệ thống giải bài toán smt hiệu năng cao – phần máy trạm

ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ


Hoàng Thế Tùng
XÂY DỰNG HỆ THỐNG GIẢI BÀI TOÁN SMT HIỆU NĂNG CAO – PHẦN MÁY TRẠM


KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ phần mềm


Cán bộ hướng dẫn: TS. Trương Anh Hoàng
Cán bộ đồng hướng dẫn: TS. Phạm Ngọc Hùng
HÀ NỘI - 2010

Tóm tắt nội dung
Vấn đề giải quyết các bài toán Satisfiability Modulo Theories (SMT) hiện nay
đang được nghiên cứu và phát triển ở nhiều nơi trên thế giới. Cho đến ngày nay, nhiều
trường đại học, tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán
SMT (hay còn gọi là SMT solver). Ví dụ như Z3 của Mcrosoft, yices của SRI, CVC3
của một số trường đại học danh tiếng của Mỹ. hay boolector, openSMT của một số
trường đại học danh tiếng khác Tuy nhiên, mỗi solver có một lợi thế ưu điểm riêng
đối với các dạng khác nhau của bài toán SMT. Vậy vấn đề đặt ra là làm sao để tận
dụng được hết các ưu điểm đó cho từng bài toán.
Để giải quyết vấn đề ấy, nhóm nghiên cứu đã nghiên cứu và xây dựng một hệ
thống giải quyết bài toán SMT trực tuyến, kết hợp nhiều bộ giải khác nhau để đưa ra
được lời giải tối ưu cho từng bài toán SMT.
Trong khuôn khổ khóa luận tốt nghiệp này của cá nhân tôi, tôi đã xây dựng hai
hệ thống con của hệ thống đã nêu trên là hệ thống trên máy khách (users) và trên máy
trạm (sử dụng để gọi các Solver). Hệ thống trên máy khách sẽ đảm nhiệm việc cung
cấp một giao diện lập trình ứng dụng (Application Programming Interface hay API) để
người dùng sử dụng có thể xây dựng bài toán SMT theo chuẩn thư viện SMT (SMTLIB)
và sau đó là gửi bài toán đến máy chủ (server). Hệ thống trên máy trạm sẽ tiếp
nhận bài toán từ máy chủ và gọi các bộ giải để giải quyết bài toán đó và gửi về máy
chủ kết quả.

Mục lục
Chương 1. Mở đầu 1
1.1. Giới thiệu . 1
1.2. Bài toán đặt ra 1
1.3. Cấu trúc nội dung tài liệu . 2
Chương 2. Kiến thức nền tảng 3
2.1. Giới thiệu SMT 3
2.2. Bộ giải SMT (SMT solver) 3
2.3. Thư viện SMT (SMT-LIB) 4
2.3.1. Cấu trúc cơ bản của SMT-LIB . 4
2.3.2. Khuôn dạng của SMT-LIB . 5
Chương 3. Phân tích hệ thống 12
3.1. Mô hình hệ thống . 12
3.2. Mô hình ca sử dụng của hệ thống 13
3.3. Mô hình hoạt động . 15
Chương 4. Phương hướng giải quyết vấn đề 17
4.1. Lựa chọn phương thức kết nối . 17
4.2. Lựa chọn ngôn ngữ lập trình 17
4.3. Xác định dữ liệu đầu vào, đầu ra của hệ thống 17
Chương 5. Mô tả hệ thống 19
5.1. Quy định cách thức giao tiếp với máy chủ 19
5.2. Phần máy khách . 20
5.2.1. Quy định giao tiếp với máy chủ . 20
5.2.2. Các lớp của hệ thống máy khách 21
5.2.2.1. Lớp config . 21
5.2.2.2. Lớp Client: 21
5.2.2.3. Lớp NetSolver . 21
5.2.2.4. Lớp Bench_attribute 22
5.2.2.5. Lớp Formula 22
5.2.2.6. Lớp func_decl 23
5.2.2.7. Lớp pred_decl 24
Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
5.2.2.8. Lớp Term . 24
5.2.2.9. Lớp annotation 24
5.2.2.10. Lớp varDecl 24
5.2.2.11. Lớp fvarDecl . 24
5.2.2.12. Lớp Arith_symb 25
5.2.2.13. Lớp Identifier 25
5.2.2.14. Lớp quant_var . 25
5.3. Phần máy trạm . 26
5.3.1. Cơ chế làm việc của máy trạm . 26
5.3.2. Quy định giao tiếp với máy chủ . 27
5.3.3. Hoạt động của hệ thống máy trạm 28
5.3.4. Các lớp của hệ thống máy trạm 30
5.3.4.1. Biểu đồ lớp của hệ thống . 30
5.3.4.2. Lớp config . 30
5.3.4.3. Lớp sessionID 30
5.3.4.4. Lớp Solver . 31
5.3.4.5. Lớp ReadThread 31
5.3.4.6. Lớp WriteThread . 34
5.4. Tổng kết . 34
Chương 6. Cài đặt và thử nghiệm . 36
6.1. Cài đặt 36
6.2. Bài toán thực nghiệm . 36
6.2.1. Xây dựng bài toán SMT dựa trên các hàm API 36
6.2.2. Thử nghiệm kết nối với máy chủ và toàn hệ thống 37
Hướng phát triển tiếp theo của hệ thống 40