Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Customized SAT-based Solver for Graph Coloring

Timo Brand, Daniel Faber, Stephan Held, Petra Mutzel

TL;DR

This work tackles the NP-hard problem of determining the chromatic number $ abla(G)$ by presenting ZykovColor, a SAT-based solver built on a Zykov-tree encoding and implemented via the IPASIR-UP interface for CaDiCaL. The method combines a transitivity propagator, strong lower-bound pruning (including cliques and Mycielskian bounds), improved clique computation, a domination-informed decision strategy, and incremental bottom-up optimization guided by the fractional chromatic number $ abla_f(G)$. An extensive ablation study demonstrates the impact of each feature, and large-scale experiments on DIMACS benchmarks and Erdős-Rényi graphs show ZykovColor outperforming state-of-the-art SAT-based and other exact coloring approaches, with notable gains in dense graphs via the fractional bound. The results highlight the practical potential of tight propagators and reusing learned clauses within SAT-based graph coloring, offering a competitive and scalable approach for real-world instances in network design and scheduling contexts.

Abstract

We introduce ZykovColor, a novel SAT-based 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.

A Customized SAT-based Solver for Graph Coloring

TL;DR

This work tackles the NP-hard problem of determining the chromatic number by presenting ZykovColor, a SAT-based solver built on a Zykov-tree encoding and implemented via the IPASIR-UP interface for CaDiCaL. The method combines a transitivity propagator, strong lower-bound pruning (including cliques and Mycielskian bounds), improved clique computation, a domination-informed decision strategy, and incremental bottom-up optimization guided by the fractional chromatic number . An extensive ablation study demonstrates the impact of each feature, and large-scale experiments on DIMACS benchmarks and Erdős-Rényi graphs show ZykovColor outperforming state-of-the-art SAT-based and other exact coloring approaches, with notable gains in dense graphs via the fractional bound. The results highlight the practical potential of tight propagators and reusing learned clauses within SAT-based graph coloring, offering a competitive and scalable approach for real-world instances in network design and scheduling contexts.

Abstract

We introduce ZykovColor, a novel SAT-based 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.

Paper Structure

This paper contains 31 sections, 2 theorems, 8 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Our Contribution
  3. Preliminaries
  4. Assignment Encoding
  5. Zykov-based Encoding
  6. IPASIR-UP Interface
  7. SAT-Based Propagator for the Zykov Encoding
  8. Transitivity Constraints
  9. Lower Bound for Pruning
  10. Inferred Propagations
  11. Improved Clique Computation
  12. Improved Decision Strategy
  13. Incremental Bottom-Up Optimization
  14. Lower Bounds Using the Fractional Chromatic Number
  15. Experimental Evaluation
  16. ...and 16 more sections

Key Result

Lemma 1

Given a subgraph $H = (V^\prime, E^\prime)$ in $G = (V,E)$ with chromatic number $k$, if there exists a vertex $v\in V \backslash V^\prime$ such that $V^\prime\backslash N(v) = \{u\}$ then $G + (u,v)$ has chromatic number at least $k+1$.

Figures (5)

  • Figure 1: Root node and first two child nodes of the Zykov tree for the graph $C_5$.
  • Figure 2: An overview of the states in the solving process and the provided user callbacks (Adapted from FazekasNPKSB24).
  • Figure 3: Survival plot of ablation study for ZykovColor variants and Full Encoding/Transitivity only.
  • Figure 4: Survival plot for different algorithms on the DIMACS graphs.
  • Figure 5: Normalized algorithm performance by parameter for ER graphs.

Theorems & Definitions (2)

  • Lemma 1: Positive pruning, hebrard2020constraint
  • Lemma 2: Negative pruning, hebrard2020constraint