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

Question

我是答案集编程（带有 Clingo 的 ASP Core-2）的新手，并且正在努力解决我无法解决的问题。 目标是解决“哈密顿路径”问题，描述如下： 在有向图中，我们正在寻找一条只访问一次图的所有节点的路径。

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

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

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

所以我可能会这样写：

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

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

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

您可能想在同一时间查看this question。用户的解决方案有不同的做法，他或她不给节点分配数字来指示顺序。