% Disjunctive encoding for Hamiltonian Cycle.
% 
% The input graph is to be encoded in the predicate arc/2;
% the starting node in the predicate start/1.

reached(X) :- in_hm(_,X).

in_hm(X,Y) v out_hm(X,Y) :- start(X), arc(X,Y).
in_hm(X,Y) v out_hm(X,Y) :- reached(X), arc(X,Y).

:- in_hm(X,Y), in_hm(X,Y1), Y != Y1.
:- in_hm(X,Y), in_hm(X1,Y), X != X1.

:- arc(X,_), not reached(X).

% Or
%   :- vertex(X), not reached(X).
% in case there is also another predicate vertex/1, which is needed
% when some vertex does not have an outgoing arc.