SATencoded "Morphed" Graph Colouring Problems
The Graph Colouring problem (GCP) is a wellknown 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 SATencoded 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) pmorph 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 E1E2 (the remaining
edges of A), and a fraction 1p of the edges from E2E1.
The testsets 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 wellknown 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 testsets
The testsets 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.
testset  instances
 vertices  edges
 morphing ratio
 colours
 vars  clauses

sw1008lp0c5  100  100  400  1  5  500  310

sw1008lp1c5  100  100  400  0.5  5  500  3100

sw1008lp2c5  100  100  400  0.25  5  500  3100

sw1008lp3c5  100  100  400  0.125  5  500  3100

sw1008lp4c5  100  100  400  2^4  5  500  3100

sw1008lp5c5  100  100  400  2^5  5  500  3100

sw1008lp6c5  100  100  400  2^6  5  500  3100

sw1008lp7c5  100  100  400  2^7  5  500  3100

sw1008lp8c5  100  100  400  2^8  5  500  3100

sw1008p0c5  1  100  400  0  5  500  3100

Table 1: SATencoded "Morphed" Graph Colouring testsets.
All instances are satisfiable.
Bibliography
[GHPW99]
 Ian Gent, Holger H. Hoos, Patrick Prosser, and Toby Walsh
Morphing: Combining Structure and Randomness.
Proc. of AAAI99, pages 654660, 1999
