% Input graph is undirected, but we use its directed representation
% just because it is easier to deal with it.
edge(Y,X) :- edge(X,Y).
edgewt(Y,X,W) :- edgewt(X,Y,W).

cycle(X,Y) v non_cycle(X,Y) :- edge(X,Y).

% Each node must have exactly one incoming and one outgoing arc.
:- vtx(X), not #count{Y : cycle(X,Y)} = 1.
:- vtx(Y), not #count{X : cycle(X,Y)} = 1.

% Each node must be reached.
reached(X) :- cycle(1,X).
reached(Y) :- reached(X), cycle(X,Y).
:- vtx(X), not reached(X).

% Total weight must not exceed the maximum weight W.
:- maxweight(W), W < #sum{C,X,Y : edgewt(X,Y,C), cycle(X,Y)}.