Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT - Từ mô hình Toán học đến Mã hoá Logic

Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Từ mô hình Toán học đến Mã hoá Logic Kiều Văn Tuyên Phòng Thí nghiệm Hệ thống Nhúng Ngày 2 tháng 5 năm 2025 Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 1 / 37.

Vận trù học (OR) và Tối ưu hóa Toán học Vận trù học (Operations Research) Tối ưu hóa Toán học (Mathematical Optimization) Lập trình Tuyến tính (LP) Lập trình Nguyên (ILP) Lập trình Nguyên Hỗn hợp (MIP) Lập trình Ràng buộc (CP) Giải bài toán Thỏa mãn (SAT) Thỏa mãn theo Lý thuyết (SMT) Ràng buộc tuyến tính Logic và ràng buộc Hình: Mối quan hệ giữa Vận trù học và các kỹ thuật tối ưu Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 2 / 37.

Vận trù học (OR) và Tối ưu hóa Toán học Vận trù học (Operations Research - OR): Khoa học về việc ra quyết định tối ưu trong các hệ thống phức tạp. Sử dụng các mô hình toán học và thuật toán để tìm giải pháp tốt nhất cho các vấn đề thực tế. Tối ưu hóa Toán học (Mathematical Optimization): Trái tim của OR. Tìm cách tối đa hóa hoặc tối thiểu hóa một hàm mục tiêu (objective function) dưới một tập các ràng buộc (constraints). Mô hình hóa là chìa khóa: Biểu diễn vấn đề thực tế thành một mô hình toán học. Các loại mô hình phổ biến chúng ta sẽ tìm hiểu: Lập trình Tuyến tính (Linear Programming - LP) Lập trình Nguyên (Integer Linear Programming - ILP) Lập trình Nguyên Hỗn hợp (Mixed Integer Linear Programming - MIP) Liên hệ với Logic: Giới thiệu Lập trình Ràng buộc (CP) và Giải bài toán Thỏa mãn (SAT/SMT) → cách tiếp cận mạnh mẽ khác, đặc biệt cho các vấn đề có cấu trúc logic. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 3 / 37.

Lập trình Tuyến tính (LP): Định nghĩa I Định nghĩa (Lập trình Tuyến tính) Một bài toán LP tìm cách tối ưu hóa (tối đa hóa hoặc tối thiểu hóa) một hàm mục tiêu tuyến tính dưới một tập các ràng buộc tuyến tính (bất đẳng thức hoặc đẳng thức). Các biến quyết định (decision variables) có thể nhận giá trị thực (liên tục). Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 4 / 37.

Lập trình Tuyến tính (LP): Định nghĩa II Dạng tổng quát: max (hoặc min) c1x1 + c2x2 + · · · + cnxn (Hàm mục tiêu) s.t. a11x1 + a12x2 + · · · + a1nxn ≤ (hoặc ≥, =)b1 a21x1 + a22x2 + · · · + a2nxn ≤ (hoặc ≥, =)b2 ... am1x1 + am2x2 + · · · + amnxn ≤ (hoặc ≥, =)bm x1, x2, . . . , xn ≥ 0 Trong đó: xj là biến quyết định, cj, aij, bi là các hằng số đã biết. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 5 / 37.

LP: Dạng chuẩn (Standard Form) và Ý nghĩa Hình học I Dạng chuẩn (Thường dùng cho thuật toán Simplex): Tối đa hóa hàm mục tiêu. Tất cả ràng buộc là đẳng thức (=). (Sử dụng biến bù/slack/surplus để chuyển đổi ≤, ≥). Tất cả biến không âm (≥ 0). Ý nghĩa Hình học (2D/3D): Mỗi ràng buộc tuyến tính định nghĩa một nửa không gian. Tập hợp các điểm thỏa mãn tất cả ràng buộc tạo thành miền khả thi (feasible region) - là một đa diện lồi (convex polytope). Kết quả quan trọng: Nếu bài toán LP có nghiệm tối ưu hữu hạn, thì ít nhất một nghiệm tối ưu nằm tại một đỉnh (vertex) của miền khả thi. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 6 / 37.

