ASP Core-2: Infinite Loop in Hamiltonian Path Solver

Question

I am totally new in answer set proramming (ASP Core-2 with Clingo) and am struggling with a problem I have not been able to solve. The goal is to solve the 'Hamiltonian Path' problem, which is described as follows: In a directed graph we're looking for a path which visits all nodes of the graph exactly once.

We can assume that all edge relations are known as facts, and that the input graph does actually contain a Hamiltonian Path. The desired output are the predicates

visited(NodeName, StepInOrder)

that each contains a node and the number at which step this node is reached. So for example, an output could be

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

See my code below. The problem is, that at the last line, the program seems to enter an infinite loop. And I do not understand what the cause of this could probably be.

% 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...

My guess is, that the program is generating an infinite number of answer sets, which all differ in their #stepInOrder value, because of some sort of cycle, but I thought this should be prevented by the not visited(Y, _).

If you need any additional context, let me know. Thanks in advance!

Answer 1

Lets go through your code:

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

I guess this works, but just writing 1 {startNode(N) : node(N)} 1. or {startNode(N) : node(N)} == 1. would do the same.

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

This one works, allthough there are more efficient approaches to write it.

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

You basically say: a node Y is visited at time C+1, if a node X was visited at time C, there is a path from X to Y, and at no time Y was visited or will be visited. So you clearly want to generate something but if you generate it you violate the rule which generated it. In clingo atoms can not change values. If an atom is labeled as True, it is True the whole time.

So I would probably write something like this:

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

which reads: given X is visited at time C, the number of outgoing marked edges from X to any node Y is exactly 1. Mark Y as visited at time C+1.

All what is missing now, is a constraint to include all nodes to be visited.

You might want to have a look at this question from around the same time. The solution of the user has a different approach, he or she does not assign numbers to the nodes to indicate an order.