-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathexp.py
208 lines (146 loc) · 5.96 KB
/
exp.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
#####################################
# File to house the experimentation
##################################
from krrt.utils import get_file_list, write_file, get_opts
from krrt.utils import experimentation as exp
import os
USAGE = """
python exp.py <experiment>
Where <experiment> is one of the following:
size_time: Compare the runtime / size of ddnnf and c2d compilation.
bdg_settings: Compare the various settings for the bdg compilation.
ddnnf_settings: Compare the various settings for the ddnnf compilation.
"""
###################
# Global Settings #
###################
all_domains = ['flat200-479', 'uf200-860', 'blocksworld', 'bmc', 'logistics', 'emptyroom-DRD', 'grid-DRD', 'sortnet-DRD']
#all_domains = ['flat200-479', 'uf200-860', 'blocksworld', 'emptyroom-DRD', 'grid-DRD', 'sortnet-DRD']
TIMEOUT = 1800 # 30min timeout
CORES = 2 # Run on a dual core machine
MEMORY = 1500 # Max of 1.5 gigs RAM
################################
# Runtime and size comparisons #
################################
def test_size_time(domain):
print "\nTesting domain '%s'." % domain
problems = get_file_list("exp-input/%s" % domain)
results_size = {}
results_time = {}
print "Doing ddnnf..."
results_ddnnf = exp.run_experiment(
base_command = "./sharpSAT-ddnnf -q",
single_arguments = {'problem': problems},
time_limit = TIMEOUT,
results_dir = "results-%s-ddnnf" % domain,
processors = CORES,
memory_limit = MEMORY,
progress_file = None
)
for result_id in results_ddnnf.get_ids():
file, size, time = _get_file_size_time_bdg(results_ddnnf[result_id])
results_size[file] = [size]
results_time[file] = [time]
print "\t...done!"
print "Doing c2d..."
results_c2d = exp.run_experiment(
base_command = "c2d",
parameters = {'-in': problems},
time_limit = TIMEOUT,
results_dir = "results-%s-c2d" % domain,
processors = CORES,
memory_limit = MEMORY,
progress_file = None
)
for result_id in results_c2d.get_ids():
file, size, time = _get_file_size_time_c2d(results_c2d[result_id])
results_size[file].append(size)
results_time[file].append(time)
print "\t...done!"
#-- Compile
file_output = "problem,ddnnf runtime,c2d runtime,ddnnf size,c2d size\n"
for prob in results_size.keys():
file_output += "%s,%f,%f,%d,%d\n" % (prob,
results_time[prob][0], results_time[prob][1],
results_size[prob][0], results_size[prob][1])
write_file(domain + '-results.csv', file_output)
#-- Cleanup
os.system("rm exp-input/%s/*.nnf" % domain)
def _get_file_size_time_bdg(result):
file = result.single_args['problem']
file_name = file.split('/')[-1]
output = result.output_file
if result.timed_out:
return (file_name, -1, result.runtime)
else:
size = exp.get_value(output, '.*Compressed Edges: (\d+).*', value_type=int)
return (file_name, size, result.runtime)
def _get_file_size_time_c2d(result):
file = result.parameters['-in']
file_name = file.split('/')[-1]
output = result.output_file
if result.timed_out:
return (file_name, -1, result.runtime)
else:
size = exp.get_value(output, '.*nodes and (\d+) edges...done.*', value_type=int)
return (file_name, size, result.runtime)
######################
# Parameter Analysis #
######################
def test_settings(domain, CMD):
problems = get_file_list("exp-input/%s" % domain)
toggles = ['PP', 'CA', 'NCB', 'CC', 'IBCP']
results = exp.run_experiment(
base_command = "%s -q" % CMD,
single_arguments = {'problem': problems,
'PP': ['-noPP', ''],
'CA': ['-noCA', ''],
'CC': ['-noCC', ''],
'NCB': ['-noNCB', ''],
'IBCP': ['-noIBCP', '']},
time_limit = TIMEOUT,
memory_limit = MEMORY,
results_dir = "results-%s-settings" % domain,
processors = CORES,
progress_file = None
)
#-- Compile
file_output = "%s,problem,size,runtime\n" % ','.join(toggles)
for result in results.get_ids():
res = results[result]
for tog in toggles:
if '' == res.single_args[tog]:
file_output += '1,'
else:
file_output += '0,'
file_output += "%s,%d,%f\n" % _get_file_size_time_bdg(res)
write_file(domain + '-results.csv', file_output)
######################################
opts, flags = get_opts()
did_something = False
if '-domain' in opts:
all_domains = [opts['-domain']]
if 'size_time' in flags:
did_something = True
if not os.path.isdir('size_time_results'):
os.system('mkdir size_time_results')
for dom in all_domains:
test_size_time(dom)
os.system('mv results-* size_time_results')
os.system('mv *-results.csv size_time_results/')
if 'bdg_settings' in flags:
did_something = True
os.system('mkdir bdg_settings_results')
for dom in all_domains:
test_settings(dom, './sharpSAT-bdg')
os.system('mv results-* bdg_settings_results')
os.system('mv *-results.csv bdg_settings_results')
if 'ddnnf_settings' in flags:
did_something = True
os.system('mkdir ddnnf_settings_results')
for dom in all_domains:
test_settings(dom, './sharpSAT-ddnnf')
os.system('mv results-* ddnnf_settings_results')
os.system('mv *-results.csv ddnnf_settings_results')
if not did_something:
print USAGE