E192-01 - Forschungsbereich Algorithms and Complexity
-
Journal:
ACM Journal on Experimental Algorithmics
-
Date (published):
Dec-2023
-
Number of Pages:
19
-
Publisher:
Association for Computing Machinery (ACM)
-
Peer reviewed:
Yes
-
Keywords:
Graph coloring; SAT Encoding; Tabu Search; SAT-based local improvement; massive graphs
en
Abstract:
Graph coloring is the problem of coloring the vertices of a graph with as few colors as possible, avoiding monochromatic edges. It is one of the most fundamental NP-hard computational problems. For decades researchers have developed exact and heuristic methods for graph coloring. While methods based on propositional satisfiability (SAT) feature prominently among these exact methods, the encoding size is prohibitive for large graphs. For such graphs, heuristic methods have been proposed, with tabu search among the most successful ones.
In this article, we enhance tabu search for graph coloring within the SAT-based local improvement (SLIM) framework. Our hybrid algorithm incrementally improves a candidate solution by repeatedly selecting small subgraphs and coloring them optimally with a SAT solver. This approach scales to dense graphs with several hundred thousand vertices and over 1.5 billion edges. Our experimental evaluation shows that our hybrid algorithm beats state-of-the-art methods on large dense graphs.
en
Project title:
SAT-Basierende lokale Verbesserungsmethoden: P32441-N35 (FWF - Österr. Wissenschaftsfonds) Strukturerkennung mit SAT: P36420-N (FWF - Österr. Wissenschaftsfonds) Revealing and Utilizing the Hidden Structure for Solving Hard Problems in AI: ICT19-065 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Doktoratskolleg: W 1255-N23 (FWF - Österr. Wissenschaftsfonds)