SAT-encoded "Morphed" 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. Generally, there are two variants of the Graph Colouring 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.

An interesting class of Graph Colouring Problems is obtained by morphing regular ring lattices with random graphs [GHPW99]: A (type B) p-morph of two graphs A=(V,E1) and B=(V,E2) is a graph C=(V,E) where E contains all the edges common to A and B, a fraction p of the edges from E1-E2 (the remaining edges of A), and a fraction 1-p of the edges from E2-E1. The test-sets considered here are obtained by morphing regular ring lattices, where the vertices are ordered cyclically and each vertex is connected to its k closest in this ordering, and random graphs from the well-known class Gnm. The morphing ratio p controls the amount of structure in the problem instances, and by varying p, the behaviour of various algorithms depending on the degree of structure and randomness can be studied [GHPW99].

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 a generator program provided by Toby Walsh. All graphs have 100 vertices and 400 edges, the regular ring lattice used for morphing connects each vertex to its 8 nearest neighbours in the cyclic ordering. For 0 < p < 1, the chromatic number of the graphs thus obtained varies. Using a special graph colouring program provided by Joe Culberson, we filtered out all instances with c!=5 colours (the regular ring lattice, i.e., the morphed graph for p=0, has chromatic number 5). All instances are satisfiable. [GHPW99] show that that for small p (around 0.01), these instances are hardest for local search algorithms, such as WalkSAT, while for higher p (around 0.2), some of the instances are extremely hard for systematic search algorithms, such as Satz.

test-set instances vertices edges morphing ratio colours vars clauses
sw100-8-lp0-c5 100 100 400 1 5 500 310
sw100-8-lp1-c5 100 100 400 0.5 5 500 3100
sw100-8-lp2-c5 100 100 400 0.25 5 500 3100
sw100-8-lp3-c5 100 100 400 0.125 5 500 3100
sw100-8-lp4-c5 100 100 400 2^-4 5 500 3100
sw100-8-lp5-c5 100 100 400 2^-5 5 500 3100
sw100-8-lp6-c5 100 100 400 2^-6 5 500 3100
sw100-8-lp7-c5 100 100 400 2^-7 5 500 3100
sw100-8-lp8-c5 100 100 400 2^-8 5 500 3100
sw100-8-p0-c5 1 100 400 0 5 500 3100

Table 1: SAT-encoded "Morphed" Graph Colouring test-sets. All instances are satisfiable.


[GHPW99] Ian Gent, Holger H. Hoos, Patrick Prosser, and Toby Walsh Morphing: Combining Structure and Randomness. Proc. of AAAI-99, pages 654-660, 1999