This page lists the exact benchmark encodings and commands used in the paper for reference, as well as additional information regarding the evaluation.
distributed-sr evaluate dump-case mmedia -e
high :- value(V),alpha(V) in [1 sec],18 <= V.
mid :- value(V),alpha(V) in [1 sec],12 <= V,V < 18.
low :- value(V),alpha(V) in [1 sec],V <= 12.
lfu :- high always in [1 sec].
lru :- mid always in [1 sec].
fifo :- low always in [1 sec],rtm50 in [1 sec].
done :- lfu.
done :- lru.
done :- fifo.
random :- not done.
value(5).
value(15).
value(25).
finish :- off in [1 sec],done.
finish :- off in [1 sec],random.For Ticker, the mmedia-at variant is used rather than mmedia, which preserves the original “@ in head” encoding. This is in accordance with the Ticker semantics, whereas our system does not require this. This way the behaviour should be as closely matched as possible.
Also note that in order to evaluate Ticker on its own, we run the system in single node mode. Since external reasoners are spawned as seperate processes and only the CPU time spend in this process and its children is counted, this is equivalent to benchmarking an “independent” Ticker instance. This process does not count any setup time of our system, or even the time required for supplying Ticker with data.
Accordingly, for external reasoners, the relevant timing columns are the child-user and child-sys columns. Only these are counted in the numbers published.
for w in (seq 1 18)
echo "Window size: " $w 1>&2
distributed-sr evaluate total-time mmedia-at -w $w -s --ticker ticker/ticker-assembly-1.0.jar --tick-interval 0.1
end 2> ticker-jtmsfor w in (seq 1 18)
echo "Window size: " $w 1>&2
distributed-sr evaluate total-time mmedia-at -w $w -s --ticker ticker/ticker-assembly-1.0.jar --tick-interval 0.1 --ticker-reasoner clingo
end 2> ticker-aspfor w in (seq 1 18)
echo "Window size: " $w 1>&2
distributed-sr evaluate total-time mmedia -w $w --ticker ticker/ticker-assembly-1.0.jar --tick-interval 0.1
end 2> distributed-jtmsNote that the at-Encoding is no longer necessary here.
for w in (seq 1 18)
echo "Window size: " $w 1>&2
distributed-sr evaluate total-time mmedia -w $w
end 2> distributed-aspdistributed-sr evaluate dump-case nqueens-2 -e
We present the encoding for 2 stages here. For 4 and 6 stages, adjust the
command line accordingly. Note that before passing the program to ticker, atoms
such as -q1 get replaced by n_q1. This happens to circumvent a parsing
restriction present in Ticker. Note that the constraints here are formulated as
odd loops. We automatically represent constraints in this way for compatibility
with Ticker’s parser, specifically for our benchmarks with Ticker-ASP.
q1(X,Y) :- d1(Y),d1(X),not -q1(X,Y).
-q1(X,Y) :- d1(Y),d1(X),not q1(X,Y).
aux1 :- q1(X1,Y),q1(X2,Y),X1 < X2,not aux1.
aux1 :- q1(X,Y1),q1(X,Y2),Y1 < Y2,not aux1.
aux1 :- q1(X1,Y1),q1(X2,Y2),X1 < X2,Y1 < Y2,d1(Z1),d1(Z2),Z1 = X2 - X1,Z2 = Y2 - Y1,Z1 = Z2,not aux1.
aux1 :- q1(X1,Y1),q1(X2,Y2),X1 < X2,Y2 < Y1,d1(Z1),d1(Z2),Z1 = X2 - X1,Z2 = Y1 - Y2,Z1 = Z2,not aux1.
placed1(X) :- q1(X,Y),d1(Y).
aux1 :- not placed1(X),d1(X),not aux1.
send1(Y) :- q1(1,Y).
#show q1/1.
q1(1,Y) :- send0(Y) in [50 msec],d1(Y).
d1(1).
d1(2).
d1(3).
d1(4).
d1(5).
d1(6).
d1(7).
d1(8).
d1(9).
d1(10).
d1(11).
d1(12).
d1(13).
d1(14).
d1(15).
d1(16).
d1(17).
d1(18).
q2(X,Y) :- d2(Y),d2(X),not -q2(X,Y).
-q2(X,Y) :- d2(Y),d2(X),not q2(X,Y).
aux2 :- q2(X1,Y),q2(X2,Y),X1 < X2,not aux2.
aux2 :- q2(X,Y1),q2(X,Y2),Y1 < Y2,not aux2.
aux2 :- q2(X1,Y1),q2(X2,Y2),X1 < X2,Y1 < Y2,d2(Z1),d2(Z2),Z1 = X2 - X1,Z2 = Y2 - Y1,Z1 = Z2,not aux2.
aux2 :- q2(X1,Y1),q2(X2,Y2),X1 < X2,Y2 < Y1,d2(Z1),d2(Z2),Z1 = X2 - X1,Z2 = Y1 - Y2,Z1 = Z2,not aux2.
placed2(X) :- q2(X,Y),d2(Y).
aux2 :- not placed2(X),d2(X),not aux2.
send2(Y) :- q2(2,Y).
#show q2/1.
q2(1,Y) :- send1(Y) in [50 msec],d2(Y).
d2(1).
d2(2).
d2(3).
d2(4).
d2(5).
d2(6).
d2(7).
d2(8).
d2(9).
d2(10).
d2(11).
d2(12).
d2(13).
d2(14).
d2(15).
d2(16).
d2(17).
d2(18).
finish :- off in [180 sec],q2(X,Y),d2(X),d2(Y).
#show finish/0.for n in (seq 2 2 6)
echo "Stages:" $n 1>&2
distributed-sr evaluate load-test nqueens-$n -u 1.0 -l 0.1
end 2> load-distributedfor n in (seq 2 2 6)
echo "Stages:" $n 1>&2
distributed-sr evaluate load-test nqueens-$n -u 1.0 -l 0.1
end 2> load-singlenodefor n in (seq 2 2 6)
echo "Stages:" $n 1>&2
distributed-sr evaluate load-test nqueens-$n -u 1.0 -l 0.1 --ticker ticker/ticker-assembly-1.0.jar --tick-interval 1 --ticker-reasoner clingo
end 2> load-tickerWhile we did benchmark Ticker-ASP on this problem, we omit the results in the charts printed, since not a single run resulted in anything but a timeout. As noted in the paper, Ticker-JTMS cannot handle this problem because of the presence of odd loops.
All experiments were conducted on a machine of the following specifications