LP: Dạng chuẩn (Standard Form) và Ý nghĩa Hình học II x1 x2 (0, 0)A (5, 0) B (4, 2) C (2, 5) D (0, 4)E z = 10 z = 12 z = 14 z = 16 ∇z Miền khả thi Đường đồng mức Nghiệm tối ưu x1 ≥ 0 x2 ≥ 0 x1 + 2x2 ≤ 12 2x1 + x2 ≤ 10 x1 + x2 ≤ 8 Hàm mục tiêu: max z = 3x1 + 4x2 Hình: Minh họa hình học của bài toán Lập trình tuyến tính Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 7 / 37.

LP: Phương pháp giải và Ví dụ I Các phương pháp giải chính: Thuật toán Đơn hình (Simplex Algorithm - George Dantzig, 1947): Di chuyển từ đỉnh này sang đỉnh kề khác của miền khả thi, liên tục cải thiện giá trị hàm mục tiêu cho đến khi đạt tối ưu. Rất hiệu quả trong thực tế, mặc dù trường hợp xấu nhất có thể là hàm mũ. Phương pháp Điểm trong (Interior-Point Methods - Karmarkar, 1984): Di chuyển bên trong miền khả thi hướng về phía nghiệm tối ưu. Có độ phức tạp thời gian đa thức được chứng minh. Thường hiệu quả cho các bài toán LP rất lớn. Solvers: Các phần mềm chuyên dụng (CPLEX, Gurobi, OR-Tools LP Solver, GLPK...) triển khai các thuật toán này. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 8 / 37.

LP: Phương pháp giải và Ví dụ II Ví dụ: Bài toán Lập kế hoạch sản xuất Một xưởng sản xuất 2 loại sản phẩm A và B. Lợi nhuận mỗi sản phẩm là $3 và $5. Thời gian gia công trên máy 1 là 1h (A) và 2h (B). Thời gian gia công trên máy 2 là 1h (A) và 1h (B). Máy 1 có 4h làm việc, máy 2 có 3h. Hỏi cần sản xuất bao nhiêu sản phẩm mỗi loại để lợi nhuận tối đa? (Mô hình hóa thành LP và giải) Biến quyết định: x1 (số sản phẩm A), x2 (số sản phẩm B). Hàm mục tiêu: max z = 3x1 + 5x2. Ràng buộc: x1 + 2x2 ≤ 4 (Máy 1) x1 + x2 ≤ 3 (Máy 2) x1, x2 ≥ 0 Kết quả: x1 = 2, x2 = 1, z = 11 Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 9 / 37.

Lập trình Nguyên (ILP): Định nghĩa và Tại sao? I Định nghĩa (Lập trình Nguyên) Một bài toán ILP tương tự như LP, nhưng yêu cầu tất cả các biến quyết định phải nhận giá trị nguyên. Binary ILP (BILP): Các biến chỉ nhận giá trị 0 hoặc 1. Tại sao cần ILP? Mô hình hóa các quyết định rời rạc: Quyết định Có/Không (Yes/No): Xây dựng nhà máy? Đầu tư dự án? (Biến 0/1) Đếm số lượng: Số lượng công nhân cần thuê? Số xe cần điều động? (Biến nguyên) Lựa chọn logic: Nếu chọn A thì phải chọn B? Chỉ chọn tối đa K phương án? Nhiều vấn đề thực tế không thể mô tả chỉ bằng các biến liên tục của LP. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 10 / 37.

Lập trình Nguyên (ILP): Định nghĩa và Tại sao? II Quyết định nhị phân (0/1) (Biến nhị phân x ∈) ON x = 1 OFF x = 0 Ví dụ: - Xây/không xây nhà máy - Tuyển/không tuyển nhân viên - Chọn/không chọn sản phẩm Hình: Quyết định nhị phân trong Lập trình Nguyên Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 11 / 37.

