Tài liệu Khóa luậ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
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
Lời cảm ơn
Trước hết, tôi xin gửi lời cảm ơn chân thành và sâu sắc đến Tiến sỹ Trương
Anh Hoàng và Tiến sỹ Phạm Ngọc Hùng, những người đã trực tiếp hướng dẫn tôi
trong suốt quá trình nghiên cứu và phát triển đề tài nghiên cứu này. Để có được
những kết quả nghiên cứu như hiện nay, tôi vô cùng biết ơn sự quan tâm, hướng dẫn
nhiệt tình của hai thầy trong thời gian vừa qua.
Tôi xin chân thành cảm ơn các thầy cô trong trường Đại học công nghệ, Đại
học Quốc Gia Hà Nội...
47 trang |
Chia sẻ: haohao | Lượt xem: 1207 | Lượt tải: 0
Bạn đang xem trước 20 trang mẫu tài liệu Khóa luậ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, để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên
ĐẠ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
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
Lời cảm ơn
Trước hết, tôi xin gửi lời cảm ơn chân thành và sâu sắc đến Tiến sỹ Trương
Anh Hoàng và Tiến sỹ Phạm Ngọc Hùng, những người đã trực tiếp hướng dẫn tôi
trong suốt quá trình nghiên cứu và phát triển đề tài nghiên cứu này. Để có được
những kết quả nghiên cứu như hiện nay, tôi vô cùng biết ơn sự quan tâm, hướng dẫn
nhiệt tình của hai thầy trong thời gian vừa qua.
Tôi xin chân thành cảm ơn các thầy cô trong trường Đại học công nghệ, Đại
học Quốc Gia Hà Nội nói chung, và các thầy cô trong khoa công nghệ thông tin nói
riêng, những người đã nhiệt tình giảng dạy, giúp tôi có những kiến thức quý báu để tôi
có thể hoàn thành được đề tài luận văn này.
Tôi xin bày tỏ lòng cảm ơn đến các anh chị cao học, và các bạn trong nhóm
nghiên cứu đã cùng tôi tìm hiểu và xây dựng hoàn chỉnh hệ thống giải quyết bài toán
Satisfiability Modulo Theories (SMT) với hiệu năng cao, giúp tôi có thể hoàn thành tốt
phần nghiên cứu của mình.
Và cuối cùng, tôi xin gửi lời cảm ơn đến gia đình, bạn bè và những người thân đã
bên cạnh, động viên giúp tôi hoàn thành tốt luận văn của mình.
Hà Nội, tháng 05/2010
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 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
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 (SMT-
LIB) 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ả.
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
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
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
Danh sách các bảng trong tài liệu
Bảng 1: Luật sinh một toán hạng ................................................................................................ 7
Bảng 2: Luật sinh một công thức ................................................................................................ 8
Bảng 3: Luật sinh một thuyết ..................................................................................................... 8
Bảng 4: Luật sinh một logic ....................................................................................................... 8
Bảng 5 Luật sinh một chuẩn ....................................................................................................... 9
Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2 ............................................... 9
Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2 .............................................. 10
Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm ............................................................... 37
Bảng 9: Kết quả thời gian của thực nghiệm ............................................................................. 37
Bảng 10: Kêt quả trả về của thực nghiệm ................................................................................ 38
Danh sách các hình trong tài liệu
Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao. ............................................... 12
Hình 3.2: Mô hình ca sử dụng của hệ thống ............................................................................ 14
Hình 3.3: Mô hình hoạt động của hệ thống ............................................................................. 15
Hình 5.1: Biểu đồ lớp của hệ thống máy trạm ......................................................................... 30
Danh sách từ viết tắt trong tài liệu
Từ viết tắt Từ chuẩn Diễn giải
SMT Satisfiability Modulo Theories Các lý thuyết module về
tính thỏa được
SMT-LIB Satisfiability Modulo Theories -
Liblary
Thư viện các lý thuyết
module về tính thỏa được
API Application Programming Interface
Giao diện lập trình ứng
dụ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 2010
Trang 1
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
Chương 1. Mở đầu
1.1. Giới thiệu
Hiện nay, cùng với sự phát triển bùng nổ của hầu hết các ngành khoa học,
ngành khoa học máy tính cũng có những tiến bộ to lớn. Song song với đó, nhu cần
nghiên cứu về việc giải hoặc đưa ra tính khả thi của một biểu thức logic ngày càng
được quan tâm và phát triển. Bởi lẽ, rất nhiều các ứng dụng hay những sự tính toán
trong ngành khoa học máy tính cần đến những công thức logic phức tạp. Trong
khoảng hai thập niên gần đây, ngành khoa học máy tính đã có những tiến bộ lớn đối
với việc tự động chứng minh hay bác bỏ tính đúng đắn của một biểu thức logic. Tuy
nhiên việc chứng minh các biểu thức logic sẽ khó khăn hơn nhiều nếu đặt chúng trong
một nền lý thuyết thay vì chứng minh một cách tổng quát [1,2]. Những vấn đề này
được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories
hay còn được viết tắt là SMT [1]).
Cho đến nay, nhiều trường đại học cùng những nhà nghiên cứu khoa học máy
tính đã có những nghiên cứu, sản phẩm để giải quyết vấn đề này. Tuy nhiên, việc xây
dựng một bộ giải các vấn đề SMT tối ưu cho mọi trường hợp và rất khó khăn. Vì vậy,
vấn đề được đặt ra là kết hợp các bộ giải SMT đó để có được một bộ giải tối ưu nhất
về mặt thời gian.
1.2. Bài toán đặt ra
Đối với việc giải quyết các vấn đề SMT, nhiều trường đại học cũng như các cơ
quan, tổ chức lớn trên thế giới đã có những nghiên cứu và đưa ra những sản phẩm của
mình. Tuy nhiên, với mỗi sản phẩm, họ đưa vào những thuật toán khác nhau để giải
quyết vấn đề này. Trong khuôn khổ đồ án, việc nghiên cứu cơ chế, và tính đúng đắn
của những bộ giải này không được đề cập đến (kết quả đưa ra của các bộ giải sẽ được
coi là luôn đúng đắn) mà sẽ tập trung vào việc sử dụng những bộ giải này như là
những công cụ giải quyết vấn đề SMT được đưa vào. Với những kết quả đưa ra bởi
các bộ giải này, cần có một kết trả được trả về tối ưu nhất về mặt thời gian.
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
Trang 2
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
Để giải quyết vấn đề nói trên, cần có một hệ thống phân phối các vấn đề SMT
cho các bộ giải và nhận về kết quả trả về tối ưu nhất về mặt thời gian. Ngoài ra để tiện
cho việc sử dụng và phát triển hệ thống, cần có một thư viện các hàm nhúng hỗ trợ
người sử dụng xây dựng các vấn đề SMT.
1.3. Cấu trúc nội dung tài liệu
Tài liệu này nhằm giới thiệu về bài toán SMT và mô tả hệ thống giải quyết bài
toán đó trực tuyến. Chương mở đầu của tài liệu giới thiệu qua về bài toán SMT và bài
toán đặt ra cho việc xây dựng hệ thống giải quyết bài toán SMT đó.
Chương thứ hai của tài liệu đề cập tới một số kiến thức về SMT và cấu trúc,
khuôn dạng của bài toán SMT được xây dựng theo chuẩn SMT-LIB. Chương này được
coi là kiến thức nền tảng để xây dựng hệ thống giải quyết bài toán SMT hiệu năng cao.
Những kiến thức trong chương này sẽ được sử dụng để xây dựng các hàm API cho hệ
thống máy khách và một số thành phần của hệ thống máy trạm.
Chương ba và chương bốn là phần phân tích và hướng giải quyết vấn đề xây
dựng hệ thống giải bài toán SMT hiệu năng cao. Chương ba sẽ tập trung hơn vào vấn
đề phân tích, đưa ra một cái nhìn tổng quan về hệ thống và quy trình hệ thống sẽ hoạt
động. Chương bốn sẽ là một số lựa chọn giải pháp để giải quyết một số vấn đề khi xây
dựng hệ thống.
Hệ thống giải bài toán SMT hiệu năng cao phần máy trạm và máy khách sẽ được
mô tả chi tiết trong chương năm. Ở chương này, hệ thống các hàm API trên máy khách
sẽ được mô tả rất chi tiết và có thể coi là tài liệu hướng dẫn cho người dùng sử dụng
các hàm API này.
Chương sáu sẽ đưa ra phần thực nghiệm và đánh giá kết quả của hệ thống. Trong
chương này, kết quả của một số thực nghiệm hệ thống sẽ được đưa ra nhằm đưa ra một
số ưu điểm mà hệ thống có được.
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
Trang 3
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
Chương 2. Kiến thức nền tảng
2.1. Giới thiệu SMT
Tính thỏa mãn là một trong những vấn đề quan trọng nhất của ngành khoa học
máy tính. Các vấn đề cần tính thỏa mãn được ứng dụng trong cả phát triển phần cứng
cũng như phần mềm, đặc biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị [3].
Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây dựng dựa trên việc
tạo ra các công thức tiền tố và việc chứng minh tính hợp lệ của chúng. Cho dù hai thập
niên gần đây, việc chứng minh tính hợp lệ của các định lý, biểu thức tiền tố có những
tiến bộ đáng kể, tuy nhiên, không phải công thức nào cũng có thể chứng minh một
cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều công thức không quan tâm
đến tính khả thi trong trường hợp tổng quát mà chỉ được quan tâm trong một lý thuyết
nền tảng [2,1]. Việc nghiên cứu tính khả thi của các công thức trong một lý thuyết nền
tảng được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo
Theories hay SMT) và các công cụ để chứng minh một cách tự động các tính khả thi
của những vẫn đề SMT được gọi là bộ giải SMT (SMT solver).
Lý thuyết về SMT sẽ được đề cập cụ thể hơn trong phần giới thiệu về thư viện
SMT.
2.2. Bộ giải SMT (SMT solver)
Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT được phát triển khá
sớm, từ đầu những năm 1980. Tại thời điểm đó, một số bộ giải được xây dựng bởi
Greg Nelson và Derek Oppent tại trường đại học Stanford , Robert Shostak tại SRI, và
Robert Boyer và J Moore tại trường đại học ở Texas. Đến cuối những năm 1990, việc
nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ SAT đã xây dựng nhiều bộ
giải SMT tiến bộ hơn [4].
Như đã đề cập ở trên, trong khuôn khổ đồ án, việc đánh giá về tính đúng đắn,
các nghiên cứu về thuật giải của từng bộ giải sẽ không được đề cập đến. Vấn đề được
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
Trang 4
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
đặt ra ở đây là kết quả của bộ giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều
các bộ giải như Absolver, Boolector, CVC3, OpenSMT, Yices, Z3…
Do yêu cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán
SMT đó có thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức năng này. Ngoài
ra hệ thống sử dụng đầu vào theo chuẩn của SMT-Lib và ngắt thời gian giải một bài
toán (trong trường hợp bài toán cần thời gian giải quá lớn), do đó, bộ giải cần phải có
hỗ trợ những chức năng này khi hoạt động. Từ những yêu cầu đó, nhóm nghiên cứu và
phát triển hệ thống đã quyết định sử dụng song song hai bộ giải là Yices của SRI
International và Z3 của Microsoft. Hai bộ giải này tuy có cấu trúc khác nhau nhưng
cùng được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-Loveland) [5]. Việc
tìm hiểu, phân tích cấu trúc cũng như thuật toán của hai bộ giải này sẽ không được đề
cập cụ thể ở đây.
2.3. Thư viện SMT (SMT-LIB)
Đề giải quyết các vấn đề SMT, việc nghiên cứu và đưa ra một chuẩn đầu vào là
rất cần thiết. Thông thường, mỗi bộ giải SMT đều có một quy định riêng cho chuẩn
đầu vào của mình, tuy nhiên như vậy sẽ thực sự khó khăn đối với việc thực thi một đầu
vào bởi các bộ giải khác nhau. Vì vậy, việc nghiên cứu và đưa ra một chuẩn đầu vào
thống nhất là rất cần thiết.
Khoảng tháng tư năm 2004, Silvio Rainise và Cesare Tinelli đã đưa ra chuẩn về
SMT-LIB đầu tiên [6]. Thời gian sau đó, họ liên tục cải tiến chuẩn đầu vào, bổ sung
những quy định chuẩn, thuyết mới. Cho đến nay, hai tác giả này đã và đang xây dựng
chuẩn SMT-LIB đã có phiên bản 2.0, tuy nhiên việc xây dựng đầu vào dựa trên chuẩn
mới này chưa được phổ biến. Hầu hết các bộ giải cũng như đầu vào cho các vấn đề
SMT-LIB đều được sử dụng bởi chuẩn 1.2 mà họ đã xây dựng vào khoảng tháng 8
năm 2006.
2.3.1. Cấu trúc cơ bản của SMT-LIB
Như đã nói ở trên, vấn đề SMT là việc kiểm tra biểu thức logic φ có thỏa mãn
được hay không trong lý thuyết nền T hay có một khuôn mẫu của T là khả thi. Vì vậy,
kiến trúc cơ bản của một SMT-LIB thường bao gồm các vấn đề sau [7]:
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
Trang 5
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
- Một thủ tục logic cơ sở (underlying logic): Định dạng SMT-LIB hiện tại có hai
định nghĩa về ngữ nghĩa của logic cơ sở. Thứ nhất là dịch nghĩa sang những
biểu thức tiền tố cổ điển, có nghĩa là thủ tục của logic cơ sở giúp cho việc
chuyển đổi sang khung làm việc của công cụ có sẵn hoặc giúp kiểm tra kết quả
một cách dễ dàng hơn. Nghĩa thứ hai là chi phối ngữ nghĩa đại số dựa trên
nhiều khuôn mẫu rút gọn.
- Một lý thuyết nền (background theory): là những lý thuyết nền dùng để kiểm
chứng tính thỏa mãn. Những lý thuyết cơ bản bao gồm lý thuyết số thực, lý
thuyết mảng.. Phiên bản hiện tại của SMT-LIB chỉ hỗ trỡ những lý thuyết cơ
bản này.
- Một ngôn ngữ đầu vào (input language): Là lớp các biểu thức được chấp nhận
như là đầu vào của SMT-LIB.
2.3.2. Khuôn dạng của SMT-LIB
Một thư viện SMT được xây dựng theo chuẩn và dựa trên những định nghĩa sau
(theo [7]):
Định nghĩa 1 (Ký hiệu của SMT-LIB – SMT-LIB signature): Một ký hiệu SMT-
LIB Σ là một bộ dữ liệu bao gồm:
- Một tập không rỗng ∑ ⊆ các ký hiệu phân cấp (sort symbol), một tập
hợp ký hiệu hàm (function symbol) ∑ ⊆ và tập hợp các ký hiệu vị từ
(predicate symbol) ∑ ⊆ ;
- Một toàn ánh (total mapping) từ các biến (term variables) X tới ΣS;
- Một quan hệ toàn phương (total relation) từ ΣF đến (ΣS)+, một chuỗi các
thành phần của ΣS, không bao giờ có một cặp định dạng (f,s1…sns) và
(f,s1…sns’) với s và s’ khác nhau;
- Một quan hệ toàn phương từ ΣP tới (ΣS)*, thứ tự các thành phần ΣP.
Định nghĩa 2 (Công thức trong SMT-LIB – SMT-LIB formula): Các công thức
trong ngôn ngữ SMT-LIB là một tập hợp tất cả các công thức đúng cú pháp
đóng (closed well-formed formula).
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
Trang 6
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
Định nghĩa 3 (khai báo lý thuyết – theory decl): chỉ tồn tại một khai báo lý
thuyết trong một bài toán SMT-LIB và phải thỏa mãn những giới hạn sau:
- Chúng bao gồm các khai báo của thuộc tính “sort” và “definition”;
- Chúng chứa ít nhất một khai báo với một thuộc tính;
- Không tồn tại khai báo định dạng f,s1…sns và f,s1…sns’ cho cùng một ký
tự hàm f mà s và s’ khác nhau;
- Tất cả các rút gọn trong khai báo ký tự hàm, vị từ được liệt kê trong khai
báo thuộc tính “sort”;
- Định nghĩa của lý thuyết được quy định trong thuộc tính “definition” và
chỉ liên quan đến các khai báo ký tự phân cấp, ký tự hàm và ký tự vị từ;
- Công thức trong thuộc tính “axiom” được xây dựng trên các khái báo ký
tự trong các thuộc tính “sort”, “funs”, “pred”.
Định nghĩa 4 (Khai báo Logic): Chỉ có một luật Logic được khai báo trong một
bài toán SMT và phải được thỏa mãn các giới hạn sau:
- Chúng bao gồm các khai báo thuộc tính “theory” và “language”;
- Chúng chứa ít nhất một khai báo đối với một thuộc tính;
- Giá trị của thuộc tính “theory” phải trùng với tên của thuyết T cho vài khai
báo của DT trong SMT-LIB.
Định nghĩa 5 (Khai báo về chuẩn): luật khai báo chuẩn phải thỏa mãn những
giới hạn sau:
- Chúng chứa chính xác một khai báo của thuộc tính “logic”, “formula” và
“status”;
- Giá trị của thuộc tính “logic” phải trùng khớp với tên của logic L cho vài
khai báo DL trong SMT-LIB;
- Mỗi một ký hiệu được khai báo trong thuộc tính “extrasorts”, “extrafuns”
và “extrapred” cần phải là một phần của các ký hiệu được định nghĩa trong
thuộc tính “language” của logic L;
- Có thể có hơn một khai báo của thuộc tính “extrasort”;
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
Trang 7
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
- Có thể có hơn một khai báo của thuộc tính “extrafuns”, và mỗi thuộc tính
“funs” của khai báo thuyết liên kết tới DL phải thỏa mãn yêu cầu 3 của
định nghĩa 3;
- Ký hiệu rút gọn trong khai báo “extrafuns” hoặc “extrapred” hoặc được
khai báo trong “extrasort” hoặc thuộc về ký hiệu của logic L;
- Công thức trong khai báo thuộc tính “assumption” và “formula” là ngôn
ngữ của L và các ký hiệu của chúng được khai báo trong thuộc tính
“extrasorts” “extrafuns” và “extrapred”.
Từ những định nghĩa trên, việc xây dựng một bài toán SMT dựa trên chuẩn
SMT-LIB sẽ theo cấu trúc sau [7]:
Bảng 1: Luật sinh một toán hạng
(1) ::= Chuỗi các ký tự, số, dấu chấm(.), nháy đơn(‘)
và gạch dưới , bắt đầu bởi ký tự
(2) ::= Bất kỳ chuỗ ký tự có thể in ra được
(3) ::= {}
(4) ::= 0 | chuỗi không rỗng các chữ số bắt đầu khác 0
(5) ::= .0*
(6) ::= [(:)*]
(7) ::= |
(8) ::= ?
(9) ::= $
(10) ::= :
(11) ::= Chuỗi không rỗng các ký tự:
=, >, <, &, @, #, +, -, *, /, %, |, ~
(12) ::= |
(13) ::= | | distinct
(14) ::=
(15) ::= |
(16) ::= | | |
(17) ::= | ( +)
| ( + *)
| (ite
*)
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
Trang 8
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
Bảng 2: Luật sinh một công thức
(1) ::= true | false | |
(2) ::= | ( +)
| ( + *)
(3) ::= not | implies | if_then_else | and | or | xor | iff
(4) ::= exists | forall
(5) ::= ( )
(6) ::=
| ( + * )
| ( +
* )
| (let ( ) *
)
| ( flet ( )
* )
Bảng 3: Luật sinh một thuyết
(1) ::= chuỗi liên tiếp các ký tự
(2) ::= “”
(3) ::= ( + *)
| ( *)
| ( *)
(4) ::= ( * *)
(5) ::=
(6) ::= :sort ( +)
| :funs (+)
| :preds ()
| :definition
| :axioms
|
(7) ::= (theory +)
Bảng 4: Luật sinh một logic
(1) ::=
(2) ::= : theory
| :language
| :extensions
| :notes
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
Trang 9
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
|
(3) ::= (logic +)
Bảng 5 Luật sinh một chuẩn
(1) ::= sat | unsat | unknown
(2) ::=
(3) ::= :logic
| :assumption
| :formula
| :status
| :extrasorts ( + )
| :extrafuns ( + )
| :extrapreds ( + )
| :notes
|
(4) benchmark ::= ( benchmark + )
Các lý thuyết nền cơ bản đã được nghiên cứu và đưa ra:
Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2
Arrays Các hàm mảng
ArraysEx Các hàm mảng mở rộng
Fixed_Size_BitVectors[32] Bit vector 32 bit
Fixed_Size_BitVectors Bit vector với kích cỡ tùy ý.
BitVector_ArraysEx Bit vector với kích cỡ tùy ý và mảng chứa kiểu
dữ liệu bit vector
Empty Thuyết trống với ký hiệu rỗng
Ints Số nguyên
Int_Arrays Mảng số nguyên
Int_ArraysEx Mảng giá trị được đánh thứ tự số nguyên với tiền
đề mở rộng
Int_Int_Real_Array_ArraysEx Mảng của mảng các số nguyên và số thực với tiền
đề mở rộng
Reals Số thực
Reals_Ints Số nguyên và số thực
Nội dung cụ thể của từng lý thuyết xin được không đề cập đến ở đây để tránh
việc trình bày lan man không cần thiết.
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
Trang 10
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
Các logic cơ bản được áp dụng trong định dạng của SMT-LIB:
Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2
AUFLIA Các công thức tuyến tính trên thuyết mảng số nguyên với
những ký tự phân cấp, hàm và thuộc tính tự do.
AUFLIRA Các công thức tuyến tính với ký hiệu hàm và ký hiệu vị từ
trong thuyết 10 nêu trên
AUFNIRA Công thức với các ký tự hàm và vị từ tự do dựa trên thuyết 10
LIA Công thức tuyến tính trên các phép toán số nguyên
LRA Công thức tuyến tính trên các phép toán số thực
QF_A Công thức lượng từ tự do trên thuyết mảng không mở rộng
QF_AUFBV Công thức lượng tự trên thuyết bitvector và mảng bitvector với
các ký hiệu hàm và ký hiệu vị từ tự do.
QF_AUFLIA Công thức tuyến tính và lượng từ tự do trên thuyết mảng các số
nguyên với ký tự phân cấp, ký tự hàm và ký tự lượng từ.
QF_AX Công thức lượng từ tự do trên thuyết của mảng mở rộng
QF_BV Công thức lượng từ tự do với thuyết bitvector cố định kích cỡ
QF_IDL Logic khác trên số nguyên. Ví dụ bất đẳng thức x-y <b với x,y
là các biến nguyên và b là một hằng số nguyên
QF_LIA Tổ hợp giữa bất đẳng thức của đa thức tuyến tính trên biến số
nguyên
QF_LRA Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số thực
QF_NIA Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số
nguyên với ít nhất một đa thức không tuyến tính
QF_RDL Logic khác của số thực, ví dụ bất đẳng thức x – y < b với x,y là
số thực và b là một hằng số hữu tỷ
QF_UF Công thức vô lượng hóa (Unquantified formulas) xây dựng
trên ký hiệu của ký tự phân cấp, ký tự hàm, ký tự vị từ không
QF_UFIDL Logic khác trên số nguyên nhưng với những ký tự phân cấp, ký
tự hàm, ký tự vị từ không được giải thích
QF_UFBV Công thức vô lượng hóa trên kiểu bitvectors với ký tự hàm và
ký tự vị từ.
QF_UFLIA Phép tính số nguyên vô lượng hóa tuyến tính với ký tự phân
cấp, ký tự hàm và ký tự vị từ
QF_UFLRA Phép tính số thực vô lượng hóa tuyến tính với ký tự phân cấp,
ký tự hàm và ký tự vị từ
QF_UFNRA Phép tính số thực vô lượng hóa không tuyến tính với ký tự
phân cấp, ký tự hàm và ký tự vị từ
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
Trang 11
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
UFNIA Phép tính số nguyên không tuyến tính với ký tự phân cấp, hàm
và vị từ không xác định.
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
Chương 3. Phân tích hệ thống
3.1. Mô hình hệ thống
Để giải một bài toán SMT một cách song song giữa các bộ giải, đồng thời đảm
bảo được hiệu năng cao cho hệ thống, nhóm nghiên cứu đã đưa ra hướng giải quyết là
xây dựng hệ thống giải quyết vấn đề SMT trực tuyến qua mạng. Hệ thống sẽ được chia
ra làm ba phần rõ rệt là phần máy khách gửi yêu cầu giải quyết vấn đề, phần máy chủ
xử lý và phân phối các vấn đề nhận được, và phần máy trạm giải quyết vấn đề được
yêu cầu. Mô hình hệ thống được xây dựng như sau:
Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao.
Việc xây dựng phát triển hệ thống giải quyết vấn đề SMT trực tuyến sẽ đáp ứng
được yêu cầu về hiệu năng xử lý đầu vào. Hệ thống sẽ tiếp nhận một lúc nhiều 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 2010
Trang 13
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
từ nhiều người sử dụng trực tuyến. Với mỗi vấn đề nhận được, hệ thống sẽ phân phối
cho tất cả các bộ giải và chờ đợi kết quả trả về tối ưu nhất về mặt thời gian để trả về
cho phía yêu cầu. Đối với những bộ giải đưa ra kết quả sau sẽ nhận được tín hiệu dừng
xử lý vấn đề đó. Do hệ thống được xây dựng trực tuyến, nên việc nhận cùng một lúc
nhiều yêu cầu cần xử lý là điều tất yếu, vì vậy, hệ thống máy chủ vừa đảm nhận việc
chia một vấn đề cho nhiều máy trạm xử lý, vừa phải xử lý đồng thời cùng lúc nhiều
yêu cầu như vậy. Về phía máy trạm, mỗi máy trạm sẽ luôn nhận và xử lý nhiều các
vấn đề một lúc và phải trả về kết quả tương ứng cho mỗi vấn đề. Để tiện cho người sử
dụng bên phía máy khách, hệ thống cần phải có một thư việc các hàm nhúng API để
người sử dụng trực tiếp xây dựng vấn đề SMT và gửi lên phía máy chủ.
3.2. Mô hình ca sử dụng của hệ thống
Đối với hai hệ thống con được cài đặt trên máy khách và máy trạm, thì máy chủ
được coi như là một tác nhân trung gian giúp duy trì tương tác giữa chúng với nhau.
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
Hình 3.2: Mô hình ca sử dụng của hệ thống
Ở phía máy khách (user), người sử dụng sẽ tạo bài toán SMT, hoặc chỉ định cho
hệ thống tệp tin SMT cần thiết phải kiểm tra tính thỏa mãn để hệ thống sẽ gửi lên phía
máy chủ (server). Sau khi gửi bài toán lên phía máy chủ, hệ thống trên máy khách sẽ
chờ cho máy chủ gửi kết quả về và nhận kết quả trả về. Viêc gửi bài toán SMT bên
phía máy khách sẽ bao gồm cả việc gửi yêu cầu thời gian ngắt của các bộ giải SMT.
Với máy trạm (solver) sau khi kết nối và nhận được tệp tin chứa vấn đề SMT
cần giải quyết, hệ thống sẽ gọi lệnh chạy các công cụ giải SMT. Sau khi đưa ra được
kết quả, hoặc sau khi nhận được tín hiệu ngắt từ phía máy chủ, máy trạm sẽ gửi lại kết
quả đến máy chủ để máy chủ gửi lại phía máy khách.
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
3.3. Mô hình hoạt động
Hình 3.3: Mô hình hoạt động của hệ thống
Từ biểu đồ hoạt động của hệ thống, ta có thể xác định được các công việc tuần
tự của hệ thống và cách làm việc của hệ thống như sau:
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
Trang 16
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
Khi hệ thống hoạt động, các máy khách sẽ kết nối đến máy chủ và xây dựng bài
toán SMT. Bài toán SMT có thể đã được mô tả bằng tệp tin hay được xây dựng bằng
chương trình với việc sử dụng hệ thống được cài đặt trên. Sau khi xác định bài toán
SMT, hệ thống máy khách sẽ gửi bài toán toán đó cho máy chủ đồng thời gửi thông tin
về thời gian giới hạn thực hiện giải bài toán và chờ đợi kết quả trả về từ phía máy chủ.
Máy chủ lắng nghe các kết nối của máy khách, khi nhận được bài toán SMT và
tham số về thời gian thực hiện bài toán gửi từ máy khách, máy chủ sẽ phân phối các
bài toán đó cho các máy trạm có bộ giải các bài toán SMT đang kết nối đến máy chủ
và đón chờ kết quả phản hồi từ máy trạm.
Máy trạm sẽ nhận bài toán từ máy chủ và bắt đầu việc thực hiện giải bài toán,
khi đó giá trị về trễ thời gian cho mỗi bài toán sẽ được sử dụng. Sau khi hệ thống trên
máy trạm gọi các bộ giải để giải quyết vấn đề được đưa tới, sẽ có hai trường hợp xảy
ra tiếp sau đó. Trường hợp một là máy trạm đó sẽ giải ra kết quả nhanh nhất và gửi về
phía máy chủ kết quả. Trường hợp thứ hai là nhận được tín hiệu ngắt tiến trình (do đã
có máy trạm khác gửi được kết quả đến máy chủ), khi đó, một lệnh ngắt tiến trình
đang được thực thi sẽ được gọi. Và ở trường hợp này, máy trạm không gửi gì về phía
máy chủ nữa.
Phía máy khách sau khi nhận được kết quả của hệ thống sẽ hiển thị cho người
dùng thấy được kết quả của bài toán mà hệ thống gửi đế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 2010
Trang 17
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
Chương 4. Phương hướng giải quyết vấn đề
4.1. Lựa chọn phương thức kết nối
Bài toán được đặt ra là xây dựng hệ thống trực tuyến, vì vậy cần có phương
thức kết nối phù hợp với những yêu cầu đã được nêu ra trong phần trên. Có hai
phương thức kết nối được đưa ra lựa chọn là xây dựng hệ thống dựa trên các kết nối
của webservice hoặc sử dụng kết nối socket.
Đối với phương thức kết nối dựa trên webservice, thời gian kết nối sẽ chậm hơn
rất nhiều so với kết nối trực tiếp qua socket. Tuy nhiên, với phương thức kết nối
socket, ta phải tự xây dựng cách thức giao tiếp giữa máy trạm với máy chủ và máy chủ
với máy khách.
Do yêu cầu tối ưu về mặt thời gian được quan tâm hàng đầu, vì vậy phương
thức được tối ưu cho hệ thống là xây dựng giao tiếp qua kết nối socket.
4.2. Lựa chọn ngôn ngữ lập trình
Do phương thức kết nối được lựa chọn là kết nối socket, vì vậy cần một ngôn
ngữ lập trình bậc cao để tiện cho việc xây dựng cách thức giao tiếp giữa máy chủ -
máy trạm và máy chủ - máy khách. Mặt khác, do các bộ giải có thể được cài đặt trên
nhiều nền hệ điều hành khác nhau, nên cần có ngôn ngữ lập trình hỗ trợ việc chạy trên
nhiều hệ điều hành khác nhau. Chính vì các lý do này, nhóm nghiên cứu đã quyết định
sử dụng ngôn ngữ lập trình Java để xây dựng hệ thống.
4.3. Xác định dữ liệu đầu vào, đầu ra của hệ thống
Để tăng hiệu năng của hệ thống giải bài toán SMT, hệ thống có sử dụng nhiều
các bộ giải khác nhau. Tuy rằng mỗi bộ giải có một chuẩn đầu vào riêng, nhưng để
tiện cho việc giải quyết vấn đề một cách nhanh chóng và hiệu quả, hệ thống chỉ sử
dụng đầu vào bài toán SMT theo chuẩn của SMT-LIB. Hiện nay, hầu hết các công cụ
giải các bài toán đều hỗ trợ chuẩn SMT-LIB, vì vậy, để tránh việc phải chuẩn hóa đầu
vào cho mỗi bài toán nhằm đảm bảo hiệu năng cao về mặt thời gian, hệ thống yêu cầu
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
Trang 18
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
đầu vào của người sử dụng phải đáp ứng nghiêm ngặt các điều kiện xây dựng một bài
toán dưới quy chẩn của SMT-LIB.
Hệ thống được chia ra thành ba thành phần với chức năng và vai trò khác nhau,
do đó với mỗi hệ thống con sẽ có một đầu vào đầu ra riêng ứng với từng chức năng
của hệ thống con đó.
Với hệ thống được cài đặt trên máy khách, người dùng sẽ đưa vào tệp tin chứa
bài toán SMT hoặc xây dựng bài toán SMT dựa trên các hàm nhúng API mà hệ thống
xây dựng. Bài toán sẽ được gửi lên máy chủ và chờ máy chủ phản hồi về kết quả.
Đối với hệ thống được cài đặt trên máy chủ, đầu vào nhận từ máy khách (bài
toán SMT) sẽ là đầu ra chuyển tới máy trạm. Và đầu vào thứ hai là kết quả nhận được
từ máy trạm cũng là đầu ra để chuyển tới máy khách.
Trên máy trạm có duy nhất một bộ dữ liệu đầu vào là bài toán SMT nhận được
từ máy chủ và một bộ dữ liệu đầu ra duy nhất là kết quả của việc giải bài toán SMT
đó.
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
Trang 19
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
Chương 5. Mô tả hệ thống
Hệ thống giải bài toán SMT hiệu năng cao được chia làm ba hệ thống con với chức
năng và tác dụng riêng. Trong giới hạn tài của tài liệu này, hệ thống con cài đặt trên
máy chủ sẽ không được đề cập đến. Trong phần này, hệ thống cài đặt trên máy khách
và máy trạm sẽ đươc giải thích và mô tả chi tiết.
5.1. Quy định cách thức giao tiếp với máy chủ
Do hệ thống hoàn toàn được xây dựng bằng phương pháp kết nối socket, vì vậy
cần phải có một cách thức giao tiếp phù hợp giữa các hệ thống con với nhau. Dựa trên
ý tưởng của ngôn ngữ XML, nhóm nghiên cứu đã đưa ra và thống nhất việc sử dụng
các thẻ đươc quy định sẵn để giao tiếp giữa các hệ thống con với nhau.
Các thẻ sẽ được định nghĩa đúng như quy chuẩn của XML với quy định sau:
- Thẻ mở sẽ có dạng
- Thẻ đóng sẽ có dạng
Đối với thẻ đơn thì không cần có thẻ đóng.
Cụ thể, các thẻ được quy định trong hệ thống như sau:
- Cặp thẻ : thể hiện sự bắt tay kết nối giữa các thành phần trong
hệ thống với nhau.
- Cặp thẻ : thể hiện việc bắt đầu chuyển dữ liệu từ tệp tin chứa bài
toán SMT giữa các hệ thống con trong hệ thống
- Cặp thẻ : thể hiện nội dung kết quả của bài toán SMT được
trả về
- Thẻ đơn : là tín hiệu ngắt kết nối được máy chủ gửi đến máy trạm
- Thẻ đơn : thể thiện sự kết thúc kết nối giữa người dùng với máy chủ
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
Trang 20
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. Phần máy khách
5.2.1. Quy định giao tiếp với máy chủ
Yêu cầu chính cho hệ thống cài đặt trên máy khách là gửi bài toán SMT và
nhận về kết quả của bài toán ấy. Quy trình kết nối của máy khách với máy chủ sẽ
như sau:
- Sau khi kết nối được máy chủ, máy khách sẽ đưa ra một loạt thẻ chào hỏi
[Name]
- Sau chuỗi các thẻ được gửi lên máy chủ, máy khách sẽ chờ đến khi máy chủ
đáp lại “OK”. Sau đó, hệ thống trên máy khách sẽ thực hiện tiến trình gửi trễ
thời gian (time out) giải bài toán SMT cần giải. Trễ thời gian này được người sử
dụng quy định và đưa vào.Trong trường hợp người dùng không thiết lập thông
tin này, thì hệ thống sẽ gửi lên thời gian mặc định là 30 giây. Quá trình gửi trễ
thời gian được quy định như sau:
[trễ thời gian]
- Sau khi gửi lên thời gian giới hạn thực thi của bài toán, hệ thống sẽ tiếp tục gửi
lên tệp tin dữ liệu chứa nội dung bài toán. Quy trình gửi tệp tin dữ liệu cũng
được theo quy định sau:
[Nội dung dữ liệu chuyển lên]
- Sau quá trình gửi tệp tin dữ liệu thành công, hệ thống trên máy khách chờ kết
quả của máy chủ trả về. Khi nhận được tín hiệu trả về ( tín hiệu kết quả trả về
được quy định là thẻ mở ) hệ thống sẽ nhận cho đến khi có tín hiệu kết
thúc (thẻ đóng ):
[nội dung kết quả trả về]
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
Trang 21
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
- Sau khi đã nhận được kết quả, máy khách sẽ chủ động ngắt kết nối đến máy
chủ.
Như đã đề cập ở trên, để tránh việc lãng phí thời gian của hệ thống cho việc
chuẩn hóa đầu vào, hệ thống yêu cầu người sử dụng đưa vào đầu vào theo đúng
chuẩn của SMT-LIB. Vấn đề đặt ra ở đây là không phải lúc nào người sử dụng
cũng có sẵn bài toán SMT được tổ chức theo quy chuẩn của STM-LIB. Chính
vì vậy, hệ thống cần phải xây dựng các hàm API để người dùng có thể xây
dựng bài toán theo đúng chuẩn định dạng của SMT-LIB.
Dựa vào các định nghĩa và quy chuẩn về đầu vào của bài toán SMT theo chuẩn
SMT-LIB (được nêu trong phần kiến thức nền tảng), hệ thống đã đưa ra các hàm API
để thuận tiện cho người sử dụng đưa vào.
5.2.2. Các lớp của hệ thống máy khách
5.2.2.1. Lớp config: lớp này được xây dựng để chứa các quy ước việc
giao tiếp cũng như các thành phần mặc định của hệ thống như các thẻ,
tên tệp tin đầu vào mặc định, thời gian ngắt mặc định, tên tệp tin chứa
dữ liệu được trả về
5.2.2.2. Lớp Client: Có chức năng mở kết nối, gửi bài toán từ tệp tin lên
máy chủ và nhận về kết quả.
5.2.2.3. Lớp NetSolver: bao gồm các hàm thiết lập tùy chọn cho người sử
dụng. Cụ thể:
- void setPath (String Path): Thiết lập đường dẫn cho tệp tin đầu vào.
Có thể là một đường dẫn đến một tệp tin sẽ được xây dựng sau đó bởi
chính người sử dụng. Hoặc cũng có thể là một tệp tin đã chứa nội
dung bài toán SMT cân gửi lên máy chủ.
- void setOutput (String Path): Thiết lập đường dẫn cho tệp tin lưu giữ
kết quả được trả về. Xin lưu ý rằng việc thiết lập đường dẫn bao gồm
cả tên tệp tin.
- void Solve (): thực thi việc gửi và nhận bài toán SMT. Thực chất hàm
này chỉ gọi một đối tượng của lớp Client và thực thi đối tượng ấy.
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
Trang 22
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
Việc xây dựng bài toán SMT sẽ dựa trên các hàm API được xây dựng
bởi các lớp sau. Xin lưu ý rằng các hàm API được xây dựng hoàn
toàn dựa trên bộ luật cú pháp của ngôn ngữ đầu vào SMT đã được
đưa ra ở trên.
5.2.2.4. Lớp Bench_attribute: Được xây dựng dựa trên bảng 5.
- Bench_attribute (String Bench_name) : Định nghĩa một thuộc tính
Benchmark đầu vào với tên là Bench_name.
- Void setLogic (String LogicName): thiết lập tên logic của Benchmark
- void setStatus (String stt) : thiết lập thuộc tính Status cho Benchmark
- void setFormulas (Formula F): thiết lập Formula cho Benchmark.
- void setAssumtion (Formula f): thiết lập Assumtion cho Benchmark
- void setAnnotation (annotation an): thiết lập Annotation cho
Benchmark
- void setNotes (String note): thiết lập Note cho Benchmark
- void setExtrasorts (Identifier[] id): Thiết lập Extrasorts cho
Benchmark
- void setExtrafuns (func_decl[] funcs): Thiết lập Extrafuns cho
Benchmark
- void setExtrapreds (pred_decl[] preds): thiết lập Extrapreds cho
Benchmark
- void printBench (): ghi Benchmark vừa thiết lập ra tệp tin được chỉ
định
5.2.2.5. Lớp Formula: Được xây dựng dựa trên bảng 2 để đưa ra các
công thức trong bài toán SMT, Các hàm hỗ trợ xây dựng bao gồm:
- Formula (boolean b): khai báo một Formula với giá trị là giá trị của
một biến logic
- Formula (fvarDecl fvar): Khai báo một Formula với giá trị là một
khai báo hàm.
- Formula (Identifier id): khai báo một Formula với giá trị là một định
danh Identifier.
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
Trang 23
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
- Formula (Identifier id, Term te[]): khai báo một Formula từ một định
danh Identifier và một mảng không rỗng các phần tử Term
- Formula (Arith_symb ar, Term te[]): khai báo một Formula từ một
(hoặc một chuỗi) các phép toán và một mảng không rỗng các phần tử
Term
- Formula (Term te[]): khai báo một Formula với từ khóa “distinct” và
một mảng không rỗng các phần từ Term
- void Setvalue (String val): đặt giá trị của Formula theo tùy biến ( khi
công thức của người sử dụng không thể xây dựng dựa trên các hàm
API trong lớp formula)
- Formula orOperator (Formula a1, Formula a2): phép “or” giữa hai
công thức
- Formula xorOperator (Formula a1, Formula a2): phép “xor” giữa hai
công thức
- Formula iffOperator (Formula a1, Formula a2): phép “iff” giữa hai
công thức
- Formula impliesOperator (Formula a1, Formula a2): phép “implies”
giữa hai công thức
- Formula existsFomular (quant_var[] qv, Formula f): công thức được
xây dựng với từ khóa “exists”
- Formula forallFomular (quant_var[] qv, Formula f): công thức được
xây dựng với từ khóa “forall”
- Formula letFormula (varDecl var,Term t, Formula f): công thức
được xây dựng với từ khóa “let”
- Formula fletFormula (fvarDecl fvar,Formula f1, Formula f2): công
thức được xây dựng với từ khóa “flet”
5.2.2.6. Lớp func_decl: khai báo một hàm của bài toán SMT, được xây
dựng dựa trên (3) bảng 3.
- func_decl (double d, Identifier id): khai báo một hàm từ giá trị một số
thực và định danh Identifier
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
Trang 24
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
- func_decl (Identifier id1, Identifier[] id): khai báo một hàm từ giá trị
một định danh Identifier và một mảng không rỗng định danh Identifier
- func_decl (Arith_symb ar,Identifier[] id): khai báo một hàm từ một
hoặc chuỗi các phép toán và mảng không rỗng các định danh id
5.2.2.7. Lớp pred_decl: khai báo một vị từ của bài toán SMT, được xây
dựng dựa trên (4) bảng 3
- pred_decl (Identifier[] id): khai báo một vị từ với giá trị của một dịnh
danh id
- pred_decl (Arith_symb ar, Identifier[] id): khai báo một vị từ từ một
(hoặc một chuỗi) các phép toán ar và một mảng các định danh id
- pred_decl (Identifier id1, Identifier[] id): khai báo một vị từ từ một
đinh danh id1 và mảng các định danh id
5.2.2.8. Lớp Term: được xây dựng dựa trên bảng 1.
- Term (varDecl v): khái báo một term từ khai báo của một biến v
- Term (double d): khai báo một term từ giá trị của một số thực d
- Term (Identifier i): khai báo một term từ một đinh danh i
- Term iteOperator (Formula f, Term t1, Term t2): toán tử “ite” của
Term
5.2.2.9. Lớp annotation: được xây dựng dựa trên (15) bảng 1, dùng để
khai báo một ghi chú trong bài toán SMT. Có hai cách khai báo như
sau:
- annotation (String attribute): khai báo ghi chú với chuỗi ký tự
attribute
- annotation (String attribute, String user_value): khai báo ghi chú với
chuỗi ký tự thuộc tính attribute và user_value
5.2.2.10. Lớp varDecl: Dùng để khai báo một biến trong bài toán SMT.
Được xây dựng dựa trên (8) bảng 1
- varDecl (String v): khai báo biến với chuỗi v
5.2.2.11. Lớp fvarDecl: được xây dựng dựa trên (9) bảng 1.
- fvarDecl (String fv): dùng để khai báo fvar với chuỗi fv
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
Trang 25
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.12. Lớp Arith_symb: dùng để khai báo một hoặc một chuỗi các tự
như đã được định nghĩa trong (10) bảng 1.
- Arith_symb (String s): khai báo một hoặc 1 chuỗi các ký tự.
5.2.2.13. Lớp Identifier: được xây dựng dựa trên (7) bảng 1, để đưa ra các
định danh cho bài toán SMT.
- Identifier (String simpleIdentifier): khai báo định danh từ một định
danh đơn giản (simple_identifier được định nghĩa trong (1) bảng 1)
- Identifier (String simleID, long num): khai báo định danh từ một định
danh đơn giản và một số nguyên)
- Identifier (String simpleId,long num1, long[] num2): khai báo định
danh từ một định danh đơn giản và một số nguyên cùng một mảng số
nguyên.
5.2.2.14. Lớp quant_var: được xây dựng dựa trên (5) của bảng 2.
- quant_var (varDecl var,Identifier id): khai báo quant_vả từ khai báo
biến var và định danh id.
Trên đây là các lớp và các hàm được xây dựng để hỗ trợ người dùng xây dựng
bài toán SMT trước khi gửi lên máy chủ. Để xây dựng được một bài toán SMT
đúng đắn bằng việc sử dụng các hàm trên, người dùng cần tuân thủ nghiêm ngặt
các định nghĩa, cách khai báo các thành phần đã được đưa ra ở trên. Chương trình
không hỗ trợ việc kiểm tra những gì người dùng nhập vào. Ví dụ với khai báo một
đối tượng của lớp Arith_symb, người dùng buộc phải đưa vào một hoặc một chuỗi
các ký tự thuộc tập các ký tự {=, >, <, &, @, #, +, -, *, /, %, |, ~ } Nếu người dùng
đưa vào sai chuỗi được thiết lập từ các ký tự trên, tệp tin chứa bài toán SMT vẫn
được sinh ra nhưng sẽ không đúng chuẩn và khi đó sẽ không có lời giải.
Ngoài ra, do một số lớp có sử dụng đối tượng của lớp khác, nên người dùng
cũng cần phải tuân thủ theo đúng việc khai báo các đối tượng của các lớp. Ví dụ,
trước khi có được một đối tượng của lớp Bench_attribute, người dùng cần phải
khai báo và xây dựng các đối tượng thuộc lớp Formula, annotation, funs_decl…
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
Trang 26
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.3. Phần máy trạm
Chức năng của hệ thống được cài đặt trên máy trạm là nhận về bài toán SMT
được máy chủ chuyển tới. Sau khi nhận được bài toán, hệ thống sẽ gọi chương trình để
giải bài toán ấy. Sau khi có được lời giải của bài toán, hệ thống sẽ gửi lại phía máy chủ
lởi giải đó. Trong trường hợp có máy trạm khác đã giải quyết xong bài toán ấy và gửi
lên máy chủ trước khi chương trình giải được cài đặt trên hệ thống giải quyết xong bài
toán, máy chủ sẽ gửi về một tín hiệu ngắt tiến trình đang chạy và không hệ thống sẽ
dừng chương trình đang chạy và không gửi gì về phía máy chủ nữa.
5.3.1. Cơ chế làm việc của máy trạm
Để đáp ứng nhu cầu nhận và giải liên tục các bài toán từ phía máy chủ, hệ thống
máy trạm cần có cơ chế phù hợp để vừa có thể nhận liên tục dữ liệu từ máy chủ, vừa
có thể thực thi việc giải bài toán (đã nhận xong từ phía máy chủ) và vừa có thể đảm
bảo việc gửi lại chính xác kết quả của bài toán tương ứng sau khi đã giải xong. Để đáp
ứng được yêu cầu này, hệ thống máy trạm cần được tổ chức các tác vụ thành các luồng
tiến trình khác nhau.
Trong ngôn ngữ lập trình Java, một luồng là một thuộc tính duy nhất [8] Nó là
đơn vị nhỏ nhất của đoạn mã có thể thi hành được mà thực hiện một công việc riêng
biệt. Một ứng dụng được viết bởi ngôn ngữ lập trình java có thể bao hàm nhiều luồng.
Mỗi luồng được đăng ký một công việc riêng biệt, mà chúng được thực thi đồng thời
với các luồng khác.
Đa luồng giữ thời gian nhàn rỗi của hệ thống thành nhỏ nhất. Điều này cho
phép các chương trình được viết bởi java có hiệu quả cao với sự tận dụng CPU là tối
đa. Mỗi phần của chương trình được gọi một luồng, mỗi luồng định nghĩa một đường
dẫn khác nhau của sự thực hiện.
Việc phân luồng được ứng dụng trong hệ thống máy trạm sẽ được đề cập cụ thể
hơn ở những phần sau của tài liệu.
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
Trang 27
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.3.2. Quy định giao tiếp với máy chủ
Do toàn bộ hệ thống được cài đặt trực tuyến, nên trường hợp nhận được nhiều
bài toán tại một thời điểm là hoàn toàn có thể xảy ra. Để xác định đúng kết quả của bài
toán tương ứng với bài toán nhận được trước đó, cần có một sự đánh dấu thứ tự cho
các bài toán ấy. Nhóm nghiên cứu đã đưa ra và thống nhất sử dụng mã sessionID được
tạo ra bởi máy chủ và được gửi kèm với nội dung.
Việc sử dụng mã sessionID còn giúp hệ thống tránh được sự nhầm lẫn giữa hai
hay nhiều bài toán cùng được gửi lên một lúc.
Quy trình kết nối giữu máy trạm và máy chủ sẽ như sau:
- Sau khi kết nối đến máy chủ, hệ thống cài đặt trên máy trạm sẽ gửi lời chào hỏi
đến máy chủ thông qua thẻ cặp thẻ chào hỏi như sau:
[Tên chương trình giải bài toán SMT]
- Máy chủ sau khi nhận được lời chào sẽ gửi đến nội dung của bài toán SMT mà
máy khách đã gửi lên yêu cầu giải. Việc gửi dữ liệu cũng được bắt đầu bằng thẻ
mở và kèm thêm mã sessionID trước đó. Mỗi dòng dữ liệu của bài toán
ấy gửi lên cũng sẽ kèm theo sessionID của bài toán đó cho đến khi thẻ đóng
được gửi lên:
sessionID |
sessionID | [nội dung dòng dữ liệu thứ 1]
….
sessionID | [nội dung dòng dữ liệu thứ n]
sessionID |
- Sauk hi nhận được dữ liệu từ tệp tin chứa bài toán SMT, hệ thống sẽ nhận trễ
thời gian giới hạn thực thi bài toán ấy. Việc nhận trễ thời gian giới hạn này
được quy định như sau:
sessionID |
sessionID | [trễ thời gian]
sessionID |
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
Trang 28
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
- Sau khi đã có dữ liệu đầy đủ của một bài toán hệt thống sẽ gọi chương trình giải
bài toán SMT để thực hiện việc giải bài toán đó. Sau khi có kết quả, hệ thống sẽ
gửi lại máy chủ theo quy chuẩn sau:
sessionID |
sessionID | [nội dung dòng kết quả trả về thứ 1]
…..
sessionID | [nội dung dòng kết quả trả về thứ 2]
sessionID |
- Sau khi gửi về kết quả, hệ thống sẽ vẫn tiếp tục nhận hoặc chờ bài toán tiếp
theo mà máy chủ sẽ gửi đến.
5.3.3. Hoạt động của hệ thống máy trạm
Với mỗi bài toán, hệ thống sẽ ghi vào một tệp tin có tên chính là sessionID của
bài toán ấy với phần mở rộng là smt. Và lời giải của bài toán đó cũng sẽ được lưu trữ
vào tệp tin có tên là sessionID.
Hiện tại, trên thế giới có nhiều các bộ giải bài toán SMT, tuy nhiên, trong
khuôn khổ luận văn này, hệ thống chỉ cài đặt và thử nghiệm trên hai bộ giải là yices
của SRI international và Z3 của Microsoft. Mỗi bộ giải sẽ được cài đặt trên một máy
trạm khác nhau cùng với hệ thống được xây dựng như đã trình bày ở trên. Do các bộ
giải là các chương trình chạy độc lập, nên hệ thống cần có lời gọi thực thi tới chúng.
Tuy ngôn ngữ lập trình Java có hỗ trợ việc gọi một lệnh của hệ điều hành, tuy nhiên để
có thể kết xuất được kết quả ra một tệp tin, hệ thống sử dụng quá trình chuyển hướng
kết xuất của chính hệ điều hành được sử dụng.
Do điệu kiện không cho phép, hiện tại hệ thống cài đặt trên máy trạm mới chỉ
được triển khai và kiểm thử trên các máy sử dụng hề điều hành windows và hệ hiều
hành có nhân Linux. Và để sử dụng được chuyển hướng kết xuất trên mỗi hệ điều
hành khác nhau, hệ thống đã xây dựng một tệp tin thực thi để hỗ trợ hệ thống gọi các
bộ giải SMT. Nội dung tệp tin hỗ trợ đó như sau:
- Đối với tệp tin .bat được cài đặt trên hệ điều hành windows
@echo off
[path]\yices.exe -e -tm %2 -smt [path]\%1.smt > [path]\%1.txt
echo done!
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
Trang 29
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
- Đối với tệp tin thực thi (tệp tin được thiết lập thuộc tính thực thi) được cài đặt
trên hệ điều hành Linux:
[path]/z3.exe /m /t:$2 /smt [path]/$1.smt > [path]/$1.txt
echo done!
- Ở đây, [path] là đường dẫn chỉ đến tệp tin (thư mục) của chương trình bộ giải
SMT. %1 sẽ được nhận vào là sesstionID của bài toán. %2 sẽ là tham số thời
gian ngắt của chương trình (được tính bằng giây).
- Với bộ giải yices, ta sử dụng tham số -e để đưa ra kết quả thỏa mãn nếu bài toán
đó khả thi. Tham số –tm để xác định trễ thời gian ngắt timeout, và tham số -smt
để xác định đầu vào của bộ giải là một tệp tin theo chuẩn SMT-LIB.
- Với bộ giải z3, tương tự ta cũng có các tham số /m tương đương với –e, /t:
tương đương với –tm và /smt tương đương với –smt của bộ giải yices.
- Cả hai bộ giải yices và z3 đều hỗ trợ cài đặt trên cả windows và Linux, vì vậy,
tùy vào điệu kiện của máy trạm, tệp tin thực thi sẽ được sửa cho phù hợp với hệ
điều hành cài đặt (không nhất thiết cài đặt yices trên hệ điều hành windows
hoặc z3 trên linux).
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.3.4. Các lớp của hệ thống máy trạm
5.3.4.1. Biểu đồ lớp của hệ thống
Hình 5.1: Biểu đồ lớp của hệ thống máy trạm
5.3.4.2. Lớp config
Lớp config chứa những quy định về địa chỉ, cổng và các thẻ giao tiếp với máy
chủ của máy trạm. Ngoài ra, lớp này còn quy định tên và đường dẫn của bộ giải được
cài đặt trên máy trạm. Việc xây dựng lớp config sẽ khiến cho việc quản lý cấu hình
cho hệ thống dễ dàng hơn.
5.3.4.3. Lớp sessionID
Để xác định được đúng dữ liệu của mỗi bài toán, tránh nhầm lẫn khi nhận nhiều
dòng dữ liệu từ nhiều bài toán cùng một lúc, và để gửi đúng lời giải cho bài toán đưa
ra, ngoài việc quy định mã sessionID cho mỗi bài toán, cần phải tổ chức dữ liệu hợp
lý. Đối với kết quả của một bài toán được gửi đến, ta chỉ cần đưa kết quả đó vào một
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
Trang 31
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
tệp tin với trên tệp tin là sessionID của bài toán đó, rồi gửi lại máy chủ session ID kèm
nội dung tệp tin đó. Còn đối với việc đọc dữ liệu đầu vào, hệ thống xây dựng một lớp
sessionID và có một mảng đối tượng của lớp dữ liệu này.
Lớp session ID sẽ bao gồm các thuộc tính sau:
- sessionID: là thuộc tính lưu lại sessionID
- content: Thuộc tính lưu lại nội dung của bài toán tương ứng với sessionID được
gửi lên.
- Timeout: thời gian ngắt của bài toán được gửi lên
- runSolver: tiến trình gọi một bộ giải để giải bài toán được gửi lên.
Mỗi đối tượng của lớp sessionID sẽ tương ứng với một bài toán được gửi lên.
Nội dung của bài toán sẽ được lưu trong thuộc tính content của lớp. Mỗi tiến trình xử
lý sẽ được khai báo bởi thuộc tính runSolver của lớp. Việc đưa tiến trình xử lý gọi bộ
giải để giải bài toán vào thành thuộc tính của lớp sessionID nhằm giải quyết vấn đề
ngắt tiến trình khi có yêu cầu từ phía máy chủ. Khi máy chủ nhận được kết quả của
cùng bài toán từ máy trạm có cài đặt bộ giải khác và gửi lên tín hiệu ngắt cho máy
trạm đang còn thực thi tiến trình giải bài toán ấy, thì việc ngắt tiến trình tương ứng với
sessionID mà máy chủ gửi lên sẽ được gọi.
5.3.4.4. Lớp Solver
Lớp này được xây dựng để thực hiện nhiệm vụ mở kết nối và có lời chào hỏi
trước khi thực hiện các thao tác khác sau đó.
5.3.4.5. Lớp ReadThread
Lớp này được xây dựng để đáp ứng việc đọc dữ liệu từ máy chủ gửi lên của
máy trạm. Sau khi kết nối được giữa máy chủ và máy trạm, hệ thống trên máy trạm
luôn đảm bảo việc lắng nghe các tín hiệu từ máy chủ. Để đảm bảo rằng, luôn có thể
nhận được nhiều dòng dữ liệu từ nhiều các bài toán khác nhau cùng một lúc.
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
Trang 32
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
Vấn đề kiểm soát bộ nhớ (mảng các đối tượng sessionID) sẽ được đánh dấu
bằng việc bài toán đã được giải xong hay chưa. Khi một sessionID mới được nhận về,
một phần tử của mảng các đối tượng sessionID mà có trạng thái rảnh sẽ được khởi tạo
và lưu lại. khi đó, trạng thái tương ứng của sessionID được bật là bận. Do việc giải
phóng bộ nhớ phụ thuộc vào việc bài toán được giải xong hay chưa, vì vậy trạng thái
của sessionID được khai báo trong lớp các đối tượng tiến trình ghi dữ liệu. Tức là
tương ứng với mảng các đối tượng của lớp sesstionID, sẽ có một mảng các đối tượng
ghi dữ liệu kết quả trả về được khởi tạo.
while (true){
_return = in.readLine(); //Đọc dữ liệu gửi lên từ phía máy chủ
if (_return.indexOf(config._tag_file)>=0){
openFile(_return); // Tạo mới một tệp tin lưu trữ bài toán mới
}
else if(_return.indexOf(config._closetag_file)>=0){ }
else if(_return.indexOf(config._tag_timeout)>=0){
sec[k].setTimeout(_return.substring(p+1));//đặt trễ thời gian cho bài
toán
closeFile(_return); //
}
else if(_return.indexOf(config._tag_destroy)>=0){
k = pos(_return); // xác định bài toán cần ngắt
interruptSolver(k); // Ngắt tiến trình xử lý bài toán
}
else {
k = pos(_return);
String content = _return.substring(p+1);
sec[k].content += content + "\n"; //lưu lại nội dung bài toá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 2010
Trang 33
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
Ngay khi tiếp nhận một bài toán mới (nhận được thẻ mở tệp tin), đối tượng của
lớp ghi dữ liệu tương ứng sẽ được đặt thuộc tính là bận. Việc quản lý thiết lập thuộc
tính bận hay rảnh này sẽ giúp cho hệ thống giới hạn được số lượng phần tử mảng
luồng đọc ghi dữ liệu. Trong trường hợp không quản lý trạng thái rảnh hay bận của các
đối tượng này, mỗi khi nhận được bài toán mới, hệ thống sẽ sinh ra một phần tử của
mảng các đối tượng ghi dữ liệu. Như vậy, các đối tượng ghi xong và được giải phóng
sẽ không được sử dụng lại, gây ra lãng phí tài nguyên.
Việc gọi tiến trình thực thi các bộ giải sẽ được thực hiện khi việc nhận dữ liệu
về bài toán được hoàn tất. Sau khi nhận được tham số trễ thời gian, hệ thống sẽ tiến
hành ghi dữ liệu ra tệp tin và gọi lệnh gọi bộ giải để giải quyết bài toán. Và khi đó, tiến
trình này sẽ được truyền cho đối tượng của lớp ghi dữ liệu để nhận và trả về kết quả.
String command = config._command + " " + sec[k].sectionID + " " +
sec[k].getTimeout();
sec[k].runSolver = Runtime.getRuntime().exec(command);
wt[k].setProc(sec[k].runSolver);
public ReadThread(Socket sk){
try {
for (int i = 0;i<config.Max_connection;i++) {
sec[i] = new section(); //khởi tạo mảng các đối tượng sessionID
wt[i] = new WriteThread(sk); //Khởi tạo mảng các đối tượng ghi dữ liệu
}
}
catch (IOException e){
e.printStackTrace();
}
}
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
Trang 34
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.3.4.6. Lớp WriteThread
Việc chờ kết quả để gửi trả về phía máy chủ cần được xây dựng thành một
luồng làm việc riêng biệt bởi đi kèm với việc gửi trả về kết quả, là việc trả về không
gian bộ nhớ cho thành phần đối tượng thuộc lớp sessionID. Ngoài ra, luồng này còn
luôn sẵn sàng để ngắt tiến trình đang thực hiện nếu có yêu cầu từ phía máy chủ gửi
lên. Ngoài ra, tính cần thiết phải đưa thành một luồng làm việc riêng biệt còn thể hiện
ở việc đáp ứng yêu cầu luôn lắng nghe dữ liệu gửi lên từ phía máy chủ.
Đối với việc gọi và thực thi bộ giải, sau khi dữ liệu được ghi vào tệp tin hoàn
tất, một tiến trình (thành phần của lớp sessionID) sẽ gọi công cụ giải được cài đặt trên
máy trạm. Khi nhận được tín hiệu “done!” xuất hiện từ luồng dữ liệu ra của tiến trình,
bài toán đã được giải xong và quá trình gửi dữ liệu về máy chủ được bắt đầu. Cùng với
đó, bộ nhớ chứa dữ liệu của bài toán được thực thi xong sẽ được giải phóng.
Việc ngắt một tiến trình khi nhận được yêu cầu ngắt từ phía máy chủ cũng được
đẩy sang phương thức của lớp này. Bởi lẽ, việc ngắt tiến trình còn liên quan đến việc
thiết lập trạng thái rảnh cho đối tượng.
5.4. Tổng kết
Mỗi hệ thống con của hệ thống giải bài toán SMT hiệu năng cao mang vai trò
riêng và đều rất quan trọng với hệ thống. Việc xây dựng tốt hệ thống máy khách sẽ
public void interruptSolver(){
this.proc.destroy(); //ngắt tiến trình đang xử lý
this.active = false; // trả về trạng thái rảnh
}
if (line.equals("done!")){
sendFile(); // gửi tệp tin kết quả
this.active = false; // thiết lập trạng thái rảnh cho đối tượng
this.stop();
}
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
Trang 35
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
giúp người dùng thuận tiện hơn nhiều trong quá trình xây dựng bài toán SMT. Còn đối
với hệ thống máy trạm, nếu được xây dựng tốt sẽ giúp cho hiệu năng xử lý bài toán
SMT sẽ tăng cao, giúp cho hiệu năng toàn hệ thống được cải thiệ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 2010
Trang 36
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
Chương 6. Cài đặt và thử nghiệm
6.1. Cài đặt
Đối với hệ thống máy khách, việc cài đặt sẽ phụ thuộc vào người sử dụng. Do
hệ thống được xây dựng như một thư viện người dùng, nên việc đưa vào những đoạn
mã chương trình của người dùng là rất dễ dàng. Hệ thống cũng hỗ trợ người dùng thực
thi trực tiếp nếu đã có tệp tin chứa nội dung bài toán SMT theo đúng chuẩn của SMT-
LIB
Đối với hệ thống máy khách. Java là một ngôn ngữ không phụ thuộc vào hệ
điều hành khi biên dịch nên hệ thống có thể cài đặt trên mọi hệ điều hành khác nhau.
Tuy nhiên, do hệ thống có sử dụng việc gọi tiến trình và kết xuất dữ liệu, nên việc cài
đặt trên hệ điều hành khác nhau cần có sự tùy chỉnh về mã lệnh cũng như tệp tin hỗ
trợ.
Trong phần thử nghiệm của nhóm phát triển, hệ thống máy khách được cài đặt
trên mộ máy tính có cấu hình phổ biến hiện nay và sử dụng nền hệ điều hành
windows. Phần máy trạm sẽ được cài đặt song song hai bộ giải trên hai máy khác
nhau: Một máy có nền windows 7 và một máy được cài sẵn hệ điều hành Linux
CenOS.
6.2. Bài toán thực nghiệm
Bài toán thực nghiệm được xây dựng nhằm kiểm tra tính đúng đắn cũng như
hiệu năng sử dụng của hệ thống.
6.2.1. Xây dựng bài toán SMT dựa trên các hàm API
Từ những hàm API của hệ thống được cài đặt trên máy khách, ta xây dựng một
chương trình sử dụng các hàm API đó để xây dựng một bài toán SMT hoàn chỉnh.
Việc sử dụng các hàm API được tuân thủ chặt chẽ theo luật và định nghĩa đã được nêu
trong phần kiến thức nền tảng và phần hướng đẫn các hàm API.
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
Trang 37
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
6.2.2. Thử nghiệm kết nối với máy chủ và toàn hệ thống
Để thử nghiệm hoạt động của toàn hệ thống, nhóm phát triển đã sử dụng một số
các tệp tin được xây dựng và đưa ra của SMT-LIB. Cụ thể
Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm
Tên tệp tin Kích thước Logic Trạng thái
Test1.SMT 1kb QF_UF sat
Test2.SMT 3kb QF_AX sat
Test3.SMT 1kb QF_AUFLIA sat
Test4.SMT 312kb QF_LIA sat
Test5.SMT 587kb QF_LIA unsat
Test6.SMT 270kb QF_LRA sat
Với tất cả các file dữ liệu kiểm thử được sử dụng như trên, ta tùy chỉnh để hệ
thống có thể chạy tối đa 6 kết nối cùng một lúc, số lượng kết nối chờ là 500. Hệ thống
cho thấy được khả năng đáp ứng tốt tất cả các yêu cầu của người dùng, đáp ứng kết
quả chính xác và thời gian đáp ứng nhanh chóng, hệ thống đưa về kết quả nhanh nhất
trong các bộ giải. Dựa vào những file dữ liệu để kiểm thử hệ thống như trên, ta có kết
quả của hệ thống về mặt thời gian như sau:
Bảng 9: Kết quả thời gian của thực nghiệm
Solver
Tên file
Z3 Yieces All
Test1.smt 1 1 1
Test2.smt 1 1 1
Test3.smt 1 1 1
Test4.smt 7 8 7
Test5.smt 20 16 16
Test6.smt 35 35 35
Kết quả trả về đối với từng bộ giải:
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
Trang 38
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
Bảng 10: Kêt quả trả về của thực nghiệm
Solver
Tên file
Z3 Yieces All
Test1.smt Sat Sat Sat
Test2.smt Sat Error Sat
Test3.smt Sat Sat Sat
Test4.smt Sat Sat Sat
Test5.smt Unsat Unsat Unsat
Test6.smt Time out TimeOut TimeOut
Từ kết hai bảng kết quả trên, ta có thể thấy rằng, hiệu quả đem lại của hệ thống
giải bài toán SMT là khá rõ ràng. Với những bài toán lớn, rõ ràng thời gian trả về của
các bộ giải là rất quan trọng. Tuy nhiên, với việc kết hợp nhiều bộ giải, vấn đề tối ưu
hóa thời gian giải bài toán đã được giải quyết. Qua những ví dụ 4, 5 ta thấy rằng thời
gian giải của các bộ giải đã có sự chênh lệch, và hệ thống đã đưa ra được thời gian trả
về kết quả tối ưu nhất.
Từ bảng 10, ta có thể thấy rằng, hầu hết các ví dụ đều có kết quả giống nhau.
Tuy nhiên, trong trường hợp kết quả trả về khác nhau, hệ thống vẫn đưa ra được kết
quả đúng đắn nhất cho người sử dụng. Ta thấy rằng, ở ví dụ 2, bộ giải yices đã không
thể đưa ra được kết quả (vì không hỗ trợ logic này), tuy nhiên bộ giải Z3 vẫn đưa ra
được kết quả cho bài toán. Còn ở ví dụ 6, ta thấy rằng, hệ thống đã hoạt động tốt với
chức năng thiết lập thời gian chờ tối đa của người dùng. Hệ thống đã ngắt và trả về cho
người sử dụng trạng thái của bài toán mà người dùng gửi lê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 2010
Trang 39
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
Kết Luận
Với hệ thống giải quyết bài toán SMT hiệu năng cao đã được xây dựng và trình
bày ở trên, việc giải quyết các bài toán SMT sẽ dễ dàng và mang lại nhiều hiệu quả
hơn rất nhiều cho người sử dụng. Tuy rằng, hệ thống mới chỉ được nghiên cứu và phát
triển trong những bước đầu hết sức đơn giản, nhưng những hiệu quả mang lại đã được
chứng minh rất rõ ràng trong phần thực nghiệm hệ thống. Do sử dụng nhiều bộ giải
cùng một lúc với cùng một bài toán nên ngoài khả năng tối ưu hóa mặt thời gian, hệ
thống còn có thể tối ưu hóa khả năng giải quyết bài toán SMT dưới nhiều chuẩn Logic,
nền lý thuyết khác nhau.
Với việc xây dựng hệ thống máy khách và máy trạm, cá nhân tôi đã có được
những hiểu biết nhất định về cấu trúc bài toán SMT cũng như việc phân luồng các tiến
trình để tận dụng được tối đa hiệu năng của máy. Tuy những hiểu biết và thành quả
còn nhiều hạn chế, nhưng đây là bước đầu để có thể phát triển hoàn thiện hệ thống giải
bài toán SMT hiệu năng cao về sau.
Việc nghiên cứu và phát triển hệ thống giải quyết tối ưu bài toán SMT một cách
đầy đủ, hoàn thiện hơn cần sự đầu tư về thời gian, trí óc và nhân sự. Rất mong sẽ có
những người cùng phát triển hệ thống về sau để hình thành nên hệ thống giải quyết bài
toán SMT tốt hơ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 2010
Trang 40
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
Hướng phát triển tiếp theo của hệ thống
Tuy hệ thống giải quyết bài toán SMT hiệu năng cao có những thành quả rất
khả quan, nhưng vẫn còn nhiều các hạn chế cần phải đầu tư và phát triển. Đối với toàn
hệ thống, hiện tại hệ thống chỉ hỗ trợ các bài toán thuộc chuẩn của SMT-LIB trong khi
đó, các bộ giải đều hỗ trợ những chuẩn đầu vào riêng. Vì vậy hệ thống cần phải phát
triển để có thể đáp ứng được nhiều các chuẩn đầu vào khác nữa để giải quyết. Hướng
giải quyết cho vấn đề này sẽ có hai cách thức: thứ nhất, hệ thống sẽ xây dựng một bộ
chuyển tất cả các đầu vào thành dạng chung SMT-LIB rồi phần bổ cho các máy trạm
xử lý, hoặc cách thứ hai có thể tìm và đưa cho đúng bộ giải hỗ trợ loại định dạng đầu
vào đó để xử lý.
Về phía máy khách, hiện tại hệ thống cài đặt trên máy khách chỉ hỗ trợ việc xây
dựng bài toán SMT hoàn toàn phải dựa trên định nghĩa và luật ngữ nghĩa được ghi
trong các bảng (1), (2), (3), (4), (5). Điều này khiến cho người dụng gặp nhiều khó
khăn khi buộc phải nhớ các luật ngữ nghĩa đó. Vì vậy, hệ thống cài đặt trên máy khách
cần xây dựng những hàm nhúng API đơn giản, hiệu quả và dễ dàng sử dụng hơn đối
với người dùng. Ngoài ra, hệ thống nên có một giao diện trực quan khi người dùng chỉ
sử dụng chức năng chỉ ra tập tin chứa bài toán SMT cần giải quyết.
Về phía máy trạm, do khuôn khổ luận văn có hạn, nên hiện tại hệ thống mới chỉ
sử dụng được hai bộ giải là yices và Z3, điều này khiến hệ thống sẽ có nhiều hạn chế
về hiệu năng xử lý các bài toán SMT được đưa vào. Vì vậy, hệ thống cần được nghiên
cứu, phát triển để có thể sử dụng nhiều hơn các bộ giải khác vào việc xử lý song song
các bài toán SMT. Ngoài ra, hệ thống cần phải nghiên cứu và phát triển trên nhiều nền
hệ điều hành khác nhau nữa. Hiện tại, việc gọi các bộ giải còn cần phải thông qua một
tệp tin thực thi của hệ điều hành, nên việc cài đặt hệ thống còn đang bị giới hạn trên
hai hệ điều hành là windows và linux.
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
Trang 41
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
Tài liệu tham khảo
[1] Roberto Sebastiani, Sanjit A. Seshia and Cesare Tinelli Clark Barrett, "Satisfiability
Modulo Theories," in Handbook of Satisfiability., 2008, ch. 12, p. 737.
[2] Leonardo de Moura and Nikolaj Bjorner, Satisfiability Modulo Theories: An Appetizer.
WA: Microsoft Research.
[3] N. Shankar, A Tutorial on Satisfiability Modulo Theories. CA: Computer Science
Laboratory.
[4] Silvio Ranise, Cesare Tinelli, The SMT-LIB Format: An Initial Proposal., 2006.
[5] Bruno Dutertre and Leonardo de Moura, The YICES SMT Solver.: Computer Science
Laboratory, SRI International.
[6] Aaron Stump, and Cesare Tinelli Clark Barrett. (2006) www.SMT-LIB.org.
[7] Silvio Ranise, Cesare Tinelli, The SMT-LIB Standard: Version 1.2., 2006.
[8] Cay S Horstmann and Gary Cornell, Core Java.: Pearson Education, 2008.
Các file đính kèm theo tài liệu này:
- 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.pdf