Graph Colouring with SAT
A colouring of a graph is an assignment of colours to its vertices such that every two adjacent vertices are coloured differently. Finding a colouring of a given graph using the fewest number of colours is a difficult problem in general. In this worksheet we demonstrate how to solve the graph colouring problem by translating it into Boolean logic and using Maple's built-in efficient SAT solver. This approach is now available as an option to Maple’s ChromaticNumber function, which also solves the graph colouring problem. Using SAT can dramatically improve the performance of this function in some cases, including the “queen graphs” problem shown in this application.
