chromatic_number.jl

using Graphs
using PicoSAT

function optimal_coloring(g::SimpleGraph{T})::Graphs.Coloring{T} where {T <: Integer}
    # FIXME which is faster: maximum clique or maximal clique?
    max_clique = argmax(length, maximal_cliques(g))
    #max_clique = independent_set(complement(g), DegreeIndependentSet())
    #@show max_clique
    for χ in length(max_clique):nv(g)
        #println("Trying χ=$χ")
        indexer = reshape(1:(nv(g)*χ), (nv(g), χ))
        cnf = Vector{Int64}[]

        # Seeding the solution on a maximal clique makes it solve faster.
        for (i, v) in enumerate(max_clique)
            push!(cnf, [indexer[v,i]])
        end

        for i in 1:nv(g)
            push!(cnf, indexer[i,:])
        end
        for e in Graphs.edges(g)
            for j in 1:χ
                push!(cnf, [ -indexer[Graphs.src(e), j], -indexer[Graphs.dst(e), j] ])
            end
        end
        sol = PicoSAT.solve(cnf)
        if sol != :unsatisfiable
            colormatrix = zeros(Bool, (nv(g), χ))
            colormatrix[filter(i->i>0, sol)] .= true
            colors = map(argmax, eachrow(colormatrix))
            @assert all(colors .>= 1)
            @assert all(colors .<= χ)
            for e in Graphs.edges(g)
                @assert colors[Graphs.src(e)] != colors[Graphs.dst(e)]
            end
            return Graphs.Coloring{T}(χ, colors)
        end
    end
    @assert false
end