3 将给定图形着色为 Mini-Sat 格式的布尔表达式

Question

我正在做一个项目，我必须读取一个表示图形的文件。我使输入文件看起来像这样：

  b c
  a c d 
  a b 
  b

所以每一行表示一个节点。例如，第一行是连接到b 和c 的节点a，第二行是连接到a、c 和d 的节点b。所以我不确定从哪里开始。我知道我们需要一堆 if 和 else 语句，以便共享一条边的两个节点不能具有相同的颜色，并且每个节点应该至少具有一种颜色。但是，我怎样才能创建节点变量本身，因为文本文件可以包含任意数量的节点。我知道我必须为一堆 if 和 else 语句做些什么，但我不知道如何使用它来将其简化为 miniSAT 格式，例如：

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

其中第一个“3”代表变量的数量，第二个 3 代表子句的数量。其他行由不同的变量组成，每个不同的数字都是它自己的变量，如果是正数，则为真，否则为假

Answer 1

您实质上是在询问如何将 3 色减少到 CNF-SAT。我们先从怎么做开始，然后说说如何生成你需要的文件。

归约背后的基本思想如下：对于每个节点 x，我们将创建三个命题变量：x_r、x_g 和 x_b 指示分配给节点的颜色（红色、绿色或蓝色）。从那里，我们需要添加 in 子句来强制执行以下约束：

1. 每个节点都被赋予至少一种颜色，
2. 每个节点最多被赋予一种颜色，并且
3. 没有两个相邻节点被赋予相同的颜色。

为了编码点（1），我们可以使用这个子句：

(x_r ∨ x_g ∨ x_b)

为了编码点（2），我们可以使用三个子句，每个子句都排除了分配两种颜色的可能性：

(¬x_r ∨ ¬x_g) ∧

(¬x_g ∨ ¬x_b) ∧

(¬x_b ∨ ¬x_r)

最后是规则 (3)。我们基本上可以采用上述策略来解决这个问题。对于每对相邻节点 x 和 y，添加以下子句：

(¬x_r ∨ ¬y_r) ∧

(¬x_g ∨ ¬y_g) ∧

(¬x_b ∨ ¬y_b)

然后通过将所有这些子句进行 AND 运算来得出整体公式。

现在，问题是如何生成您想要生成的输出文件。有很多方法可以做到这一点。这里有几个选项：

1. 您可以直接从图中的节点和边数中准确计算出需要多少子句和变量，然后使用一些巧妙的算术技巧通过做一些数学运算来计算出每个子句对应的变量哪些索引。

2. 您可以构建变量和子句的一些内部表示（例如，有一个从节点到与其颜色变量关联的数字的映射，然后有一个子句列表），构建该表示，然后对其进行迭代生成输出文件。

我个人推荐选项 (2)，因为我认为这可能是最简单的方法。

希望这会有所帮助！