Luận văn Thạc sĩ Công nghệ thông tin: Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính

Chia sẻ: Tomjerry001 | Ngày: | Loại File: PDF | Số trang:65

Thêm vào BST

Báo xấu

26
lượt xem 2
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Mục tiêu nghiên cứu của đề tài "Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính" là đề xuất áp dụng phương pháp kiểm thử cặp đôi vào SMT Solver raSAT và đã cho kết quả cải tiến đáng kể hiệu quả của raSAT.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Luận văn Thạc sĩ Công nghệ thông tin: Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN QUÂN PHƯƠNG PHÁP TÍNH TOÁN KHOẢNG GIẢI CÁC RÀNG BUỘC KHÔNG TUYẾN TÍNH LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 2016
ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN VĂN QUÂN PHƯƠNG PHÁP TÍNH TOÁN KHOẢNG GIẢI CÁC RÀNG BUỘC KHÔNG TUYẾN TÍNH Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. TÔ VĂN KHÁNH Hà Nội – 2016
LỜI CAM ĐOAN Tôi xin cam đoan rằng, luận văn thạc sĩ công nghệ thông tin “Phương pháp tính toán khoảng giải các ràng buộc không tuyến tính.” là sản phẩm nghiên cứu của riêng cá nhân tôi dưới sự giúp đỡ rất lớn của Giảng viên hướng dẫn là TS. Tô Văn Khánh, không sao chép lại của người khác. Những điều đã được trình bày trong toàn bộ nội dung của luận văn này hoặc là của chính cá nhân tôi, hoặc là được tổng hợp từ nhiều nguồn tài liệu. Tất cả các tài liệu tham khảo đều có nguồn gốc rõ ràng và được trích dẫn hợp pháp. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định cho lời cam đoan của mình. Hà nội, tháng 10 năm 2016 Học viên Nguyễn Văn Quân
LỜI CẢM ƠN Trước tiên tôi xin bày tỏ lòng biết ơn chân thành và sâu sắc đến thầy giáo, TS. Tô Văn Khánh - người đã dành nhiều tâm huyết, tận tình chỉ bảo và giúp đỡ tôi trong suốt quá trình bắt đầu thực hiện đề tài cho đến khi tôi hoàn thành đề tài. Tôi xin gửi lời cảm ơn chân thành tới các thầy cô giáo khoa Công nghệ thông tin, trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội - nơi tôi đã theo học trong thời gian qua. Các thầy cô đã cung cấp cho tôi những kiến thức quý báu, tạo điều kiện tốt nhất cho tôi trong suốt quá trình học tập và nghiên cứu tại trường. Cuối cùng tôi xin chân thành cảm ơn những người thân trong gia đình, đặc biệt là bố mẹ tôi là nguồn động viên và ủng hộ tôi. Xin cảm ơn bạn bè cùng khóa, đồng nghiệp trong cơ quan đã giúp đỡ tôi trong quá trình học tập và nghiên cứu thực hiện luận văn này. Tuy rằng, tôi đã cố gắng hết sức trong quá trình làm luận văn nhưng không thể tránh khỏi thiếu sót, tôi rất mong nhận được những góp ý của thầy cô và các bạn. Hà nội, tháng 11 năm 2016 Học viên Nguyễn Văn Quân
MỤC LỤC 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 .........................................................................................................................1 Chương 1. GIỚI THIỆU ...............................................................................................3 1.1. Giải các ràng buộc đa thức ....................................................................................3 1.2. Ứng dụng của giải các ràng buộc đa thức .............................................................4 1.3. Các SMT giải ràng buộc toán học .........................................................................5 Chương 2. PHƯƠNG PHÁP TÍNH TOÁN KHOẢNG .............................................7 2.1. Giới thiệu về phương pháp tính toán khoảng ........................................................7 2.2. Phương pháp tính toán khoảng CI ........................................................................8 2.3. Phương pháp tính toán khoảng Affine Interval...................................................10 2.3.1. Dạng AF ...........................................................................................................11 2.3.2. Dạng AF1 .........................................................................................................13 2.3.2. Dạng AF2 .........................................................................................................15 2.4. Phương pháp tính toán khoảng C AI ...................................................................18 Chương 3. SMT SOLVER VÀ SMT SOLVER raSAT ...........................................23 3.1. SAT Solver ..........................................................................................................23 3.2. SMT Solver .........................................................................................................24 3.3. Thủ tục DPLL .....................................................................................................26 3.3.1 Thủ tục DPLL cho SAT ....................................................................................26 3.3.1 Thủ tục DPLL cho SMT ...................................................................................30 3.4. SMT Solver raSAT .............................................................................................32 Chương 4. CẢI TIẾN KỸ THUẬT KIỂM THỬ TRÊN SMT SOLVER raSAT ..41 4.1. Kiểm thử trên raSAT ...........................................................................................41 4.2. Kiểm thử cặp đôi .................................................................................................45 4.3 Kiểm thử cặp đôi trên raSAT ...............................................................................47
4.4 Thực nghiệm ........................................................................................................49 4.4.1 Kết quả raSAT tại các cuộc thi SMT – COMP .............................................49 4.4.2 raSAT 0.2 .......................................................................................................50 4.4.3 Benchmarks ...................................................................................................50 4.4.4 Kết quả thực nghiệm ......................................................................................51 KẾT LUẬN ..................................................................................................................53 TÀI LIỆU THAM KHẢO...........................................................................................54
BẢNG CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT STT Thuật ngữ viết tắt Thuật ngữ đầy đủ 1 SAT Satisfiability 2 SMT Satisfiability Modulo Theories 3 DPLL Davis Putnam Logemann Loveland 4 CNF Conjunctive Normal Form 5 CA Classical Interval 6 AI Affine Interval 7 AF Affine Form 8 AF1 Affine Form1 9 AF2 Affine Form2 10 CAI Chebyshev Approximation Interval 11 IA Interval Arithmetic 12 PID Proportional Integral Derivative Quantifier elimination - Cylindrical Algebraic 13 QE-CAD Decomposition 14 CAD Cylindrical algebraic decomposition 15 RAHD Real Algebra in High Dimensions 16 ICP Interval constraint propagation 17 VS Virtual substitution 18 APC Atomic polynomial constraint 19 ICC Interval constraint contraction
DANH MỤC HÌNH VẼ STT Số hiệu Tên hình vẽ 1 Hình 1 Đồ thị biểu diễn giá trị xấp xỉ Chebyshev của x 2 và x|x|. 2 Hình 2 Mô hình giải quyết vấn đề bằng SAT. 3 Hình 3 Phương pháp “Eager approach”. 4 Hình 4 Phương pháp “Lazy approach”. 5 Hình 5 Sơ đồ cơ chế hoạt động của thủ tục DPLL. 6 Hình 6 Kết quả của ràng buộc đa thức. 7 Hình 7 Kết quả kiểm thử của ràng buộc đa thức. 8 Hình 8 Kiến trúc của SMT Solver raSat. 9 Hình 9 Kết quả kiểm thử của ràng buộc đa thức. 10 Hình 10 Kiểm thử trong SMT Solver raSat.
DANH MỤC BẢNG STT Số hiệu Tên bảng 1 Bảng 1 Chọn giá trị cho biến trong khoảng dựa vào hệ số ưu tiên. 2 Bảng 2 Bảng giá trị đầu vào của các biến. 3 Bảng 3 Các ca kiểm thử sử dụng kỹ thuật kiểm thử cặp đôi. 4 Bảng 4 Các ca kiểm thử cặp đôi của 2 biến đầu vào. 5 Bảng 5 Các ca kiểm thử cặp đôi thêm các giá trị biến thứ ba. 6 Bảng 6 Các ca kiểm thử cặp đôi của ba biến lặp theo chiều dọc. 7 Bảng 7 Các ca kiểm thử cặp đôi của ba biến lặp theo chiều ngang. Bảng so sánh raSAT 0.2 và raSAT áp dụng kiểm thử cặp 8 Bảng 8 đôi. 9 Bảng 9 Kết quả raSAT 0.1 tại cuộc thi SMT - COMP 2014. 10 Bảng 10 Kết quả raSAT 0.2 tại cuộc thi SMT - COMP 2015. 11 Bảng 11 Kết quả raSAT 0.3 và 0.4 tại cuộc thi SMT - COMP 2016. Kết quả thực nghiệm của raSAT 0.2 và raSAT0.2 – 12 Bảng 12 Pairwise testing.
MỞ ĐẦU Với sự phát triển của công nghệ thông tin các sản phẩm phần mềm được xây dựng với các yêu cầu khắt khe về chất lượng và độ tin cậy. Đặc biệt là các hệ thống ứng dụng trong các ngành công nghệ cao như hàng không, vận tải, y tế... cần độ tin cậy và chính xác cao. Bởi chỉ một sai sót nhỏ của hệ thống có thể gây ra những tổn thất to lớn về tính mạng con người và thiệt hại kinh tế. Với nhu cầu như vậy các công cụ kiểm thử và kiểm chứng tự động ra đời sẽ giúp các nhà phát triển đảm bảo độ tin cậy và giảm chi phí sản xuất phần mềm. Hiện nay rất nhiều kỹ thuật được nghiên cứu và sử dụng để đảm bảo chất lượng của phần mềm. Hai kỹ thuật truyền thống đã và đang được sử dụng để đảm bảo chất lượng phần mềm là kiểm thử phần mềm (Software testing) và kiểm chứng phần mềm (Software verification). Tuy nhiên việc sử dụng các phương pháp kiểm thử chỉ làm giảm bớt lỗi của hệ thống mà không thể kết luận được hệ thống không có lỗi. Các phương pháp kiểm chứng đang được quan tâm số một trong việc chứng minh tính đúng đắn của hệ thống. Hiện nay các hướng nghiên cứu về SMT solver đang được quan tâm rộng rãi bởi chúng đóng vai trò quan trọng trong bài toán kiểm chứng phần mềm. SMT solver đóng vai trò là công cụ nền (backend engine) trong các công cụ kiểm chứng phần mềm. Các bài toán kiểm chứng được đưa về giải tính thỏa mãn (SAT/UNSAT) của các công thức logic bằng các công cụ SMT solver. Giải các ràng buộc đa thức toán học (Polynomial constraint) được ứng dụng nhiều trong phân tích hệ thống, kiểm chứng phần cứng và phần mềm, cụ thể như chứng minh tính bất biến của một chương trình hoặc phân tích kết quả của các hệ thống. Tất cả các ứng dụng trên cần được tự động và cần có công cụ để hỗ trợ để giải quyết bài toán. Giải các ràng buộc đa thức toán học là đưa ra kết luận ràng buộc đó là SAT hoặc UNSAT. 1
Ở luận văn này chúng tôi sẽ tập trung nghiên cứu về các kỹ thuật giải các ràng buộc phi tuyến tính (non-linear constraints) bằng phương pháp tính toán xấp xỉ (approximation methods) và thực nghiệm trên công cụ SMT Solver raSAT. Cụ thể mục tiêu của luận văn là nghiên cứu về các phương pháp tính toán khoảng (Interval Arithmetic) để giải các ràng buộc phi tuyến tính. Đồng thời luận văn cũng đề xuất áp dụng phương pháp kiểm thử cặp đôi vào SMT Solver raSAT và đã cho kết quả cải tiến đáng kể hiệu quả của raSAT. Luận văn bao gồm 4 chương, trong đó phần giới thiệu về giải các ràng buộc toán học và ứng dụng của giải các ràng buộc toán học sẽ nằm ở Chương 1. Chương 2: Giới thiệu về phương pháp tính toán khoảng và các kĩ thuật tính xấp xỉ (over approximation) gồm Classical Interval (CA), Affine Interval (AI) và Chebyshev Approximation Interval (CIA). Chương 3: Giới thiệu về SAT Solver và SMT Solver. Trình bày các kĩ thuật trong SMT Solver raSAT trong việc giải các ràng buộc đa thức. Chương 4: Trình bày về các kĩ thuật kiểm thử trong raSAT. Đề xuất kỹ thuật kiểm thử cặp đôi (pairwise) áp dụng cho raSAT. Phần kết luận: Kết luận và hướng nghiên cứu dự định trong tương lai. 2
Chương 1. GIỚI THIỆU 1.1. Giải các ràng buộc đa thức Giải các đa thức đóng vai trò quan trọng trong các lĩnh vực kiểm chứng (veriﬁcation) phần mềm, chứng minh tính dừng (proving termination), tính bất biến của chương trình (loop invariant generation) [28]. Do vậy việc đưa ra các phương pháp và công cụ để giải tự động các ràng buộc đa thức là yêu cầu thiết yếu. Kiểm thử không thể kiểm tra được tất cả các trường hợp có thể xảy ra của chương trình, do vậy việc chứng minh tính đúng của chương trình là một giải pháp thay thế. Để chứng minh chương trình không có lỗi có thể chuyển sang bài toán giải ràng buộc toán học. Sau đó sẽ thực hiện giải các ràng buộc toán học đó để đưa ra kết luận là chương trình có lỗi hoặc không có lỗi. Ràng buộc toán học có thể là đơn thức, đa thức tuyến tính hoặc phi tuyến tính. p p Đơn thức (Monomial): Một đơn thức được biểu diễn gồm v1 1 … vmm với các điều kiện m > 0, vi là biến, pi > 0 𝑣ới i ∈ {1 … m} và vi # vj với i , j ∈ {1 … m}, i # j . Một đơn thức là một hàm tuyến tính (linear) nếu m=1 và p=1. Đa thức (Polynomial): Định nghĩa Polynomial Atom, Constraint, Clause và CNF:  Một nguyên tử đa thức (polynomial atom) được xây dựng từ những toán tử quan hệ như ≥ , > 𝑣à = giữa các biểu thức toán học được xây dựng bằng cách áp dụng các phép cộng, trừ qua các biến và các số học.  Một ràng buộc đa thức (polynomial constraint) là một kết hợp logic của các nguyên tử đa thức.  Một mệnh đề là một ràng buộc đa thức bao gồm các phép tuyển hay phép phủ định của các đa thức nguyên tử. Một ràng buộc đa thức thuộc CNF nếu nó là một mệnh đề chuẩn tắc hội . 3
1.2. Ứng dụng của giải các ràng buộc đa thức Giải các ràng buộc đa thức ứng dụng trong việc phân tích, chứng minh tính đúng đắn của chương trình. Các ứng dụng cụ thể của giải các ràng buộc đa thức gồm:  Tự động phát hiện lỗi làm tròn và lỗi tràn số [3]: Trong khoa học máy tính số thực thường được sử dụng để xử lý. Tuy nhiên trong các hệ thống phần cứng cần tiếc kiệm bộ nhớ để có chi phí thấp và tốc độ cao nên các xử lý sẽ sử dụng số nhị phân để xử lý các tính toán. Việc chuyển đổi các thuật toán trên số thực về số nhị phân rất dễ cho các kết quả khác nhau do các lỗi làm tròn và tràn số. Do vậy việc kiểm soát các lỗi làm tròn, tràn số và các lỗi ở biên là vô cùng cần thiết. Ví dụ các ứng dụng sử lý tín hiệu số như bộ giải mã Mpeg, các thư viện OpenGL...  Chứng minh tính tự động [23]: Giải các ràng buộc toán học ứng dụng trong việc chứng minh tính dừng của thuật toán. Chứng minh tự động tính dừng của thuật toán là việc đánh giá thuật toán sẽ dừng trong bất kể trường hợp nào hoặc ngược lại thuật toán có thể là sẽ chạy mãi mãi.  Chứng minh tính đúng của chương trình [14]: Giải các ràng buộc tuyến tính hoặc phi tuyến tính ứng dụng trong việc chứng minh tính đúng của một chương trình. Chứng minh tính đúng của một chương trình là đi khẳng định chương trình luôn đúng với mọi thay đổi của các biến trong chương trình. Chuyển đổi một chương trình về các ràng buộc toán học và đi chứng minh ràng buộc đó là một cách gián tiếp đi chứng minh tính đúng của một chương trình.  Thiết kế bộ điều khiển cơ khí [15]: Bộ điều khiển (PID - Proportional Integral Derivative) được ứng dụng rộng rãi trong các điều khiển công nghiệp. Giải các ràng buộc toán học có thể ứng dụng trong việc thiết kế các bộ điều khiển phức tạp và cần độ tin cậy cao. 4
Ví dụ như công ty Fujitsu đã ứng dụng giải các ràng buộc phi tuyến tính trong việc thiết kế bộ điều khiển đọc/ghi của ổ cứng. Ví dụ 1.2.1: Phân tích tính dừng của chương trình sau: Biểu diễn chương trình trên thành các biểu thức logic như sau.  pt1 : 𝑦 ≥ 1 , 𝑥 ′ = 𝑥 − 1, 𝑦 ′ = 𝑦, 𝑧 ′ = 𝑧  pt2 : 𝑦 < 𝑧 , 𝑥 ′ = 𝑥 − 1, 𝑦 ′ = 𝑦, 𝑧 ′ = 𝑧 − 1  pt3 : 𝑦 ≥ 𝑧 , 𝑥 ′ = 𝑥, 𝑦 ′ = 𝑧 + 1, 𝑧 ′ = 𝑧 Nếu có thể giải được đa thức pt1 ˄ pt2 ˄ pt3 là UNSAT thì kết luận chương trình trên không bị lặp vô hạn. 1.3. Các SMT giải ràng buộc toán học Hiện nay các SMT giải các ràng buộc toán học có thể chia thành năm loại như sau:  QE-CAD: RAHD [19] (Real Algebra in High Dimensions) là một công cụ giải các ràng buộc phi tuyến tính trên tập số thực. RAHD phát triển dựa vào lý thuyết QE-CAD (Quantifier Elimination - Cylindrical Algebraic Decomposition) đề xuất bởi tác giả Tarski. 5
 Interval constraint propagation (ICP): ICP sử dụng phương pháp tính toán khoảng để tính sấp xỉ để phân tích xung đột. Các công cụ phát triển dựa vào ICP gồm RSOLVER [21], iSAT [4].  Bit-blasting: Là phương pháp chuyển đổi bài toán về các công thức logic mệnh đề và sử dụng SAT Solver để giải. Các công cụ phát triển dựa vào Bit-blasting gồm MiniSMT [5], UCLID [1].  Linearization: Là phương pháp chuyển đổi các ràng buộc đa thức về ràng buộc tuyến tính và sử dụng một SMT Solver để giải ràng buộc tuyến tính này. Các công cụ phát triển dựa vào phương pháp này gồm Barcelogic [9], CORD [2].  Virtual substitution (VS) [6]: Là thủ tục được sử dụng để nhúng với SMT Solver. Các công cụ phát triển dựa vào phương pháp này gồm SMT-RAT [13], Z3 [8]. Trong đó Z3 là công cụ kết hợp hai phương pháp VS và ICP để giải các ràng buộc tuyến tính. 6
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 Trong các tính toán số học đôi khi việc tìm được kết quả chính xác là việc vô cùng khó khăn, do vậy việc tính toán các giá trị gần đúng với kết quả thực tế là một giải pháp được đưa ra. Phương pháp tính toán khoảng (Interval Arithmetic - IA) sử dụng để tìm cận trên và cận dưới của các ràng buộc dựa trên phương pháp tính xấp xỉ (approximation methods). Phương pháp này được áp dụng cho giải các bài toán để tìm ra kết quả gần đúng với mức độ lỗi có thể chấp nhận được. Ví dụ: Với phương trình x 2 + x − 6 = 0 ta dễ dàng sử dụng công thức biến đổi trong trương trình trung học cơ sở để tìm được nghiệm của phương trình là x1 = −3 và x2 = +2. Tuy nhiên với một số bài toán không thể tìm được nghiệm chính xác của bài toán, ví dụ với phương trình x 2 − 2 = 0 thì nghiệm được biểu diễn √2. Như vậy nếu chỉ sử dụng các kiểu số cơ bản thì không thể biểu diễn chính xác tất cả các giá trị của bài toán mà bắt buộc phải làm tròn để lấy giá trị xấp xỉ. Do vậy các nhà khoa học đã đưa ra lý thuyết tính toán khoảng (Interval Arithmetic -IA) để kiểm soát lỗi làm tròn trong các tính toán, do vậy kết quả thu được sẽ được kiểm soát về độ tin cậy. Các số thực x, y trong phương pháp tính toán khoảng được biểu diễn như sau:  x = [ x , x ], y = [ y , y ], Trong đó x = min( x ∈ x ) , y = min( y ∈ y ) là cận dưới lần lượt của x và y, x = max ( x ∈ x ), y = max ( y ∈ y) là cận trên lần lượt của x và y .  x = y nếu x = y và x = y  x < 𝑦 nếu x < y  x > 𝑦 nếu y > y  x là số thực đơn (single real number) nếu x = x. Ví dụ 0 = [ 0 , 0 ] 7
Trong phương pháp tính toán khoảng có hai kĩ thuật chính gồm Classical Interval (CI) [20] và Affine Arithmetic (AF) [24]. Ngoài ra còn một số kĩ thuật được phát triển từ hai kĩ thuật trên gồm AF, AF1, AF2 [17] và Chebyshev Affine Interval (C AI) [27]. Chi tiết các kĩ thuật sẽ được trình bày lần lượt ở phần tiếp theo của luận văn. 2.2. Phương pháp tính toán khoảng CI Kĩ thuật tính toán khoảng Classical Interval (CI) [20] được tác giả Ramnon E.Moore giới thiệu vào năm 1960. Ý tưởng chính của kĩ thuật này là đặt giới hạn lỗi làm tròn trong các tính toán số học bằng cách biểu diễn mỗi giá trị trong CI bởi một khoảng giới hạn. Các khoảng giới hạn này sẽ được sử dụng để tính toán thay thế cho giá trị gốc. Kĩ thuật Classical Interval được định nghĩa như sau. Định nghĩa 2.2.1: Một Classical Interval của x là một khoảng x = [ xl , xu ] trong đó xl ≤ x ≤ xu . Định nghĩa 2.2.2: Các phép toán cơ bản trong Classical Interval gồm ☉= { + , − , × ,÷ } được định nghĩa như sau.  [ x l , x u ] + [ yl , yu ] = [ x l + yl , x u + yu ]  [ x l , x u ] − [ yl , yu ] = [ x l − yu , x u − yl ]  [xl , xu ] × [ yl , yu ] = [min(xl yl , xl yu , xu yl , xu yu ), max(xl yl , xl yu , xu yl , xu yu ) ] 1 1  [xl , xu ] ÷ [ yl , yu ] = [ xl , xu ] × [ , ] nếu 0 ∉ [ yl , yu ] yl yu Bổ đề 2.2.3:Với x = [ xl , xu ], y = [ yl , yu ] thì z = x ☉ y ∈ [ xl , xu ] ☉ [ yl , yu ] , trong đó ☉= { + , − , × ,÷ }. Ví dụ 2.2.4:Cho x = [ 1 ,4 ] , y = [ 3 ,6 ] tính z = x ☉ y với ☉={ + , − , × ,÷ }.  Phép cộng z = x + y : z = [ 1 ,4 ] + [ 3 , 6 ] = [ −1 + 3 , 4 + 6] = [ 2 , 10] 8
Kết luận 𝑧 = [ 2 , 10]  Phép trừ z = x − y : z = [ 1 ,4 ] − [ 3 , 6 ] = [ −1 − 6 , 4 − 3] = [ −7 , 1] Kết luận 𝑧 = [ −7 , 1]  Phép nhân z = x × y : z = [ 1 ,4 ] × [ 3 , 6 ] = [ min (−1 × 3, −1 × 6, 4 × 3, 4 × 6), max(−1 × 3, −1 × 6, 4 × 3, 4 × 6) ] = [ min(−3, −6, 12, 24), max(−3, −6, 12, 24)] = [ −6 , 24 ] Kết luận z = [ −6 , 24 ]  Phép chia z = x ÷ y : z = [ 1 ,4 ] ÷ [ 3 , 6 ] 1 1 = [ 1 ,4 ] × [ , ] 3 6 1 1 4 2 1 1 4 2 = [ min (− , − , , ) , max (− , − , , )] 3 6 3 3 3 6 3 3 1 4 =[− , ] 6 3 1 4 Kết luận z = [ − , ] 6 3 Hạn chế của Classical Interval là kết quả tính toán có thể rộng hơn kết quả thực tế mong muốn trong các phép tính lớn. Khi mà kết quả ở một trạng thái là đầu vào của trạng thái tiếp theo. Nguyên nhân là do các đầu vào ban đầu của CI là độc lập và không phục thuộc nhau do đó trong trường hợp các tính toán có liên quan tới các đầu vào phục thuộc nhau sẽ làm kết quả của phép toán sai lệnh so với kết quả thực tế. Ví dụ với phép toán trừ ( − ) , sử dụng công thức ở 2.2.2 với x = [2 , 5] kết quả thu được là x − x = [2 , 5] − [2 , 5] = [−3 , 3] . Do kĩ thuật CI không thể nhận biết được hai đầu vào là giống nhau nên sẽ biểu diễn hai giá trị với 9
cùng một khoảng do vậy dẫn đến kết quả là [−3 , 3] thay vì kết quả chính xác là [0 , 0] . Ví dụ với các phép toán nhiều hơn hai đầu vào cho x = [4 , 6] tính x(10 − x) . Sử dụng các công thức ở 2.2.2 như sau : 10 − x = [10 , 10] − [4 , 6] = [4 , 6] x(10 − x) = [4 , 6] × [4 , 6] = [16 , 36] Kết quả chính xác là [24 , 25] thay vì [16 , 36] . Do kĩ thuật Classical Interval không nhận biết được hai đầu vào của phép nhân là x và (10 − x) phụ thuộc nhau nên dẫn đến khoảng kết quả thu được rộng hơn rất nhiều so với khoảng kết quả thực tế của phép toán. Như vậy với các phép tính có nhiều hơn hai đầu vào không độc lập nhau sẽ dẫn đến lỗi tính toán và kết quả thu được rộng hơn mong muốn. Để khắc phục nhược điểm này của Classical Interval phần tiếp theo của luận văn sẽ giới thiệu phương pháp tính toán khoảng Affine Interval (AI). 2.3. Phương pháp tính toán khoảng Affine Interval Kĩ thuật tính toán khoảng Affine Interval (AI) [24] được giới thiệu bởi hai tác giả Comba và Stolfi vào năm 1993. Kĩ thuật AI được phát triển từ kĩ thuật CI bằng cách tự động theo dõi việc làm tròn số để giảm thiểu các lỗi trong mỗi bước tính toán. Ngoài ra để khắc phục nhược điểm các đầu vào độc lập của CI như ở trên, AI có thể theo dõi mỗi tương tác giữa các thành phần của đa thức. Mục đích của AI là cung cấp các giới hạn tính toán để đảm bảo cho các kết quả tính toán có lỗi đủ nhỏ, đặc biệt trong các chuỗi tính toán lớn kĩ thuật AI sẽ phát huy được lợi thế này. AI được đánh giá là kĩ thuật có độ chính xác cao, tuy nhiên kĩ thuật này phức tạp và tốn nhiều chi phí cho việc áp dụng vào các ứng dụng thực tế. Các biến trong Affine Interval được biểu diễn bởi số thực ɛ (noise symbols) có giá trị trong khoảng [−1 , 1]. Các tính toán trong Affine Interval 10
cho phép giữ giá trị ban đầu của các tính toán dựa trên kí tự ɛ và cải thiện độ chính xác khi thực hiện phép trừ (−). Ví dụ x ∈ (1 , 3), x được biểu diễn x = 2 + ɛ, khi đó x = (2 + ɛ) − (2 + ɛ) có giá trị hợp lý bằng 0. Affine Interval được phát triển dưới các dạng Affine Forms (AF) bằng cách xác định số lượng biến để theo dõi mức độ lỗi khi thực hiện lấy xấp xỉ hoặc làm tròn trong phép nhân. Phần tiếp theo của luận văn sẽ giới thiệu các dạng của Affine Interval gồm AF, AF1, AF2. 2.3.1. Dạng AF Định nghĩa 2.3.1: Dạng AF [17] của biến x biểu diễn như sau: n ẍ = a0 + ∑ ai ɛi i=1 n n Với x ∈ ( a0 − ∑|ai | , a0 + ∑|ai | ) , ɛi ∈ [−1 , 1] (noise symbols) i=0 i=0 Định nghĩa 2.3.2: Cho x, y biểu diễn lần lượt dưới dạng AF như sau: n ẍ = a0 + ∑ ai ɛi i=1 n ÿ = b0 + ∑ bi ɛi i=1 Các phép toán của dạng AF gồm ☉={ + , − , × ,÷ } như sau: n ẍ + ÿ = (a0 + b0 ) + ∑(ai + bi )ɛi i=1 n ẍ − ÿ = (a0 − b0 ) + ∑(ai − bi )ɛi i=1 n n n ẍ × ÿ = (a0 b0 ) + ∑(a0 bi − b0 ai )ɛi + ( ∑|ai | ) ( ∑|bi | ) ɛn+1 i=1 i=1 i=1 11