ASP Core-2：哈密顿路径求解器中的无限循环

Question

我完全不熟悉答案集编程（ASP Core-2 with Clingo）并且正在努力解决我无法解决的问题。目标是解决'Hamiltonian Path'问题，描述如下：在有向图中，我们正在寻找一条仅访问图中所有节点一次的路径。

我们可以假设所有边关系都被称为事实，并且输入图确实包含哈密顿路径。所需的输出是谓词

visited(NodeName, StepInOrder)

每个包含一个节点和到达该节点的步骤的编号。因此，例如，输出可能是

visited(a, 1), visited(c, 2), visited(b, 3)

请参阅下面的代码。问题是，在最后一行，程序似乎进入了无限循环。而且我不明白这可能是什么原因。

% pick one random start node
1 <= {startNode(N) : node(N)} <= 1.

% define helper predicate inPath which is true once and false once for each edge of the graph
{inPath(X, Y)} :- edge(X,Y).

% create possible paths
visited(X, 1) :- startNode(X).
visited(Y, C+1) :- visited(X, C), inPath(X, Y), not visited(Y, _).  % infinite loop here

% some killing constraints to eliminate invalid solution candidates...

我的猜测是，该程序正在生成无限数量的答案集，由于某种循环，它们的#stepInOrder 值都不同，但我认为这应该通过 not visited(Y, _).

如果您需要任何其他上下文，请告诉我。提前致谢！

Answer 1

让我们检查一下您的代码：

1 <= {startNode(N) : node(N)} <= 1.

我想这行得通，但只写 1 {startNode(N) : node(N)} 1. 或 {startNode(N) : node(N)} == 1. 也可以。

% define helper predicate inPath which is true once and false once for each edge of the graph
{inPath(X, Y)} :- edge(X,Y).

虽然有更有效的方法来编写它，但这个有效。

% create possible paths
visited(X, 1) :- startNode(X).
visited(Y, C+1) :- visited(X, C), inPath(X, Y), not visited(Y, _).  % infinite loop here

你基本上说：在时间 C+1 访问了节点 Y，如果在时间 C 访问了节点 X，则有一条路径来自 X 到 Y，并且 Y 从未被访问过或将被访问过。所以你显然想要生成一些东西，但是如果你生成了它，你就违反了生成它的规则。在 Clingo 中，原子不能更改值。如果一个原子被标记为真，那么它一直都是真。

所以我可能会这样写：

1 { visited(Y,C+1) : inPath(X,Y) } 1 :- visited(X, C).

内容为：给定 X 在时间 C 被访问，从 X 到任何节点 Y 的传出标记边的数量恰好是 1。标记 Y 时间 C+1.

现在所缺少的，是一个包含所有要访问的节点的约束。

您可能想在大约同一时间查看。用户的解决方案有不同的做法，他或她没有给节点分配编号来表示顺序。

ASP Core-2：哈密顿路径求解器中的无限循环

ASP Core-2: Infinite Loop in Hamiltonian Path Solver

answer-set-programming

clingo