Lập trình Nguyên (ILP): Định nghĩa và Tại sao? III Quyết định đếm (Biến nguyên y ∈ Z+) 0 1 2 3 4 y = 3 Ví dụ: - Số nhân viên cần thuê - Số xe cần điều động - Số lượng sản phẩm đặt hàng Hình: Quyết định đếm trong Lập trình Nguyên Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 12 / 37.

ILP: Thách thức và Phương pháp giải I Thách thức lớn: Giải ILP khó hơn rất nhiều so với LP (NP-hard). Tại sao? Miền khả thi không còn lồi (chỉ là tập các điểm nguyên rời rạc). Thuật toán Simplex không áp dụng trực tiếp (nghiệm LP tối ưu có thể không nguyên). Làm tròn nghiệm LP thường không cho nghiệm ILP tối ưu, thậm chí có thể không khả thi. Không gian tìm kiếm lớn (tổ hợp). Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 13 / 37.

ILP: Thách thức và Phương pháp giải II x y x + 7y = 17.5 Linear opt. solution = 25 (0, 2.5) Integer opt. solution = 23 (3, 2) (0, 2) Hình: Minh họa sự khác biệt giữa nghiệm LP tối ưu và nghiệm ILP tối ưu Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 14 / 37.

ILP: Thách thức và Phương pháp giải III Phương pháp giải chính: Nhánh và Cận (Branch and Bound - B&B): Chia bài toán thành các bài toán con nhỏ hơn (branching) bằng cách thêm ràng buộc vào biến chưa nguyên. Giải LP tương ứng (LP relaxation) tại mỗi nút để lấy cận (bounding). Cắt bỏ (pruning) các nhánh không hứa hẹn. Mặt phẳng cắt (Cutting Planes): Thêm các ràng buộc tuyến tính mới (cuts) để cắt bỏ phần không nguyên của miền LP mà không loại bỏ điểm nguyên nào. Kết hợp: Branch and Cut (B&B + Cutting Planes) là phương pháp phổ biến nhất trong các solver hiện đại. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 15 / 37.

ILP: Ví dụ I Ví dụ: Bài toán Cái túi 0/1 (0/1 Knapsack Problem) Có n món đồ, mỗi món đồ j có trọng lượng wj và giá trị vj. Một cái túi có sức chứa tối đa W. Chọn các món đồ để cho vào túi sao cho tổng giá trị là lớn nhất mà không vượt quá sức chứa. Mô hình ILP (Binary): Biến quyết định: xj = 1 nếu chọn món đồ j, xj = 0 nếu không chọn (j = 1..n). Hàm mục tiêu: max �n j=1 vjxj Ràng buộc: �n j=1 wjxj ≤ W Biến: xj ∈ Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 16 / 37.

ILP: Ví dụ II Túi Sức chứa: W = 15 Đồ 1 w1 = 4 v1 = 10 x1 = 1 Đồ 2 w2 = 3 v2 = 7 Đồ 5x2 = 1 w5 = 8 v5 = 15 x5 = 1 Đồ 3 w3 = 6 v3 = 9 x3 = 0 Đồ 4 w4 = 7 v4 = 8 x4 = 0 chọn chọn chọn không chọn không chọn Tổng trọng lượng: 4 + 3 + 8 = 15 ≤ W Tổng giá trị: 10 + 7 + 15 = 32 Bài toán Cái túi 0/1 Hình: Minh họa bài toán Cái túi 0/1 với n món đồ, mỗi món có trọng lượng wj và giá trị vj Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 17 / 37.

Lập trình Nguyên Hỗn hợp (MIP): Định nghĩa và Tính linh hoạt I Định nghĩa (Lập trình Nguyên Hỗn hợp) Một bài toán MIP tương tự như ILP, nhưng cho phép một số biến là nguyên và một số biến là liên tục (thực). Tại sao MIP lại mạnh mẽ? Kết hợp được cả quyết định rời rạc (biến nguyên) và các đại lượng liên tục (biến thực). Mô hình hóa được rất nhiều bài toán thực tế phức tạp trong sản xuất, logistics, tài chính, năng lượng... Ví dụ: Quyết định xây nhà máy (0/1) và lượng sản phẩm sản xuất tại đó (liên tục). Quyết định bật/tắt máy phát điện (0/1) và công suất phát (liên tục). Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 18 / 37.

