Sat solving techniques improve graph labeling with minimum label span
Solving Minimum Span Antibandwidth and Cyclic Antibandwidth Labeling Problems
Artificial Intelligence
Summary
Assigning numbers to connected points in a network can be tricky, especially when trying to keep certain minimum gaps between connected points. The authors focus on a related problem where the gap is set first, and the goal is to use the smallest possible range of numbers. They developed a method using SAT solvers (tools that decide if a set of logical statements can be true) to find exact solutions more efficiently. Their approach works well compared to existing optimization software, especially when they apply certain constraints. This shows that SAT solving is a strong tool for these challenging graph labeling problems.
What this means in practice
- •For network schedulers: Schedule tasks with constraints on spacing by minimizing label ranges to improve resource usage based on exact SAT solving methods.
- •For circuit layout engineers: Design chip layouts minimizing label spans under spacing constraints for components connected closely using SAT-based approaches.
Authors
Hieu Truong Xuan, Khanh To Van
Abstract
The Antibandwidth and Cyclic Antibandwidth problems are NP-hard graph labeling problems that aim to maximize the minimum (cyclic) distance between labels assigned to adjacent vertices. Extensive research on these problems has resulted in a variety of mathematical formulations and computational approaches. However, their minimum span perspective, in which a prescribed minimum (cyclic) distance is fixed and the objective is to minimize the label span, has received comparatively little attention. In this paper, we consider this complementary perspective by introducing the Minimum Span Antibandwidth/Cyclic Antibandwidth Labeling (MSABL/MSCABL) problems and developing a unified Boolean Satisfiability (SAT)-based framework for solving them. The SAT-based framework formulates MSABL/MSCABL as a sequence of decision problems and exploits their monotonicity to accelerate the search process. We also consider two SAT solving strategies, parallel and incremental SAT solving: the former examines multiple candidate spans concurrently, while the latter reuses a single SAT instance while progressively restricting the label domain. The proposed approaches are evaluated on benchmark instances from the Harwell-Boeing Sparse Matrix Collection and compared with CPLEXCP, CPLEXMIP, and Gurobi. The results show that SAT-based approaches are highly competitive in solution quality, with the parallel approach performing best overall for MSCABL and the incremental approach for MSABL. With the no-hole constraint, they remain competitive with CPLEXCP and significantly outperform CPLEXMIP and Gurobi, particularly for MSCABL. These results demonstrate the effectiveness of SAT solving as an exact approach for MSABL and MSCABL.