SAT Algorithms for Colouring Some Special Classes of Graphs: Some Theoretical and Experimental Results

The local search algorithm GSAT is based on the notion of Satisfiability. It has been used successfully for colouring graphs, solving instances of the 3SAT problem, planning blocks world exercises, and other applications. The runtime performance of GSAT can be considerably enhanced by the incorporation of a noise generating component such as tabu search or random walk. This has been verified experimentally on numerous occasions, but few attempts have been made to explain the observed phenomena analytically. This paper examines, in the context of graph colouring, some aspects of the role of the tabu list in GSAT. Two slightly different SAT formulations of graph colouring are considered. Three classes of graphs are defined that have the interesting property that, for certain initial partial colourings of the nodes, a proper colouring cannot be achieved by GSAT without the use of a tabu list. The minimum length of the tabu list that is necessary for solving the problem is determined for each class. It is found that this length varies considerably from case to case, and is sometimes quite large. We study experimentally the variation of runtime with the length of the tabu list to verify and further explore the theoretical results. We examine the general performance of other local search SAT methods like WalkSAT, Novelty, RNovelty, Novelty+ and RNovelty+ on these classes of graphs and to make a comparative assessment of all these methods.