Large SAT-encoded 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.

Large DIMACS GCP instances

The large graph colouring instances included in the DIMACS benchmark test-set  (see Table 1) stem originally from a study of algorithms for the optimisation variant of the graph colouring problem which has focused on Simulated Annealing [JAMS89]. The instances stem from randomly generated graphs in which an edges between two given vertices is included with a fixed probability p. All the instances are satisfiable.
Interestingly, the instances g125.18.cnf and g125.17.cnf are based on the same graph, in the first instance 18-colouring are allowed and in the latter only 17 colours are allowed. In fact, when trying to solve these two instances with Walksat, instance g125.18.cnf is easily solved with reasonable parameter settigns, while instance g125.17.cnf is much harder.

instance  colours  vars  clauses  satisfiable? 
g125.18.cnf  18  2250  70163  yes 
g125.17.cnf  17  2125  66272  yes 
g250.15.cnf 15  3750  233965  yes 
g250.29.cnf 29  7250  454622  yes 

Table 1: Large SAT-encoded Graph Colouring instances
 
 

Bibliography

[JAMS89] D.S. Johnson, C.R. Aragon, L.A. McGeoch, and C. Schevon. Optimization by Simulated Annealing: An Experimental Evaluation: Part II, Graph Coloring and Number Partitioning. Operations Research,, Vol. 37(6), pages 865-892, 1989.