Ứ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
Lĩnh vực: Công nghệ thông tin
Khoa: Khoa Công Nghệ Thông Tin
Lượt xem: 83
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.
The Graph Bandwidth Problem is a fundamental combinatorial optimization problem with numerous applications in system design and structured data processing. Several approaches have been proposed to address this problem, including heuristic and metaheuristic algorithms, exact optimization methods based on integer programming and constraint search, as well as more recent approaches based on SAT and Constraint Programming. However, these methods still face limitations in terms of scalability and efficiency when applied to problems with complex real-world structures. This paper presents a SAT solver-based approach for solving the graph bandwidth problem, in which the problem is encoded as a Boolean satisfiability problem in conjunctive normal form (CNF) with constraints on position assignment and bandwidth limits. Based on this formulation, the paper investigates a practical application in optimizing the linear arrangement of control modules in a production line, with the objective of minimizing the maximum length of direct signal connections. Experimental results on a representative instance demonstrate that the proposed approach is capable of finding optimal solutions and significantly reducing the bandwidth compared to initial layouts. Furthermore, the proposed method exhibits a high degree of generality and can be extended to incorporate additional practical constraints, making it applicable to larger-scale linear arrangement problems.