将无向图转换为 CNF SAT 以进行 3 着色

Question

现在，为了将其转化为 CNF SAT 问题，我理解：

1. 每个节点必须至少有一种颜色。
2. 每个节点最多只能有一种颜色。
3. 连接的节点不能有相同的颜色。

但我无法继续前进，因为我不知道要返回什么。如果我们有一个函数Convert(graph)，其中图有3个节点，即nodes = (0,1,2)和3个边，即edges = [(0,1), (0,2), (1,2)]，可能有colors = (1,2,3)； 对于这种特殊情况，转换为 CNF SAT 表格的输出应该是什么样的？谢谢

Answer 1

这是一个简单的直接编码：

对于每个节点，引入 k 个变量（k = 颜色数），以及一个简单列出这些变量的子句（强制选择至少一种颜色）。

对于每条边 (X, Y) 和颜色 c，引入防止 X 和 Y 同时具有颜色 c 的二元子句，即-Xc -Yc。

对于此图，DIMACS 格式的总 CNF 可能如下所示：

p cnf 9 12
1 2 3 0
4 5 6 0
7 8 9 0
-1 -4 0
-2 -5 0
-3 -6 0
-4 -7 0
-5 -8 0
-6 -9 0
-1 -7 0
-2 -8 0
-3 -9 0

求解器可能会给出（例如，显然还有更多可能性）1 -2 -3 -4 -5 6 -7 8 -9 0，这意味着节点 0 得到颜色 1，节点 1 得到颜色 3，节点 2 得到颜色 2。

顺便注意，没有使用“每个节点最多只能有一种颜色”的约束。简单的后处理可以解决这个问题。对于某些图表和一些颜色数量，您可能会得到一个节点被分配多种颜色的结果（仅当它不与邻居共享这些颜色中的任何，并且通常如果可能的话它仍然会获胜'不会发生，因为求解器没有动力去做），你可以简单地选择其中任何一个。如果这不可接受，请为与节点关联的每对变量添加一个二进制子句，以禁止它们同时设置，例如-1 -2 0、-1 -3 0 等。

有更高级的编码可以更好地扩展到更大的图。