z3 - 使用 Z3 求解简单的 TSP

Question

我是 SMT 求解器的新手。我想知道如何编码具有 4/6 个节点的简单 TSP 问题？我很困惑如何使用 Z3pay APA 设置我的约束。任何形式的提示或帮助将不胜感激。

Answer 1

您可以将您的 TSP 问题表述为ILP问题。现在的问题是如何将 TSP 编码为 ILP。有两个众所周知的答案：Miller-Tucker-Zemlin和Dantzig-Fulkerson-Johnson。

基本思想如下：假设我们有n个城市。让我们用 d_ij 表示城市 i 和 j 之间的距离，让我们用 x_{ij} 表示布尔值（0 或 1），TSP 是否包含从 i 到 j 的边。然后找到最小的旅行意味着

minimize sum_{i,j} x_{ij} d_{ij}

使得 x_{ij} 描述一个循环。在这两个条件下，我们得到一个或多个循环：

sum_{j} x_{ij} = 1 for all i              exactly one outgoing edge per city
sum_{i} x_{ij} = 1 for all j              exactly one ingoing edge per city

现在我们必须排除解决方案包含多个循环的情况。我们可以添加这个指数级的Dantzig-Fulkerson-Johnson条件：

sum_{i in S} sum_{j in S} x_{ij} < |S| for all proper subsets S of {1, ..., n}

请注意，如果我们的解决方案包含两个循环，那么 S 是其中一个循环的顶点集，则 x_{ij}-sum 将为 |S|。另一方面，如果只有一个循环，则 x_{ij}-sum 永远不会达到 |S|，例如，如果从 {1, ..., n} 中删除一个顶点，则剩余边数为n-2，但 |S| = n-1。

当然，指数数量的约束不是我们想要的，所以我们寻找一种更聪明的方法来排除子循环情况。这就是米勒-塔克-泽姆林介入的地方。

另一种方法是简单地忽略子循环问题，计算解决方案并检查解决方案是否包含子循环。如果是这样，则通过将其添加为惰性约束来排除该解决方案并重复直到获得单周期解决方案。这里的关键字是惰性约束。

Answer 2

有一个很好的示例可能对您有用：http: //z3.codeplex.com/SourceControl/changeset/view/1235b3ea24d9#examples/python/hamiltonian/hamiltonian.py