图着色算法的布尔公式

Question

我有一个有5个顶点的图。

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();

我需要用布尔表达式来表达着色这个图的问题。

假设a、b和c是三种颜色，而文字ai表示i有颜色a的顶点，那么上面的图可以这样着色：

a0, b1, c2, a3, b4

怎样才能得到布尔公式，当满足时，它为图的着色提供了一个解决方案。

Answer 1

您正在寻找图中所有顶点的着色，每个顶点都有三个可用的颜色，因此没有两个相邻的节点具有相同的颜色。

因此，有三种条件：

1.两个相邻的节点不能具有相同的颜色。

因此，例如，边(0，1)将意味着这三个约束：

• 节点0和1不能同时具有
• 节点0和1不能同时具有b颜色。
• 节点0和1不能同时具有c颜色。

转换成布尔表达式：

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

你需要为所有的边生成这样的三重奏。因此，总共有3x7=21个布尔析取：

¬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.所有节点都必须有颜色。

因此，例如，对于节点0，我们将具有以下约束：

• 节点0必须具有a、b或c颜色。

转换成布尔表达式：

a0 ∨ b0 ∨ c0

您需要对所有节点执行相同的操作，因此总共有5个这样的表达式：

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

3.任何节点都不能得到多个颜色。

因此，例如，对于节点0，我们将拥有：

• 节点0不能同时显示a和b颜色。
• 节点0不能同时显示a和c颜色。
• 节点0不能同时具有b和c颜色。

转换成布尔表达式：

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

您需要对所有节点执行相同的操作，因此，对于这种类型，总共需要3*5=15个这样的表达式：

¬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

结论

以上所有的析取(有21 +5+ 15 = 41 )都必须是真(共轭)。这样的问题是一个布尔可满足性问题，特别是3-SAT，是一个NP-完全问题.

生成布尔表达式的代码。

下面的代码假设Graph将公开一个节点列表，其中每个节点都有一个id和邻居。

这些析取作为字符串输出，每个字符串位于一个单独的行上：

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));
            }
        }
    }
}

看到它在repl.it上运行。

Answer 2

得到每个边的方程，并将它们与和(ci是顶点i的颜色)连接起来：

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

布尔公式只检查是否找到了图的有效着色，而不是最小的颜色数。