Lập trình Nguyên Hỗn hợp (MIP): Định nghĩa và Tính linh hoạt II Lập lịch công việc (thời gian bắt đầu có thể liên tục) với ràng buộc về số lượng công nhân (nguyên). M1 M2 M3 P1 P2 P3 M1 M2 M3 y1 y2 y3 Nhà máy 1: x1 = 1 Nhà máy 2: x2 = 0 0 ≤ y1 ≤ 100;0 ≤ y2 ≤ 80; 0 ≤ y3 ≤ 120 y1 + y2 + y3 ≤ 200 · x1 (Sản lượng chỉ khả thi khi nhà máy được xây) Mô hình MIP: xj ∈ (biến nhị phân) yi ≥ 0 (biến liên tục) � j xj ≤ 1 (chọn tối đa 1 nhà máy) yi ≤ M · xj (liên kết biến) Hình: Minh họa bài toán MIP với quyết định xây dựng nhà máy (nhị phân) và sản lượng sản xuất (liên tục) Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 19 / 37.

Từ Tối ưu hóa đến Logic Thoả mãn I LP/ILP/MIP tập trung vào tối ưu hóa hàm mục tiêu dưới ràng buộc số học (chủ yếu là tuyến tính). Tuy nhiên, nhiều bài toán có cấu trúc logic phức tạp hoặc các ràng buộc phi tuyến tính khó biểu diễn trực tiếp bằng (M)ILP. Lập trình Ràng buộc (Constraint Programming - CP): Một cách tiếp cận khác, tập trung vào việc tìm một lời giải khả thi thỏa mãn một tập các ràng buộc đa dạng (logic, số học, tổ hợp...). Thường sử dụng các kỹ thuật lan truyền ràng buộc (constraint propagation) và tìm kiếm. Giải bài toán Thỏa mãn Mệnh đề (SAT): Trường hợp đặc biệt của CP, chỉ dùng biến Boolean (0/1) và ràng buộc logic mệnh đề (thường ở dạng CNF - Conjunctive Normal Form). Cực kỳ hiệu quả cho các bài toán có cấu trúc logic mạnh (kiểm chứng mạch, quy hoạch...). Giải bài toán Thỏa mãn Mệnh đề (SAT): Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 20 / 37.

Từ Tối ưu hóa đến Logic Thoả mãn II Mở rộng SAT bằng cách tích hợp các "lý thuyết"nền (theories) như: Số học tuyến tính (Linear Arithmetic), Mảng (Arrays), Bit-vectors... Cho phép biểu diễn các ràng buộc phức tạp hơn SAT nhưng vẫn tận dụng được sức mạnh của SAT solvers. Liên kết: Quyết định 0/1 trong (M)ILP tương ứng với biến Boolean trong SAT/SMT. Ràng buộc logic có thể mã hóa thành mệnh đề SAT hoặc ràng buộc SMT. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 21 / 37.

Từ Tối ưu hóa đến Logic Thoả mãn III MIP CP SAT SMT Tối ưu với biến nguyên và liên tục Các ràng buộc toán học phức tạp Biến Boolean SAT + lý thuyết mở rộng Sắp xếp & lập lịch Mã hóa logic ràng buộc VD: TSP, Knapsack, bin packing VD: Kiểm chứng phần mềm/phần cứng VD: Sudoku, N-queens VD: Mã hóa Boolean phức tạp MIP CP SAT SMT Mối quan hệ giữa các phương pháp tối ưu hóa và thỏa mãn Hình: Sơ đồ Venn thể hiện quan hệ giữa MIP, CP, SAT và SMT Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 22 / 37.

Bài toán: Simple Assembly Line Balancing with Power Peak Minimization (SALB3PM) I Hình: Minh họa dây chuyền lắp ráp và công suất tiêu thụ (Nguồn: Py et al.) Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 23 / 37.

