satcol Determine whether a given graph is k-colorable for some k. How does it work? Given a graph in the well-known DIMACS format, the program outputs a CNF file. This is then fed to an external SAT solver.