In [368]:
%matplotlib
import os,sys
import numpy as np
import matplotlib
import matplotlib.pyplot as plt
import pylab
from IPython import display
from itertools import cycle
#from statsmodels.distributions.empirical_distribution import ECDF
In [369]:
bname_map=dict()
def read_data(path):
out=[]
with open(path) as f:
indata = f.readlines()
#Each line is full pathname and the running-time
for ale in indata:
toks = ale.split(",")
bmark = os.path.basename(toks[0]).strip()
runtime = int(toks[1])
out.append((bmark, runtime))
out=sorted(out, key=lambda tup:tup[1])
f.close()
return out
od = read_data("app_results_1")
In [370]:
bname_map = {k:v for (v,k) in enumerate([x for (x,y) in od] )}
#ensure dictionary items are set only once?
In [371]:
def joinify(od):
#[(cnf, runtime)] -> [(index, runtime)]
iod = []
for (c,r) in od :
i=bname_map[c]
iod.append((i,r))
iod = zip(*iod)
return iod
def rj(p) :
return joinify(read_data(p))
In [372]:
od = joinify(od)
#ecdf = ECDF(od[1])
#print ecdf
brc4=cycle(['r','g','0.5','b','black','0.6']) #Sequential
mk=cycle(['s','o','v','*','x'])
In [411]:
def plot_scatter():
matplotlib.rcParams.update({'font.size': 12})
matplotlib.rcParams.update({'lines.linewidth': 1.0})
fig = plt.figure(tight_layout=True)
ax = fig.add_subplot(1,1,1)
fig.set_size_inches(10,5)
ax.set_xlabel("Input")
ax.set_ylabel("Time (s)")
X=np.arange(27)
od=rj("app_results_1")
ax.plot(X, sorted(od[1]), ls='-', label='1', color=brc4.next(),marker=mk.next())
print od[0]
print X
od=rj("app_results_10_8")
ax.plot(X, sorted(od[1]), ls='-', label='10', color=brc4.next(),marker=mk.next())
od=rj("app_results_20_8")
ax.plot(X, sorted(od[1]), ls='-', label='20', color=brc4.next(),marker=mk.next())
od=rj("app_results_25_8")
ax.plot(X, sorted(od[1]), ls='-', label='25', color=brc4.next(),marker=mk.next())
od=rj("app_results_50_8")
ax.plot(X, sorted(od[1]), ls='-', label='50', color=brc4.next(),marker=mk.next())
od=rj("app_results_100_8")
ax.plot(X, sorted(od[1]), ls='-', label='100', color=brc4.next(),marker=mk.next())
ax.set_ylim(-20,1110)
major_ticks = np.arange(0, 30, 5)
minor_ticks = np.arange(0, 30, 1)
ax.set_xticks(major_ticks)
ax.set_xticks(minor_ticks, minor=True)
ax.grid(which='minor', alpha=0.7)
ax.grid(which='major', alpha=0.7)
ax.legend(loc='best')
plt.savefig("scatter_cdf.pdf", bbox_inches="tight")
return ax
In [412]:
plot_scatter()
Out[412]:
In [366]:
def plot_box():
matplotlib.rcParams.update({'font.size': 12})
matplotlib.rcParams.update({'lines.linewidth': 1.0})
fig = plt.figure(tight_layout=True)
ax = fig.add_subplot(1,1,1)
fig.set_size_inches(8,5)
ax.set_xlabel("Clause Sharing")
ax.set_ylabel("Time (s)")
d=[rj("app_results_1")[1], rj("app_results_10_8")[1], rj("app_results_20_8")[1], \
rj("app_results_25_8")[1], rj("app_results_50_8")[1], rj("app_results_100_8")[1]]
ax.boxplot(d)
ax.set_xticklabels(['1','10','20','25','50','100'])
plt.savefig("boxplot_all.pdf", bbox_inches="tight")
#plot_box()
In [386]:
def plot_compare():
#Compare ManySAT with parallel lingeling
matplotlib.rcParams.update({'font.size': 12})
matplotlib.rcParams.update({'lines.linewidth': 1.0})
fig = plt.figure(tight_layout=True)
ax = fig.add_subplot(1,1,1)
fig.set_size_inches(10,5)
ax.set_xlabel("Input")
ax.set_ylabel("Time (s)")
od=rj("app_results_1")
ax.plot(od[0], od[1], ls='None', label='ManySAT, c=1', color='black',marker='o')
od=rj("app_results_10_8")
ax.plot(od[0], od[1], ls='None', label='ManySAT, c=10', color='black',marker='s')
#open("../../lingeling-bal-2293bef-151109/app_results_1_8")
od=rj("../../lingeling-bal-2293bef-151109/app_results_0_4")
ax.plot(od[0], od[1], ls='None', label='plingeling, no sharing', color='r',marker='o')
od=rj("../../lingeling-bal-2293bef-151109/app_results_1_8")
ax.plot(od[0], od[1], ls='None', label='plingeling with sharing', color='r',marker='s')
ax.set_ylim(-20,1110)
major_ticks = np.arange(0, 30, 5)
minor_ticks = np.arange(0, 30, 1)
ax.set_xticks(major_ticks)
ax.set_xticks(minor_ticks, minor=True)
ax.grid(which='minor', alpha=0.7)
ax.grid(which='major', alpha=0.7)
ax.legend(loc='best')
plt.savefig("scatter_compare.pdf", bbox_inches="tight")
return ax
plot_compare()
Out[386]:
In [415]:
def cmp_manysat_lingeling():
matplotlib.rcParams.update({'font.size': 12})
matplotlib.rcParams.update({'lines.linewidth': 1.0})
fig = plt.figure(tight_layout=True)
ax = fig.add_subplot(1,1,1)
fig.set_size_inches(8,5)
ax.set_xlabel("Solver")
ax.set_ylabel("Time (s)")
d=[rj("app_results_1")[1], rj("../../lingeling-bal-2293bef-151109/app_results_0_4")[1], \
rj("app_results_10_8")[1], rj("../../lingeling-bal-2293bef-151109/app_results_1_8")[1]]
ax.boxplot(d)
ax.set_xticklabels(['dManySAT','pLingeling \n No Sharing','ManySAT, c=10','pLingeling \n With Sharing'])
plt.savefig("cmp_box.pdf", bbox_inches="tight")
cmp_manysat_lingeling()
In [ ]: