# 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.

#### Bibliography

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