Solving Hamiltonian cycle in answer set programming

Question

Hamiltonian cycle instantiation and encoding:

% vertices: n=node
n(1..4).

% edges: e=edge
e(1,(2;3)). e(2,(3;4)). e(3,(1;4)). e(4,1).

% starting point
s(1).


# p=path, o=omit, op=on-path, r=reach, s=start% generate path
p(X,Y):- not o(X,Y), e(X,Y).
o(X,Y):- not p(X,Y), e(X,Y).

% at most one incoming/outgoing edge
:- p(X,Y), p(U,Y), X < U.
:- p(X,Y), p(X,V), Y < V.
    
% at least one incoming/outgoing edge
op(Y):- p(X,Y), p(Y,Z).
:-  n(X), not op(X).
    
% connectedness
r(X):- s(X).
r(Y):- r(X), p(X,Y).
:- n(X), not r(X).

Solver: ! clingo file_name.lp
Return:

clingo version 5.6.2
Reading from encoding.lp
Solving...
UNSATISFIABLE

Models       : 0
Calls        : 1
Time         : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

My question is: is this program really unsatisfiable or am I encoding it the wrong way?

Answer 1

No, it is not unsatisfiable. There exists indeed exactly one Hamiltonian cycle from a, which is clearly a->b->c->d(->a).

You are just declaring the nodes using numbers, but the starting node is a (not a number).

The part in which you encoded the logics of the problem looks ok to me.

Replacing s(a) with s(1) we obtain SATISFIABLE as result:

clingo version 5.3.0
Reading from test.lp
Solving...
Answer: 1
n(1) n(2) n(3) n(4) e(4,1) e(1,2) e(1,3) e(2,3) e(2,4) e(3,1) e(3,4) s(1) r(1) p(1,2) o(1,3) p(2,3) r(2) r(3) op(2) p(4,1) o(2,4) o(3,1) p(3,4) r(4) op(4) op(1) op(3)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

---

P.S. Note that the two following lines:

p(X,Y):- not o(X,Y), e(X,Y).
o(X,Y):- not p(X,Y), e(X,Y).

can be compacted with:

p(X,Y) | o(X,Y) :- e(X,Y).