3 Coloring a given graph to a boolean expression in a Mini-Sat format

Question

I'm working on a project where I have to read a file representing a graph. I made the input file looks like this:

  b c
  a c d 
  a b 
  b

So each line signifies a node. For eg, the first line is node a which is connected to b and c and the second is node b connected to a, c, and d. So I'm not really sure where to start here. I know that we need a bunch of if and else statements such that two nodes sharing an edge cannot have the same color and each node should have at least one color. But then how can I create the node variables itself as the text file can contain any amount of nodes. I know what I have to do for the bunch of if and else statements but I do not get how can I use that to reduce it to a miniSAT format like:

p cnf 3 3 
1 -2 0 
2 -3 0 
-1 3 0

where the first "3" represents the number of variables and the second 3 represents the number of clauses. The other lines consist of different variables such that each different number is its own variable and if it's positive then it is true else false

Answer 1

You're essentially asking for how to reduce 3-coloring to CNF-SAT. Let's start with how to do that, then talk about how to generate the file you need.

The basic idea behind the reduction is the following: for each node x, we'll create three propositional variables: x_r, x_g, and x_b that indicate what color is assigned to the node (red, green, or blue). From there, we need to add in clauses to enforce the following constraints:

1. every node is given at least one color,
2. every node is given at most one color, and
3. no two adjacent nodes are given the same color.

To encode point (1), we can use this clause:

(x_r ∨ x_g ∨ x_b)

To encode point (2), we can use three clauses, each of which rules out the possibility that two colors are assigned:

(¬x_r ∨ ¬x_g) ∧

(¬x_g ∨ ¬x_b) ∧

(¬x_b ∨ ¬x_r)

Finally, there's rule (3). We can basically adapt the above strategy to solve this problem. For each pair of adjacent nodes x and y, add in these clauses:

(¬x_r ∨ ¬y_r) ∧

(¬x_g ∨ ¬y_g) ∧

(¬x_b ∨ ¬y_b)

The overall formula is then made by AND-ing all of these clauses together.

Now, the question is how to generate the output file that you want to generate. There are plenty of ways you could do this. Here's a few options:

1. You could calculate exactly how many clauses and variables are needed directly from the number of nodes and edges in the graph, then use some clever arithmetic tricks to output each clause by doing some math to figure out which variables correspond to which indices.

2. You could build some internal representation of variables and clauses (for example, have a map from nodes to the number associated with its color variables, then have a list of clauses), build that representation, then iterate over it to generate the output file.

I'd personally recommend option (2), as I imagine that's probably the easiest way of doing this.

Hope this helps!