Date: Thu, 23 Oct 2003 12:48:16 -0400 (EDT)
From: Matthew A Hibbs
Subject: HW3 Generator Clarification

There seems to be some confusion about how to go about writing the
generator for the programming portion of HW3. To clarify this a bit, I'm
going to step through the reduction of the graph coloring problem down to
CNF, as discussed in class.

To remind you, the graph coloring problem is this: Given a graph, assign
each of the vertices a color such that no two adjacent vertices share the
same color. In order to convert this to CNF, we need to create a set of
rules that capture what it takes to have a valid graph coloring. We also
want to include some sense of random-ness so that our generator won't
produce the same CNF each time. It is also desireable (but not required)
to always produce satisfiable CNFs.

One way that we can meet all of these criteria is to first randomly
generate a validly colored graph, and create the set of rules/clauses
based on this randomly generated graph. So, let's break the problem down
into several smaller steps.

First, we need to decide how many nodes will be in the graph, and how many
colors we'll use. You could generate these numbers randomly, or you could
fix them at some pre-chosen value. In either case, let's say you have n
nodes in your graph and k colors. Next, we can randomly color each node
of our graph one of the available colors, you might do this with an array.

Now, we can connect up nodes that are different colors to create the
graph. You could do this with an adjacency matrix or an adjacency list.
If you connect each node to all other nodes that don't share its color,
your CNF will be relatively 'hard' becuase there will be a small number of
models that will satisfy all of your clauses (this isn't neccessarily
bad). If you want to make your CNF 'easier' one way to do this is to
enforce a limit on the degree of any node in the graph.

Now that we have our graph, we can ignore the colors of all the nodes, but
we know that a valid coloring exists for the graph, so our CNF should be
satisfyable. Next, let's think about what rules we need to have to encode
this problem. First, we need to guarantee that every node has exactly one
color. Then, we need to guarantee that no two adjacent nodes share the
same color.

The literals for our CNF will be of the form N{i,j} which means that node
i has the color j. So in general we will have n*k literals, one for every
node being every color. Now, to guarantee that every node is exactly one
color, we need to grantee that every node is at least one color, and that
every node is no more than one color. To guarantee 'at least one color'
we can have a rule like this for every node i:
(N{i,1} v N{i,2} v ... v N{i,k})

Then to guarantee 'no more than one color', we want rules like this for
every node i, and every color:
N{i,1} -> (-N{i,2} ^ -N{i,3} ^ ... ^ -N{i,k})
N{i,2} -> (-N{i,1} ^ -N{i,3} ^ ... ^ -N{i,k})
...
N{i,k} -> (-N{i,1} ^ -N{i,2} ^ ... ^ -N{i,k-1})
Now, to simplify these rules to CNF let's use the rule (A->B)=(-A v B):
-N{i,1} v (-N{i,2} ^ -N{i,3} ^ ... ^ -N{i,k})
-N{i,2} v (-N{i,1} ^ -N{i,3} ^ ... ^ -N{i,k})
...
-N{i,k} v (-N{i,1} ^ -N{i,2} ^ ... ^ -N{i,k-1})
Now, we can use the law of distribution (see fig 7.11 in R&N) to reduce
this to CNF:
(-N{i,1} v -N{i,2}) ^ (-N{i,1} v -N{i,3}) ^ ... ^ (-N{i,1} v -N{i,k})
(-N{i,2} v -N{i,1}) ^ (-N{i,2} v -N{i,3}) ^ ... ^ (-N{i,2} v -N{i,k})
...
(-N{i,k} v -N{i,1}) ^ (-N{i,k} v -N{i,2}) ^ ... ^ (-N{i,k} v -N{i,k-1})

The generator code doesn't need to go through this whole conversion
process, you can just generate this last set of CNF clauses directly. So
just how many clauses does this take? We need n clauses for the 'at least
one color' rules, and then we need n*k*(k-1) clauses for the 'no more than
one color' rules. Note that we've duplicated some rules. This is okay,
but we could avoid this without too much trouble.

Now let's look at the adjacency rules. For every edge of our graph, we
need to make rules that prohibit the adjacent nodes from sharing a color.
So for all adjacent nodes i and j, we need rules like this:
-(N{i,1} ^ N{j,1})
-(N{i,2} ^ N{j,2})
...
-(N{i,k} ^ N{j,k})
Now, to convert these rules to CNF, we can just apply DeMorgans law:
(-N{i,1} v -N{j,1})
(-N{i,2} v -N{j,2})
...
(-N{i,k} v -N{j,k})
Now, how many of these rules will we have? Let z = number of edges in our
graph. It will take z*k clauses for the adjacency rules.

So, all together, it takes n + n*k*(k-1) + z*k clauses to encode the graph
coloring problem in CNF. Again, we can just generate the final CNFs, the
code doesn't need to go through the entire conversion process. All of
that said, your writeup for this part does need to go through this process
of deriving down to CNFs.

One more note about the 'creativity' portion. As stated on the
assignment, you are not allowed to use graph coloring. However, it is
okay to do a 'creative' variant of graph coloring (many, many problems are
reducible to graph coloring). Try to have some fun with the problem you
choose and it will most likely be 'creative'.

Cheers,
Matt