Since 3 coloring is an NP and SAT is NP complete, meaning that it's NP hard,
it has to be the case that we could use SAT to solve 3 coloring problems,
but it's actually a little bit interesting to see how you might do that.
So let's take a look, here's a simple little graph and one, two, three, four nodes, four edges
and imagine that we want to try to 3-color this graph.
What we're going to do is we're going to create a ??? formula that is satisfiable
if and only if this graph is 3 colorable, so that it's really the same problem,
and the way that we're going to do that is we're going to create a bunch of boolean variables,
12 of them to be exact, corresponding to each of the four nodes--a, b, c, and d,
and for each node, we'll a boolean variable saying whether that node is
red or green or yellow, the three colors.
For example, assigning the variable a red to true, a green to false and a yellow to false
means that we're coloring the a node red, and so once we've assigned true values,
trues and falses to all 12 of these variables that corresponds perhaps to some coloring.
In fact, you have to be a little bit careful here because if we assigned two of these to true,
which is a perfectly reasonable thing to do in a boolean formula, you can't really interpret this
as a coloring except for may be a is orange, but that's not really allowed.
What we have to do now is given these 12 variables, we have to create a formula that is true
if and only if it corresponds to a valid coloring, meaning that both exactly one of each of these
triples the variables are true and there's no collisions--
for example, we can't have a colored red and b colored red because they're connected by an edge.
They will have to be different if they're connected by an edge.
The formula for this can be generated automatically and I'll give you glimpse at it.
Here it is, at least one version of it, and it's a little bit weird and complicated,
but it actually falls into some nice structures.
First there's a bunch of logic to say that it should be the case that say--
the a red, a green, and a yellow variables, one of them should be true.
If they're all false, then it's not telling us what color a should be, and it also has to be case
that no pair of colors can be true for a given node.
It can't be the case that both a red is true and a green is true, so that's bad.
There has to be at least one true and not the case that both a is both red and green
not the case that a is both red and yellow and not the case that both a is green and yellow,
and we do that for all four of the nodes and that tells us that
there's a meaningful color assignment to the nodes.
Then we have some additional clauses that say--
what can't be the case that a is red and b is red at the same time.
It can't be the case that a is green and b is green at the same time and it can't be the case
that a is yellow and b is yellow at the same time.
What is that saying, that saying the color--whatever the color happens to be--
for a it can't match the color of b and that's because they share an edge in the graph.
For each of the edges in the graph, we have three of these statements to rule out
all possible color matches, so there's three of these for one edge, two edge, three edge--
there's four edges in the graph so we have four blocks of these.
In this formula now as a whole has a satisfying assignment, has an assignment that makes
this whole expression true if and only if there's a coloring, a 3 coloring of that graph.
Now, in this case, I generated this formula by carefully looking at the graph
and going back and forth in making the formula, but you can automate this idea
by just generalizing the way that I did this here.
Why don't you think about how to do that and I'll ask you a question
just to make sure that you got the idea.