A benchmark from the rule-reasoning world: 10,000 labelled edges and one rule that looks for walks of exactly ten edges, all with the same label, that return to where they started. EyeProlog finds 1,518 of them, proves each one, and checks every proof.
Run it in the playground · Source
The facts are triples edge(From, Label, To). A cycle for label R is a
sequence of nodes D0, D1, …, D9 where each consecutive pair is joined by an
R-edge and the last one leads back to D0.
The question is monadic because each answer is about a single relation label, and it is a benchmark because the search must stay selective over a large, random-looking graph.
edge(i30, i12, i33).
edge(i61, i29, i42).
edge(i57, i46, i87).
edge(i45, i35, i45).
edge(i6, i37, i6).
A few of the 10,000 edges. Some, like edge(i45, i35, i45), are self-loops:
node i45 points to itself under label i35.
cycle(R, [D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, D0]) :-
edge(D0, R, D1),
edge(D1, R, D2),
edge(D2, R, D3),
edge(D3, R, D4),
edge(D4, R, D5),
edge(D5, R, D6),
edge(D6, R, D7),
edge(D7, R, D8),
edge(D8, R, D9),
edge(D9, R, D0).
The head repeats D0 at both ends, which is how the rule says “closed”. The
body runs left to right, so each edge lookup already knows its start node and
label, and the clause index keeps every step cheap.
eyeprolog examples/basic-monadic.pl
cycle(i35, [i45, i45, i45, i45, i45, i45, i45, i45, i45, i45, i45]).
cycle(i37, [i6, i6, i6, i6, i6, i6, i6, i6, i6, i6, i6]).
cycle(i62, [i81, i24, i81, i24, i81, i24, i81, i24, i81, i24, i81]).
cycle(i62, [i81, i24, i81, i24, i81, i24, i81, i24, i81, i81, i81]).
cycle(i62, [i81, i24, i81, i24, i81, i24, i81, i81, i24, i81, i81]).
1,518 cycles in all (full output). A self-loop
gives a cycle that stays put; a small loop such as i81 → i24 → i81 can be
combined with a self-loop on i81 in many orders, which is why label i62
contributes so many answers.
eyeprolog --proof examples/basic-monadic.pl
step(cycle(i35, [i45, i45, i45, i45, i45, i45, i45, i45, i45, i45, i45]),
rule(10001),
['R' = i35,
'D0' = i45,
'D1' = i45,
'D2' = i45,
'D3' = i45,
'D4' = i45,
'D5' = i45,
'D6' = i45,
'D7' = i45,
'D8' = i45,
'D9' = i45],
[edge(i45, i35, i45),
edge(i45, i35, i45),
Clause 10,001 is the cycle rule (the 10,000 edges come first). The first answer uses the same self-loop ten times; the step lists all ten uses.
condition('C1', resolution, ok, 1883).
condition('C4', coverage, ok, 16698).
condition('C7', relevance, ok, 3401).
verdict(checked).
The checker replays all 1,883 steps against the program and confirms that every one of the 1,518 claims and their 16,698 uses is covered, without searching the graph again. Nothing is trusted.
--goal 'cycle(i37, Path)'. How many cycles does it
have, and why?--stats and compare the number of solver calls with the number of
edges. What keeps the search from trying all 10,000 edges at every step?edge(D9, R, D0), to the front of the rule. Does
the answer set change? Does the running time?Learn more in The Art of EyeProlog, Chapter 13 and Chapter 21.