reachable(V) :- chosen(a, V).
reachable(V) :- chosen(U, V), reachable(U).

% Choose exactly one edge from each vertex.
chosen(U, V) :-
    edge(U, V), not other(U, V).
other(U, V) :-
    edge(U, V), not chosen(U, V).

% Every vertex must be reachable.
:- vertex(U), not reachable(U).
% You cannot choose two edges to the same vertex
:- chosen(U, W), U \= V, chosen(V, W).
:- chosen(W, U), U \= V, chosen(W, V).


%% %%% To use preliminary-DCC introduce the dcc/1 rules corresponding to
%% %%% the NMR-check (the translation will be prefomed by the compiler in
%% %%% the final version).
%% dcc(vertex(U)) :- not reachable(U).
%% dcc(not reachable(U)) :- vertex(U).
%% dcc(chosen(U,W)) :- U \= V, chosen(V,W).
%% dcc(chosen(U,W)) :- U \= V, chosen(V,W).
%% dcc(chosen(W,U)) :- U \= V, chosen(W,V).
%% dcc(chosen(W,U)) :- U \= V, chosen(W,V).

?- reachable(a).


#show chosen/2.