Performance Analysis of DSATUR and SAT-Solving: A Comparative Study on Graph-Coloring

Sammanfattning

The Graph Coloring Problem (GCP) is a foundational challenge in graph theory, demanding the assignment of colors to graph vertices so that no two adjacent vertices share the same color, with the objective of minimizing the number of colors used. This problem is not only theoretical but also has a lot of practical applications. Given its NP-hard classification, finding the minimum number of colors required for any graph is a complex task, with no known polynomialtime solution that applies universally. Various strategies have been developed to tackle this issue, including heuristic algorithms and Boolean satisfiability problem (SAT) solving approaches. Heuristic algorithms offer quick, adaptable solutions without guaranteed optimality, while SAT solving transforms the problem into a SAT, leveraging recent advances in this area to find effective solutions. Due to the importance of these methods and the relevance of the GCP, it promotes a systematic comparison between heuristic algorithms and SAT solving techniques regarding their efficiency and solution quality within this specific context. Our study aims to explore this by conducting empirical experiments to compare these two popular optimization strategies across different graph coloring problem instances, focusing on aspects such as problem size, graph density, solution quality, and computational time. This research is conducted under specific constraints, excluding parallel computing and distributed SAT solving methods and imposing a maximum computational limit to ensure the manageability of the study. Through this comparative analysis, we seek to provide valuable insights into the relative performance of heuristic algorithms and SAT solving methods in addressing the GCP, thereby contributing to a better understanding of their applicability and effectiveness in various scenarios. Our results show that the heuristic algorithm DSATUR offers quicker solutions than SAT solving for almost all problem instances, but that SAT solving reaches a solution with fewer colors used for all different graph types. These findings can help give insight into picking the right algorithm for the right purpose