Fast Exact Solvers for Chromatic Number

Finding the chromatic number of a graph is an NP-Hard problem, so there isn't a fast solver 'in theory'. Is there any publicly available software that can compute the exact chromatic number of a graph quickly?

I'm writing a Python script that computes the chromatic number of many graphs, but it is taking too long for even small graphs. The graphs I am working with a wide range of graphs that can be sparse or dense but usually less than 10,000 nodes. I formulated the problem as an integer program and passed it to Gurobi to solve. Do you have recommendations for software, different IP formulations, or different Gurobi settings to speed this up?

import networkx as nx
from gurobipy import *

# create test graph
n = 50
p = 0.5
G = nx.erdos_renyi_graph(n, p)

# compute chromatic number -- ILP solve
m = Model('chrom_num')

# get maximum number of variables necessary
k = max(nx.degree(G).values()) + 1

# create k binary variables, y_0 ... y_{k-1} to indicate whether color k is used
y = []
for j in range(k):
    y.append(m.addVar(vtype=GRB.BINARY, name='y_%d' % j, obj=1))

# create n * k binary variables, x_{l,j} that is 1 if node l is colored with j
x = []
for l in range(n):
    x.append([])
    for j in range(k):
        x[-1].append(m.addVar(vtype=GRB.BINARY, name='x_%d_%d' % (l, j), obj=0))

# objective function is minimize colors used --> sum of y_0 ... y_{k-1}
m.setObjective(GRB.MINIMIZE)
m.update()

# add constraint -- each node gets exactly one color (sum of colors used is 1)
for u in range(n):
    m.addConstr(quicksum(x[u]) == 1, name='NC_%d' % u)

# add constraint -- keep track of colors used (y_j is set high if any time j is used)
for u in range(n):
    for j in range(k):
        m.addConstr(x[u][j] <= y[j], name='SH_%d_%d' % (u,j))

# add constraint -- adjacent nodes have different colors
for u in range(n):
    for v in G[u]:
        if v > u:
            for j in range(k):
                m.addConstr(x[u][j] + x[v][j] <= 1, name='ADJ_%d_%d_COL_%d' % (u,v,j))

# update model, solve, return the chromatic number
m.update()
m.optimize()
chrom_num = m.objVal

I am looking to compute exact chromatic numbers although I would be interested in algorithms that compute approximate chromatic numbers if they have reasonable theoretical guarantees such as constant factor approximation, etc.

You might want to try to use a SAT solver or a Max-SAT solver. I expect that they will work better than a reduction to an integer program, since I think colorability is closer to satsfiability.

SAT solvers receive a propositional Boolean formula in Conjunctive Normal Form and output whether the formula is satisfiable. The following problem COL_k is in NP:

Input: Graph G and natural number k.

Output: G is k-colorable.

To solve COL_k you encode it as a propositional Boolean formula with one propositional variable for each pair (u,c) consisting of a vertex u and a color 1<=c<=k. You need to write clauses which ensure that every vertex is is colored by at least one color. You also need clauses to ensure that each edge is proper. Then you just do a binary search to find the value of k such that G is k-colorable but not (k-1)-colorable. There are various free SAT solvers. I have used Lingeling successfully, but you can find many others on the SAT competition website. They all use the same input and output format. Google "MiniSAT User Guide: How to use the MiniSAT SAT Solver" for an explanation on this format.

You can also use a Max-SAT solver, again consult the Max-SAT competition website. They can solve the Partial Max-SAT problem, in which clauses are partitioned into hard clauses and soft clauses. Here, the solver finds the maximal number of soft clauses which can be satisfied while also satisfying all of the hard clauses, see the input format in the Max-SAT competition website (under rules->details).

You can formulate the chromatic number problem as one Max-SAT problem (as opposed to several SAT problems as above). In this sense, Max-SAT is a better fit. On the other hand, I have the impression that SAT solvers generally perform better than Max-SAT solvers. I don't have any experience with this kind of solver, so cannot say anything more.