Munmun Dey¹ and Amitava Bagchi², ¹Sanaka Educational Trust's Group of Institutions, India and ²Heritage Institute of Technology, India

The graph colouring problem can be solved using methods based on Satisfiability (SAT). An instance of the problem is defined by a Boolean expression written using Boolean variables and the logical connectives AND, OR and NOT. It has to be determined whether there is an assignment of TRUE and FALSE values to the variables that makes the entire expression true.A SAT problem is syntactically and semantically quite simple. Many Constraint Satisfaction Problems (CSPs)in AI and OR can be formulated in SAT. These make use of two kinds of searchalgorithms: Deterministic and Randomized.It has been found that deterministic methods when run on hard CSP instances are frequently very slow in execution.A deterministic method always outputs a solution in the end, but it can take an enormous amount of time to do so.This has led to the development of randomized search algorithms like GSAT, which are typically based on local (i.e., neighbourhood) search. Such methodshave been applied very successfully to find good solutions to hard decision problems.

SAT, GSAT, Graph Colouring, Randomized Search Algorithms, CSPs