Bài toán: Simple Assembly Line Balancing with Power Peak Minimization (SALB3PM) II Bối cảnh: Cân bằng dây chuyền lắp ráp (Assembly Line Balancing - ALB) là bài toán OR kinh điển trong sản xuất. Cho tập các tác vụ (tasks) với thời gian thực hiện và quan hệ thứ tự (precedence). Chia các tác vụ vào các trạm làm việc (workstations). Ràng buộc: Tổng thời gian tác vụ/trạm ≤ thời gian chu kỳ (cycle time), tuân thủ thứ tự. Biến thể SALB3PM (Py et al. [3, 4, 6, 7]): Mỗi tác vụ tiêu thụ một lượng năng lượng (power) nhất định khi chạy. Mục tiêu: Tìm một cách xếp lịch (phân công tác vụ vào trạm VÀ xác định thời điểm bắt đầu) sao cho công suất đỉnh (peak power) - tổng công suất tiêu thụ tại bất kỳ thời điểm nào - là nhỏ nhất. Lý do: Giảm chi phí điện năng, bảo vệ môi trường, tăng độ ổn định hệ thống. Đây là một bài toán tối ưu hóa tổ hợp khó. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 24 / 37.

Mô hình ILP cho SALB3PM (Py et al. [3] - Hình 4) Hình: Mô hình Integer Linear Program cho SALB3PM (Nguồn: Py et al.) Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 25 / 37.

Mô hình ILP cho SALB3PM (Py et al. [3] - Hình 4) Các thành phần chính: Biến quyết định: Xj,k ∈: Tác vụ j được gán cho trạm k? Sj,t ∈: Tác vụ j bắt đầu tại thời điểm t? Wmax ∈ Z+: Công suất đỉnh (biến mục tiêu). Hàm mục tiêu (1): min Wmax Ràng buộc chính (Giải thích một số): (2): Mỗi tác vụ được gán đúng 1 trạm. (3): Tổng thời gian tác vụ/trạm ≤ cycle time c. (4), (6), (9): Ràng buộc thứ tự (precedence). (5): Mỗi tác vụ bắt đầu đúng 1 lần. (7): Không chồng chéo tác vụ trên cùng một trạm. (8): Wmax là cận trên của tổng công suất tại mọi thời điểm t. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 26 / 37.

Tiếp cận dựa trên SAT (Py et al. - Section 5) I Ý tưởng chính: Thay vì giải trực tiếp bài toán tối ưu hóa ILP, tác giả đề xuất giải một chuỗi các bài toán thỏa mãn (feasibility) bằng SAT. Tại sao SAT? SAT solvers hiện đại cực kỳ mạnh mẽ trong việc xử lý các ràng buộc logic phức tạp. Có thể hiệu quả hơn ILP solvers đối với một số cấu trúc bài toán. Cho phép sử dụng các kỹ thuật mã hoá (encoding) logic chuyên biệt. Quy trình tổng quát (Xem Algorithm 1): 1 Bước 1: Mô hình hóa bài toán khả thi ban đầu bằng SAT. Biểu diễn tất cả các ràng buộc của SALBP (chưa xét Wmax) thành công thức CNF. 2 Bước 2: Gọi SAT solver. Tìm một lời giải khả thi (nếu có). 3 Bước 3: Phân tích lời giải. Tính công suất đỉnh (Pcurrent) của lời giải tìm được. Nếu Pcurrent tốt hơn Pbest hiện tại, cập nhật Pbest. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 27 / 37.

Tiếp cận dựa trên SAT (Py et al. - Section 5) II 4 Bước 4: Thêm ràng buộc tối ưu hóa. Xác định các tập tác vụ C chạy đồng thời gây ra công suất đỉnh ≥ Pbest. Thêm các mệnh đề (clause) vào công thức SAT để cấm các tập tác vụ C này chạy đồng thời trong tương lai. (Đây là ràng buộc (13) trong mô hình SAT). 5 Bước 5: Lặp lại từ Bước 2. Cho đến khi SAT solver trả về "UNSATISFIABLE"(không còn lời giải khả thi nào tốt hơn). → Lời giải ứng với Pbest cuối cùng là nghiệm tối ưu. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 28 / 37.

