
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 3color 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 nodesa, 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 colorwhatever 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.