SAT-encoded "Flat" Graph Colouring Problems

The Graph Colouring problem (GCP) is a well-known combinatorial problem from graph theory: Given a graph G=(V,E), where V={v_1,v_2,...,v_n} is the set of vertices and E the set of edges connecting the vertices, find a colouring C: V -> N, such that connected vertices always have different colours. There are two variants of this problem: In the optimisation variant, the goal is to find a colouring with a minimal number of colours, whereas in the decision variant, the question is to decide whether for a particular number of colours, a couloring of the given graph exists. The two variants are tightly related, as optimal colourings can be found by solving a series of decision problems, using, for instance, binary search to determine the minimal number of colours. In the context of SAT-encoded Graph Colouring problems, we focus on the decision variant.

SAT encoding

Following earlier approaches in literature, we use a straightforward strategy for encoding GCP instances into SAT: Each assignment of a colour to a single vertex is represented by a propositional variable; each colouring constraint (edge of the graph) is represented by a set of clauses ensuring that the corresponding vertices have different colours, and two additional sets of clauses ensure that valid SAT assignments assign exactly one colour to each vertex.

GCP test-sets

The test-sets provided here (see Table 1) are generated using J.Culberson's flat graph generator (see also Joe Culbersons's Graph Coloring Page for more information). They consist of 3-colourable flat graphs the connectivity of which is adjusted in such a way that the instances are very hard to solve (in average) for graph colouring algorithms like the Brelaz heuristic [Hog96]. All instances are satisfiable.

test-set instances vertices edges colours vars clauses
flat30-60 100 30 60 3 90 300
flat50-115 1000 50 115 3 150 545
flat75-180 100 75 180 3 225 840
flat100-239 100 100 239 3 300 1117
flat125-301 100 125 301 3 375 1403
flat150-360 100 150 360 3 450 1680
flat175-417 100 175 417 3 525 1951
flat200-479 100 200 479 3 600 2237

Table 1: SAT-encoded Graph Colouring test-sets (flat random graphs). All instances are satisfiable.


Bibliography

[Hogg96] Tad Hogg Refining the Phase Transition in Combinatorial Search. Artificial Inteligence, Vol. 81, pages 127-154, 1996
[Hog96] Tad Hogg Refining the Phase Transition in Combinatorial Search. Artificial Inteligence, Vol. 81, pages 127-154, 1996