Detecting even cycles in a directed graph using answer set programming (clingo)?

I struggled a bit with that task. But I want to know, how I can detect if there is an even cycle in a directed graph using answer set programming with clingo. If there is an even cycle, the program should return satisfiable, if there is no even cycle then unsatisfiable.

vertexes are coded as vt(x), and edges as edge(x,y).

Example 1: vt(a), vt(b), vt(c), vt(d) with edge(a,b), edge(b,c), edge(c,a) should return unsatisfiable. Here we have one odd cycle with a,b,c.

Example 2: vt(a), vt(b), vt(c), vt(d) with edge(a,b), edge(b,c), edge(c,a), edge(a,d), edge(d,a) should return satisfiable. Here we have one odd cycle a,b,c and one even cycle a,d.

I tried using a reachable/3 predicate where the third component is a counter which counts the current length of the path. Then check if the number is even, though it doesnt work properly.

You can achieve what you want by using the following program:

% if there exists an edge from X to Y, then there exists an odd path from X to Y
oddPath(X,Y) :- edge(X,Y) .

% if there exists an even path from X to Y an edge from Y to Z, then there exists an odd path from X to Z
oddPath(X,Z) :- evenPath(X,Y), X!=Y, edge(Y,Z) .

% if there exists an odd path from X to Y an edge from Y to Z, then there exists an even path from X to Z
evenPath(X,Z) :- oddPath(X,Y), X!=Y, edge(Y,Z) .

% if X is a node and there exists an even path from X to itself, then there exists an even cycle
existsEvenCycle :- vt(X), evenPath(X,X) .

% the program is satisfiable if and only if there exists an even cycle
:- not existsEvenCycle .

All the rules are explained in the code.

Note that the two X!=Y are necessary since a cycle shouldn't be "walked" twice (otherwise every odd cycle would also be even).