ỨNG DỤNG SAT SOLVER TRONG GIẢI BÀI TOÁN BĂNG THÔNG ĐỒ THỊ CHO TỐI ƯU BỐ TRÍ MÔ-ĐUN ĐIỀU KHIỂN TUYẾN TÍNH

Tóm tắt

Bài toán băng thông đồ thị (Graph Bandwidth Problem) là một bài toán tối ưu tổ
hợp quan trọng với nhiều ứng dụng trong thiết kế hệ thống và xử lý dữ liệu có cấu trúc. Đã
có một số hướng tiếp cận được đề xuất để giải bài toán này bao gồm các thuật toán heuristic
và metaheuristic, các phương pháp tối ưu hóa chính xác dựa trên quy hoạch nguyên và tìm
kiếm ràng buộc, cũng như các hướng tiếp cận hiện đại dựa trên SAT và Constraint
Programming; tuy nhiên, các phương pháp này vẫn còn gặp hạn chế về khả năng mở rộng
hoặc hiệu quả khi áp dụng cho các bài toán có cấu trúc thực tế phức tạp. Bài báo này trình
bày một phương pháp tiếp cận dựa trên SAT Solver để giải bài toán băng thông, trong đó bài
toán được chuyển đổi thành dạng thỏa mãn Boolean dưới dạng chuẩn CNF với các ràng buộc
về gán vị trí và giới hạn băng thông. Trên cơ sở đó, bài báo nghiên cứu ứng dụng cụ thể trong
tối ưu bố trí các mô-đun điều khiển của dây chuyền sản xuất tuyến tính, nhằm giảm độ dài
cực đại của các kết nối tín hiệu trực tiếp. Kết quả thực nghiệm trên một mô hình minh họa
cho thấy phương pháp đề xuất có khả năng tìm được nghiệm tối ưu, giúp giảm đáng kể băng
thông so với các phương án bố trí ban đầu. Ngoài ra, phương pháp tiếp cận cũng cho thấy
tính tổng quát, có thể mở rộng để tích hợp thêm các ràng buộc thực tế và áp dụng cho các bài
toán bố trí tuyến tính quy mô lớn hơn.