“检查K个节点的循环是否存在”还原为SAT？

Question

我收到以下问题陈述：

“给定一个无向图，检查是否存在 K 个节点的循环。”

我想获取任何输入并将其转换为 SAT 求解器的合取范式公式。

第一步是创建变量。我们有 N 个变量，表示节点是否是循环的一部分，以及 M 个变量，它们对于边来说是相同的。

第二部分是通过条款制定约束。我们首先添加一个约束“x1 + x2 + ... + xn = k”。一种方法是创建 nCk 个子句，这将代表所有可能的选择。然而，我正在努力设置其余的约束来检查所选节点是否形成循环。

我想过重新创造DNF中的所有可能性，然后将其转化为CNF，但这会产生太多子句。

有什么建议可以以 CNF 形式解决这个问题吗？ （对不起我的英语）

Answer 1

我们首先添加一个约束“x1 + x2 + ... + xn = k”。一种方法是创建 nCk 子句，它代表所有可能的选择。

另一种选择是创建计数电路（Tseytin 变换）或分类器，然后将其输出限制为

k

。这引入了额外的变量。

但是，我正在努力设置其余约束以检查所选节点是否形成循环。

我也不知道在该公式中解决它的好方法，但是您可以更改变量以使其能够在没有指数数量的子句的情况下解决该问题：

• 让

  x[i,j]

  指示节点

  i

  是否位于循环中的位置

  j

  。
• 限制每个节点最多使用一次。 O(n²) 个子句
• 限制每个位置只有一个与之关联的节点。 O(kn²) 条
• 约束每对不相邻节点不位于位置

  s

  和

  s+1

  （包括环绕）。 O(kn²) 条