Mô hình SAT cho SALB3PM (Py et al. - Hình 5) Hì h Biể diễ SALB3PM bằ ô thứ ệ h đề (N ồ P t l ) Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 29 / 37.

Mô hình SAT cho SALB3PM (Py et al. - Hình 5) I Biến Boolean trong SAT: Xj,k: Tác vụ j gán cho trạm k (Giống ILP). Sj,t: Tác vụ j bắt đầu tại thời điểm t (Giống ILP). Aj,t: Tác vụ j đang hoạt động (active) tại thời điểm t. (Biến phụ quan trọng!) Mã hoá Ràng buộc (Ví dụ liên kết ILP ↔ SAT): ILP (2) ↔ SAT (1) & (2): Exactly-One Assignment. SAT (1): � k∈M Xj,k (At-Least-One - ALO) SAT (2): ¬Xj,k1 ∨ ¬Xj,k2 for k1 < k2 (At-Most-One - AMO, Pairwise encoding) ILP (5) ↔ SAT (4) & (5): Exactly-One Start Time. (Tương tự Assignment). ILP (7) ↔ SAT (7): Non-overlap (trên cùng trạm k). ¬Xi,k ∨ ¬Xj,k ∨ ¬Ai,t ∨ ¬Aj,t for i ̸= j. (Nếu i, j cùng ở trạm k, chúng không thể cùng active tại t). Liên kết Sj,t và Aj,t (SAT (8)): Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 30 / 37.

Mô hình SAT cho SALB3PM (Py et al. - Hình 5) II ¬Sj,t ∨ Aj,t+e for e ∈ [0, τj − 1]. (Nếu j bắt đầu tại t, nó phải active trong suốt thời gian τj). Ràng buộc thứ tự (ILP (6)/(9) ↔ SAT (9)): (Phức tạp hơn, diễn giải logic) Nếu i ≺ j và cùng trạm k, thì Si,t1 và Sj,t2 không thể xảy ra nếu t1 > t2. Ràng buộc Tối ưu hóa (SAT (13)): � j∈C ¬Aj,t for each set C causing peak ≥ Pbest. (Cấm tập C cùng active tại t). Đây là cách "cắt"lời giải không mong muốn. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 31 / 37.

Thảo luận: Chuyển đổi SAT sang ILP? I Từ ILP sang SAT/SMT (Như ví dụ trên): Khả thi: Có nhiều kỹ thuật encoding (Binomial, Sequential, Binary...) để biểu diễn ràng buộc số học và logic thành mệnh đề Boolean hoặc công thức SMT. Thách thức: Kích thước encoding có thể lớn (ví dụ: encoding số học bằng SAT). Cần chọn encoding phù hợp (trade-off giữa số biến/clause và khả năng lan truyền ràng buộc). Hàm mục tiêu thường được xử lý lặp (như bài báo) hoặc bằng MaxSAT/Optimization Modulo Theories. Từ SAT sang ILP (Thường ít phổ biến và khó hơn): Tại sao khó? Biểu diễn một mệnh đề logic (clause) bằng bất đẳng thức tuyến tính có thể cần biến phụ hoặc các kỹ thuật phức tạp (ví dụ: ∨ thành �). Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 32 / 37.

Thảo luận: Chuyển đổi SAT sang ILP? II Mất cấu trúc logic: ILP solvers không thực hiện lan truyền ràng buộc logic hiệu quả như SAT solvers. Khó biểu diễn các encoding SAT hiệu quả (như Sequential Counter) một cách trực tiếp và gọn gàng bằng ILP. SAT là bài toán quyết định, ILP thường là tối ưu hóa. Khi nào có thể làm? Đôi khi người ta chuyển đổi một phần bài toán logic sang ILP để kết hợp với các phần khác đã ở dạng ILP, nhưng thường không hiệu quả bằng giải trực tiếp bằng SAT/SMT nếu bài toán có cấu trúc logic mạnh. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 33 / 37.

