A Customized {SAT}-based Solver for Graph Coloring

We introduce {ZykovColor}, a novel {SATbased} algorithm to solve the graph coloring problem working on top of an encoding that mimics the Zykov tree. Our method is based on an approach of Hébrard and Katsirelos (2020) that employs a propagator to enforce transitivity constraints, incorporate lower bounds for search tree pruning, and enable inferred propagations. We leverage the recently introduced {IPASIR}-{UP} interface for {CaDiCaL} to implement these techniques with a {SAT} solver. Furthermore, we propose new features that take advantage of the underlying {SAT} solver. These include modifying the integrated decision strategy with vertex domination hints and using incremental bottom-up search that allows to reuse learned clauses from previous calls. Additionally, we integrate a more effective clique computation and an algorithm for computing the fractional chromatic number to improve the lower bounds used for pruning during the search. We validate the effectiveness of each new feature through an experimental analysis. {ZykovColor} outperforms other state-of-the-art graph coloring implementations on the {DIMACS} benchmark set. Further experiments on random Erdős-Rényi graphs show that our new approach matches or outperforms state-of-the-art {SAT}-based methods for both very sparse and highly dense graphs. We give an additional configuration of {ZykovColor} that dominates other {SAT}-based methods on the Erdős-Rényi graphs. This paper has been awarded the “Code and Data Available” and “Results Reproduced” badges as recognition that the author(s) have followed reproducibility principles. Code and data that allow readers to reproduce the results in this paper are available at https://doi.org/10.5281/zenodo.17328845. Participation in the {ALENEX} artifact evaluation phase was optional and performed at the request of the author(s).