1

我希望就如何实现这一点提出建议：

定义：无向图 G 由顶点集 V 和边集 E 定义，其中每条边是大小为 2 的 V 的子集，即无序顶点对 {u, v}。G中长度为k的循环是不同顶点的序列v_1，...，v_k，其中{v_1，v_2}，{v_2，v_3}，...，{v_k-1，v_k}，{v_k，v_1 } 是 G 的所有边。G 中的哈密顿循环是长度为 n = |V| 的循环，即恰好通过图的每个顶点一次的 chcle。如果 G 有一个哈密顿循环，我们称它为 G 哈密顿量。

问题：提供以下决策问题的命题逻辑公式：给定一个无向图 G，G 是哈密顿量吗？配方将由 Z3 检查。

输入格式将是：

4
0 1
1 2
2 3
3 0
1 3

其中第一个数字表示顶点的数量，其余的对都是 G 中的边。

输出应该是：0 1 2 3

显然，输出将始终是数字 1、...、n-1 的某种排列，其中 n = |V| 但我看不到如何仅使用命题逻辑来处理整数。

任何建议表示赞赏。

问候。

这是适用于给定输入的解决方案。如果我可以编写一个 perl 例程来生成边的组合（n 选择 k），那么我可以将其推广到任意数量的输入：

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)

(declare-const e1 Bool)
(declare-const e2 Bool)
(declare-const e3 Bool)
(declare-const e4 Bool)
(declare-const e5 Bool)

(assert (xor (and e1 e2 e3 e4) (and e1 e2 e3 e5) (and e1 e2 e4 e5) (and e1 e3 e4 e5) (and e2 e3 e4 e5)))

(assert (and v0 v1 v2 v3))

(assert (=> e1 (and v0 v1)))
(assert (=> e2 (and v1 v2)))
(assert (=> e3 (and v2 v3)))
(assert (=> e4 (and v3 v0)))
(assert (=> e5 (and v1 v3)))

(check-sat)
(get-model)
4

2 回答 2

2

这个想法是让 SMT 求解器生成 n 个数字，比如 a1..an，然后断言以下所有内容：

  • 所有这些数字都在 0 和 n-1 之间
  • 所有的数字都是不同的
  • 顶点 a1 .. an 形成一个循环，即检查 a1-a2、a2-a3、...、a(n-1)-an 和 an-a1 之间是否存在边

也就是说，您只需描述什么是“哈密顿循环”，如果确实存在，SMT 求解器就会找到它。

现在，困难在于如何在 SMTLib2 中表达所有这些，以便 Z3 可以解析它。当然可以，但我建议使用更高级的语言来提供与 SMT 求解器的绑定。例如，Haskell 和 Scala 就是您可以使用 Z3 编写脚本的两种语言。这样，您只需专注于问题，宿主语言将在幕后为您处理翻译。这需要在学习宿主语言和相关库方面进行一些投资，但在我看来这是非常值得的。

例如，以下是使用 Haskell 和 Z3 解决此问题的方法：http: //gist.github.com/1715097。解决方案是仅仅 7 行 Haskell，您可以使用它来查询您想要的任何大小的图形。该解决方案利用了 Haskell 的表达能力和 Z3 的 SMT 求解器功能，呈现出简洁的界面。

于 2012-02-01T04:32:50.353 回答
1

您可以使用布尔变量对边缘关系进行编码，例如使用 R-5-4 来表示 R 中的 if (5,4)。

让 E 成为您的输入边关系。

将关系 R 约束为 E 的子集，使得每个顶点都恰好连接到 R 中的两条边。

现在将关系 T 约束为 R 的传递闭包。

如果 T 是全连接的（所有 T-n1-n2 都为真），则 R 是 Hamilton 圈， (V,E) 是 Hamilton 图。

于 2017-01-24T09:14:52.370 回答