Tổng quan về các Solvers phổ biến I Việc lựa chọn công cụ phù hợp là rất quan trọng! LP/ILP/MIP Solvers: CPLEX (IBM): Mạnh mẽ, tiêu chuẩn công nghiệp. (Thương mại, có bản quyền học thuật). Gurobi: Rất mạnh, hiệu năng cao. (Thương mại, có bản quyền học thuật). SCIP: Miễn phí cho học thuật, rất tốt, tích hợp cả kỹ thuật CP. GLPK: Mã nguồn mở, miễn phí. Sử dụng khi: Mô hình chủ yếu là ràng buộc tuyến tính, mục tiêu tối ưu rõ ràng. CP Solvers / Frameworks: Google OR-Tools (CP-SAT): Mã nguồn mở, cực kỳ hiệu quả, đặc biệt là CP-SAT solver. Giao diện đa ngôn ngữ. (Rất nên dùng!) MiniZinc: Ngôn ngữ mô hình hóa cấp cao, hỗ trợ nhiều backend solvers. Tốt để học và thử nghiệm nhanh. Choco Solver (Java), CP Optimizer (IBM)... Sử dụng khi: Bài toán có nhiều ràng buộc tổ hợp phức tạp (alldifferent, cumulative...), cấu trúc logic mạnh. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 34 / 37.

Tổng quan về các Solvers phổ biến II SAT Solvers: Glucose, MiniSat, CaDiCaL, Kissat...: Nhanh, hiệu quả cho bài toán SAT thuần túy. Thường được gọi qua thư viện như PySAT. Sử dụng khi: Bài toán có thể mã hóa hoàn toàn bằng logic mệnh đề. SMT Solvers: Z3 (Microsoft): Mạnh mẽ, đa năng, hỗ trợ nhiều lý thuyết. CVC5, Yices2... Sử dụng khi: Bài toán kết hợp logic Boolean với ràng buộc số học, mảng, bit-vector... (phổ biến trong kiểm chứng). Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 35 / 37.

Tổng kết và So sánh LP: Nền tảng, hiệu quả cho bài toán liên tục, tuyến tính. Nghiệm tối ưu ở đỉnh. ILP/MIP: Mô hình hóa quyết định rời rạc, mạnh mẽ cho nhiều bài toán thực tế. Khó giải hơn LP (NP-hard). Giải bằng Branch & Bound/Cut. SAT/SMT/CP: Cách tiếp cận khác, tập trung vào ràng buộc (logic, tổ hợp). SAT: Cực nhanh cho logic Boolean thuần túy. SMT: Mở rộng SAT với các lý thuyết nền. CP: Linh hoạt với nhiều loại ràng buộc, dùng lan truyền và tìm kiếm. Encoding là chìa khóa: Cách bạn mô hình hóa bài toán (chuyển sang ILP hay SAT/SMT/CP) ảnh hưởng lớn đến hiệu năng giải. Case Study SALB3PM: Minh họa cách một bài toán tối ưu MIP có thể được giải bằng cách lặp giải các bài toán khả thi SAT, thông qua việc mã hóa ràng buộc và thêm ràng buộc tối ưu hóa. Lựa chọn công cụ: Không có phương pháp nào "tốt nhất"cho mọi bài toán. Hiểu rõ bản chất bài toán và điểm mạnh/yếu của từng cách tiếp cận/solver là rất quan trọng. Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 36 / 37.

Q & A Câu hỏi? Thảo luận về LP, ILP, MIP, SAT/SMT, Encoding, Solvers... Kiều Văn Tuyên (Phòng Thí nghiệm Hệ thống Nhúng) Nhập môn Lập trình Tuyến tính, Nguyên, Hỗn hợp và liên hệ với SAT/SMT Ngày 2 tháng 5 năm 2025 37 / 37.