Bài toán độ rộng băng thông của đồ thị có trọng số (WGBP) mở rộng bài toán cổ điển bằng cách đưa vào trọng số cạnh nhằm mô hình hóa các tương tác không đồng nhất trong các ứng dụng như sắp xếp lại ma trận thưa và bố trí mạch VLSI. Bài báo đề xuất một khung phương pháp dựa trên SAT, trong đó các ràng buộc sắp xếp đỉnh và độ giãn có trọng số được mã hóa dưới dạng chuẩn CNF bằng các kỹ thuật pseudo-Boolean và cardinality, cho phép khai thác hiệu quả các SAT solver hiện đại dựa trên cơ chế học mệnh đề (CDCL). Bài toán tối ưu được giải thông qua quy trình SAT lặp kết hợp tìm kiếm nhị phân trên cận độ rộng băng thông. Được cài đặt bằng PySAT và đánh giá với MiniSat và Glucose, phương pháp đề xuất cho thấy khả năng xác định hiệu quả giá trị tối ưu và cải thiện đáng kể tính cục bộ cấu trúc của các ma trận thưa có trọng số, qua đó khẳng định tiềm năng của các kỹ thuật SAT trong tối ưu hóa bố trí đồ thị có trọng số.
The Weighted Graph Bandwidth Problem (WGBP) extends the classical bandwidth minimization problem by incorporating edge weights to model heterogeneous interactions in applications such as sparse-matrix reordering and Very Large-Scale Integration (VLSI) placement. This paper proposes a SAT-based framework that encodes vertex-ordering and weighted-stretch constraints into Conjunctive Normal Form (CNF) using pseudo-Boolean and cardinality encodings, enabling the use of modern ConflictDriven Clause Learning (CDCL) solvers. The optimization task is solved via an iterative SAT-based procedure with a binary search strategy over bandwidth bounds. Implemented using PySAT and evaluated with MiniSat and Glucose, the proposed approach effectively determines optimal bandwidth values and improves structural locality in weighted sparsematrix instances, demonstrating the practical potential of SAT techniques for weighted graph layout optimization.