Đồ Án Xây dựng hệ thống giải bài toán smt hiệu năng cao – phần máy chủ

TÓM TẮT NỘI DUNG Việc giải quyết các bài toán Satisfiability Modulo Theories (SMT) được nghiên cứu rất nhiều trên khắp thế giới. Hiện nay, trên thế giới đã có rất nhiều bộ giải quyết các bài toán (hay còn gọi là Solver) SMT từ một tệp SMT đã được xây dựng trên thế giới, trong đó phải kể đến CVC3, Z3, Yieces, IASolver, SatSolver, Và mỗi Solver đó đều có những đặc trưng và thế mạnh riêng trong mỗi trường hợp của bài toán SMT. Trong nhiều năm qua, bài toán giải quyết bài toán SMT hiệu năng cao đã được xây dựng, đặc biệt nó là đề tài tìm hiểu, nghiên cứu của rất nhiều trường đại học của các nước trên thế giới. Do vậy, việc xây dựng bước đầu của hệ thống giải quyết bài toán SMT hiệu năng cao là điều quan trọng để những người phát triển khác về sau có thể nâng cấp, phát triển hệ thống tốt hơn. Dựa trên những ưu điểm của các Solver, chúng ta xây dựng một hệ thống có cơ chế kết nối các ưu điểm đó của Solver để có thể tìm ra được kết quả cho bài toán SMT một cách nhanh chóng.
Trong khóa luận tốt nghiệp này, một hệ thống giải quyết bài toán SMT hiệu năng cao mã nguồn mở được bước đầu được xây dựng nên. Hi vọng, cùng với những người phát triển khác sau này của hệ thống, trường ta sẽ có một hệ thống giải quyết bài toán SMT tốt hơn, mang tên trường Đại Học Công Nghệ.

MỤC LỤC
CHƯƠNG 1. MỞ ĐẦU 1
1.1.Giới thiệu. 1
1.2.Phát biểu bài toán giải quyết bài toán SMT hiệu năng cao– phía máy chủ. 1
1.3.Kết quả đã đạt được. 2
1.4.Các nội dung chính của luận văn. 2
CHƯƠNG 2. GIỚI THIỆU VỀ SMT, SMT SOLVER 3
2.1.Giới thiệu về SMT 3
2.2.Giới thiệu về SMT Solver. 3
2.3.Các ứng dụng của bài toán SMT 4
CHƯƠNG 3: PHÂN TÍCH HỆ THỐNG VÀ HƯỚNG GIẢI QUYẾT 5
3.1.Phân tích yêu cầu. 5
3.2.Các thành phần của hệ thống. 5
3.3.Cách thức giao tiếp của các thành phần của hệ thống. 7
3.4.Ngôn ngữ lập trình. 10
3.5.Cơ chế phục vụ của Server. 10
CHƯƠNG 4. THIẾT KẾ TỔNG THỂ HỆ THỐNG 17
4.1. Biểu đồ ca sử dụng của hệ thống. 17
4.2.Biểu đồ hoạt động của hệ thống. 18
CHƯƠNG 5. THIẾT KẾ CHI TIẾT SERVER 20
5.1.Biểu đồ lớp của Server. 21
5.2.Lớp tiếp nhận các kết nối - ServerSMT 21
5.3.Lớp quản lý các tiến trình RequestThread. 25
5.4.Lớp chứa danh sách các Request từ người dùng - RequestQueue. 28
5.5.Lớp các quy ước giao tiếp giữa các thành phần - config. 29
5.6.Lớp phiên làm việc - Session. 31
5.7.Lớp thực hiện tương tác với User - RequestHandler. 33
5.8.Lớp tương tác với các Solver - SolverHandler. 34
5.9.Lớp chuyển kết quả từ các Solver về dạng chuẩn - convert 36
5.10.Lớp theo dõi các hoạt động hệ thống - debug. 37
5.11.Lớp thực thi Server - ServerSMTStart 38
5.12.Tổng kết 38
CHƯƠNG 6. CÀI ĐẶT VÀ THỬ NGHIỆM . 39
6.1.Cài đặt 39
6.2.Bài toán thực nghiệm 40
CHƯƠNG 7. KẾT LUẬN 43
Hướng phát triển tiếp theo của hệ thống. 44
TÀI LIỆU THAM KHẢO 45

TÀI LIỆU THAM KHẢOx
[TABLE="width: 100%"]
[TR]
[TD][1]
[/TD]
[TD]Leonardo de Moura, SMT Solvers: Introduction & Applications. Cambridge, USA: Microsoft Research, 2007.
[/TD]
[/TR]
[TR]
[TD][2]
[/TD]
[TD]Cesare Tinelli and Silvio Ranise, The SMT-LIB Standard.: Computer Science Department,The University of Iowa,Iowa City, IA, USA, 2006.
[/TD]
[/TR]
[TR]
[TD][3]
[/TD]
[TD]Barrett Clark, Deters Morgan, Oliveras Albert, and Stump Aaron, Satisfiability Modulo Theories Competition (SMT-COMP) 2010: Rules and Procedures.: Department of Computer Science, New York University, 2010.
[/TD]
[/TR]
[TR]
[TD][4]
[/TD]
[TD]Leonardo de Moura, SMT Solvers Theory & Practice.: Microsoft Research, 2006.
[/TD]
[/TR]
[TR]
[TD][5]
[/TD]
[TD]Erik T. Ray, Learning XML.: O'Reilly, 2001.
[/TD]
[/TR]
[TR]
[TD][6]
[/TD]
[TD]Clark S. Lindsey, S. Tolliver Johnny, and Lindblad Thomas, An Introduction to Scientific and Technical Computing with Java.: Cambridge University, 2005.
[/TD]
[/TR]
[TR]
[TD][7]
[/TD]
[TD]Steven Haines, Java Reference Guide.: Steven Haines , 2005.
[/TD]
[/TR]
[TR]
[TD][8]
[/TD]
[TD]Sinan Si Alhir, Learning UML. O'Reilly, 2003.
[/TD]
[/TR]
[/TABLE]