Boolean formula for a graph vertex-colouring algorithm

Question

I have a graph which has 5 vertexes.

Graph g1 = new Graph(5);
        g1.addEdge(0, 1);
        g1.addEdge(0, 2);
        g1.addEdge(1, 2);
        g1.addEdge(1, 3);
        g1.addEdge(3, 2);
        g1.addEdge(3, 4);
        g1.addEdge(4, 2);
        System.out.println("Coloring of graph 1");
        g1.greedyColoring();

I need to express the problem of coloring this graph as a boolean expression.

Suppose a, b, and c are three colours, and the literal ai means vertex i has color a. Then the above graph could be colored like this:

a0, b1, c2, a3, b4

How can I get a boolean formula that, when satisfied, provides a solution for coloring this graph?

trincot · Accepted Answer · 2024-09-09 18:12:56Z

You are looking for coloring all vertices in a graph, each with one out of three available colors, such that no two adjacent nodes have the same color.

There are thus three types of conditions:

1. Two adjacent nodes cannot have the same color

So for instance, the edge (0, 1) will imply these three constraints:

Node 0 and 1 cannot both have color a
Node 0 and 1 cannot both have color b
Node 0 and 1 cannot both have color c

Translated into a boolean expression:

¬a0 ∨ ¬a1
¬b0 ∨ ¬b1
¬c0 ∨ ¬c1

You would need to generate such triplets of disjunctions for all edges. So in total you'll have 3 x 7 = 21 boolean disjunctions:

¬a0 ∨ ¬a1    ¬a0 ∨ ¬a2    ¬a1 ∨ ¬a2    ¬a1 ∨ ¬a3    ¬a3 ∨ ¬a2    ¬a3 ∨ ¬a4    ¬a4 ∨ ¬a2
¬b0 ∨ ¬b1    ¬b0 ∨ ¬b2    ¬b1 ∨ ¬b2    ¬b1 ∨ ¬b3    ¬b3 ∨ ¬b2    ¬b3 ∨ ¬b4    ¬b4 ∨ ¬b2
¬c0 ∨ ¬c1    ¬c0 ∨ ¬c2    ¬c1 ∨ ¬c2    ¬c1 ∨ ¬c3    ¬c3 ∨ ¬c2    ¬c3 ∨ ¬c4    ¬c4 ∨ ¬c2

###2. All nodes must get a color

So for instance, for node 0 we will have this constraint:

Node 0 must have color a, b, or c

Translated into a boolean expression:

a0 ∨ b0 ∨ c0

You would need to do the same for all nodes, so in total you'll have 5 such expressions:

a0 ∨ b0 ∨ c0
a1 ∨ b1 ∨ c1
a2 ∨ b2 ∨ c2
a3 ∨ b3 ∨ c3
a4 ∨ b4 ∨ c4

3. No nodes can get more than one color

So for instance, for node 0 we will have:

Node 0 cannot have both color a and b
Node 0 cannot have both color a and c
Node 0 cannot have both color b and c

Translated into a boolean expression:

¬a0 ∨ ¬b0
¬a0 ∨ ¬c0
¬b0 ∨ ¬c0

You would need to do the same for all nodes, so in total you'll have 3 * 5 = 15 such expressions for this type:

¬a0 ∨ ¬b0    ¬a1 ∨ ¬b1    ¬a2 ∨ ¬b2    ¬a3 ∨ ¬b3    ¬a4 ∨ ¬b4
¬a0 ∨ ¬c0    ¬a1 ∨ ¬c1    ¬a2 ∨ ¬c2    ¬a3 ∨ ¬c3    ¬a4 ∨ ¬c4
¬b0 ∨ ¬c0    ¬b1 ∨ ¬c1    ¬b2 ∨ ¬c2    ¬b3 ∨ ¬c3    ¬b4 ∨ ¬c4

Conclusion

All the above disjunctions (there are 21 + 5 + 15 = 41 of them) need to be true (conjugated). Such a problem is a Boolean satisfiability problem, and more particularly 3-SAT, and is an NP-Complete problem.

Code to produce the boolean expressions

The following code assumes that the Graph object will exposes a nodes list where each node has an id and neighbors.

The disjunctions are output as strings, each on a separate line:

Graph g1 = new Graph(5);
g1.addEdge(0, 1);
g1.addEdge(0, 2);
g1.addEdge(1, 2);
g1.addEdge(1, 3);
g1.addEdge(3, 2);
g1.addEdge(3, 4);
g1.addEdge(4, 2);
char colors[] = {'a', 'b', 'c'};
// Type 1
for (Node node : g1.nodes) {
    for (Node neighbor : node.neighbors) {
        for (char color : colors) {
            System.out.println(String.format("¬%1$c%2$d ∨ ¬%1$c%3$d", color, node.id, neighbor.id));
        }
    }
}
// Type 2
for (Node node : g1.nodes) {
    String expr[] = new String[colors.length];
    int i = 0;
    for (char color : colors) {
        expr[i++] = String.format("%s%d", color, node.id);
    }
    System.out.println(String.join(" ∨ ", expr));
}
// Type 3
for (Node node : g1.nodes) {
    for (char color1 : colors) {
        for (char color2 : colors) {
            if (color1 < color2) {
                System.out.println(String.format("¬%1$c%3$d ∨ ¬%2$c%3$d", color1, color2, node.id));
            }
        }
    }
}

If I have to write these formulas together, are they connected by and (&&), as mentioned by @maraca ?
Yes, as I wrote in the conclusion paragraph they need to all be true, which means they must be conjugated (i.e. AND operator).

maraca · Accepted Answer · 2017-05-06 14:35:21Z

1

You get an equation for each edge and connect them with and (ci is the color used for vertex i):

c0 != c1 && c0 != c2 && c1 != c2 && c1 != c3 && c2 != c3 && c2 != c4 && c3 != c4

The boolean formula only checks if you have found a valid coloring for the graph, not if the number of colors is minimized.

edited May 6, 2017 at 14:35

answered May 6, 2017 at 14:26

maraca

9,5873 gold badges27 silver badges50 bronze badges

Comments

Rhyd Lewis · Accepted Answer · 2025-01-13 11:53:12Z

0

As a point of interest, we can also say something similar in reverse. That is, all boolean expressions can be expressed as graph coloring problems.

To do this, take an arbitrary boolean expression (a satisfiability problem), and write it out in 3-conjunctive normal form. From this, we can convert the latter expression into a graph that is 3-colorable if and only if the original expression is satisfiable. This proves that the graph 3-coloring problem in NP-complete.

Here's an example based on the proof of Karp (1972). (Karp, M. "Complexity of Computer Computations", Reducibility Among Combinatorial Problems, pages 85–103. Plenum, New York, 1972.)

answered Jan 13 at 11:53

Rhyd Lewis

671 silver badge4 bronze badges

Collectives™ on Stack Overflow

Boolean formula for a graph vertex-colouring algorithm

3 Answers 3

1. Two adjacent nodes cannot have the same color

3. No nodes can get more than one color

Conclusion

Code to produce the boolean expressions

2 Comments

Comments

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

3 Answers 3

1. Two adjacent nodes cannot have the same color

3. No nodes can get more than one color

Conclusion

Code to produce the boolean expressions

2 Comments

Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Related