-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathREADME.html
344 lines (320 loc) · 46.4 KB
/
README.html
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>FastBATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks</title>
<style>
/* From extension vscode.github */
/*---------------------------------------------------------------------------------------------
* Copyright (c) Microsoft Corporation. All rights reserved.
* Licensed under the MIT License. See License.txt in the project root for license information.
*--------------------------------------------------------------------------------------------*/
.vscode-dark img[src$=\#gh-light-mode-only],
.vscode-light img[src$=\#gh-dark-mode-only] {
display: none;
}
/* From extension vscode.markdown-math */
@font-face{font-family:KaTeX_AMS;font-style:normal;font-weight:400;src:url(fonts/KaTeX_AMS-Regular.woff2) format("woff2"),url(fonts/KaTeX_AMS-Regular.woff) format("woff"),url(fonts/KaTeX_AMS-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Caligraphic;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Caligraphic-Bold.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Bold.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Caligraphic;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Caligraphic-Regular.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Regular.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Fraktur;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Fraktur-Bold.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Bold.woff) format("woff"),url(fonts/KaTeX_Fraktur-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Fraktur;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Fraktur-Regular.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Regular.woff) format("woff"),url(fonts/KaTeX_Fraktur-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Main-Bold.woff2) format("woff2"),url(fonts/KaTeX_Main-Bold.woff) format("woff"),url(fonts/KaTeX_Main-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:italic;font-weight:700;src:url(fonts/KaTeX_Main-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Main-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Main-BoldItalic.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:italic;font-weight:400;src:url(fonts/KaTeX_Main-Italic.woff2) format("woff2"),url(fonts/KaTeX_Main-Italic.woff) format("woff"),url(fonts/KaTeX_Main-Italic.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Main-Regular.woff2) format("woff2"),url(fonts/KaTeX_Main-Regular.woff) format("woff"),url(fonts/KaTeX_Main-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Math;font-style:italic;font-weight:700;src:url(fonts/KaTeX_Math-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Math-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Math-BoldItalic.ttf) format("truetype")}@font-face{font-family:KaTeX_Math;font-style:italic;font-weight:400;src:url(fonts/KaTeX_Math-Italic.woff2) format("woff2"),url(fonts/KaTeX_Math-Italic.woff) format("woff"),url(fonts/KaTeX_Math-Italic.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:normal;font-weight:700;src:url(fonts/KaTeX_SansSerif-Bold.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Bold.woff) format("woff"),url(fonts/KaTeX_SansSerif-Bold.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:italic;font-weight:400;src:url(fonts/KaTeX_SansSerif-Italic.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Italic.woff) format("woff"),url(fonts/KaTeX_SansSerif-Italic.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:normal;font-weight:400;src:url(fonts/KaTeX_SansSerif-Regular.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Regular.woff) format("woff"),url(fonts/KaTeX_SansSerif-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Script;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Script-Regular.woff2) format("woff2"),url(fonts/KaTeX_Script-Regular.woff) format("woff"),url(fonts/KaTeX_Script-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size1;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size1-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size1-Regular.woff) format("woff"),url(fonts/KaTeX_Size1-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size2;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size2-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size2-Regular.woff) format("woff"),url(fonts/KaTeX_Size2-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size3;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size3-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size3-Regular.woff) format("woff"),url(fonts/KaTeX_Size3-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size4;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size4-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size4-Regular.woff) format("woff"),url(fonts/KaTeX_Size4-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Typewriter;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Typewriter-Regular.woff2) format("woff2"),url(fonts/KaTeX_Typewriter-Regular.woff) format("woff"),url(fonts/KaTeX_Typewriter-Regular.ttf) format("truetype")}.katex{text-rendering:auto;font:normal 1.21em KaTeX_Main,Times New Roman,serif;line-height:1.2;text-indent:0}.katex *{-ms-high-contrast-adjust:none!important;border-color:currentColor}.katex .katex-version:after{content:"0.13.24"}.katex .katex-mathml{clip:rect(1px,1px,1px,1px);border:0;height:1px;overflow:hidden;padding:0;position:absolute;width:1px}.katex .katex-html>.newline{display:block}.katex .base{position:relative;white-space:nowrap;width:-webkit-min-content;width:-moz-min-content;width:min-content}.katex .base,.katex .strut{display:inline-block}.katex .textbf{font-weight:700}.katex .textit{font-style:italic}.katex .textrm{font-family:KaTeX_Main}.katex .textsf{font-family:KaTeX_SansSerif}.katex .texttt{font-family:KaTeX_Typewriter}.katex .mathnormal{font-family:KaTeX_Math;font-style:italic}.katex .mathit{font-family:KaTeX_Main;font-style:italic}.katex .mathrm{font-style:normal}.katex .mathbf{font-family:KaTeX_Main;font-weight:700}.katex .boldsymbol{font-family:KaTeX_Math;font-style:italic;font-weight:700}.katex .amsrm,.katex .mathbb,.katex .textbb{font-family:KaTeX_AMS}.katex .mathcal{font-family:KaTeX_Caligraphic}.katex .mathfrak,.katex .textfrak{font-family:KaTeX_Fraktur}.katex .mathtt{font-family:KaTeX_Typewriter}.katex .mathscr,.katex .textscr{font-family:KaTeX_Script}.katex .mathsf,.katex .textsf{font-family:KaTeX_SansSerif}.katex .mathboldsf,.katex .textboldsf{font-family:KaTeX_SansSerif;font-weight:700}.katex .mathitsf,.katex .textitsf{font-family:KaTeX_SansSerif;font-style:italic}.katex .mainrm{font-family:KaTeX_Main;font-style:normal}.katex .vlist-t{border-collapse:collapse;display:inline-table;table-layout:fixed}.katex .vlist-r{display:table-row}.katex .vlist{display:table-cell;position:relative;vertical-align:bottom}.katex .vlist>span{display:block;height:0;position:relative}.katex .vlist>span>span{display:inline-block}.katex .vlist>span>.pstrut{overflow:hidden;width:0}.katex .vlist-t2{margin-right:-2px}.katex .vlist-s{display:table-cell;font-size:1px;min-width:2px;vertical-align:bottom;width:2px}.katex .vbox{align-items:baseline;display:inline-flex;flex-direction:column}.katex .hbox{width:100%}.katex .hbox,.katex .thinbox{display:inline-flex;flex-direction:row}.katex .thinbox{max-width:0;width:0}.katex .msupsub{text-align:left}.katex .mfrac>span>span{text-align:center}.katex .mfrac .frac-line{border-bottom-style:solid;display:inline-block;width:100%}.katex .hdashline,.katex .hline,.katex .mfrac .frac-line,.katex .overline .overline-line,.katex .rule,.katex .underline .underline-line{min-height:1px}.katex .mspace{display:inline-block}.katex .clap,.katex .llap,.katex .rlap{position:relative;width:0}.katex .clap>.inner,.katex .llap>.inner,.katex .rlap>.inner{position:absolute}.katex .clap>.fix,.katex .llap>.fix,.katex .rlap>.fix{display:inline-block}.katex .llap>.inner{right:0}.katex .clap>.inner,.katex .rlap>.inner{left:0}.katex .clap>.inner>span{margin-left:-50%;margin-right:50%}.katex .rule{border:0 solid;display:inline-block;position:relative}.katex .hline,.katex .overline .overline-line,.katex .underline .underline-line{border-bottom-style:solid;display:inline-block;width:100%}.katex .hdashline{border-bottom-style:dashed;display:inline-block;width:100%}.katex .sqrt>.root{margin-left:.27777778em;margin-right:-.55555556em}.katex .fontsize-ensurer.reset-size1.size1,.katex .sizing.reset-size1.size1{font-size:1em}.katex .fontsize-ensurer.reset-size1.size2,.katex .sizing.reset-size1.size2{font-size:1.2em}.katex .fontsize-ensurer.reset-size1.size3,.katex .sizing.reset-size1.size3{font-size:1.4em}.katex .fontsize-ensurer.reset-size1.size4,.katex .sizing.reset-size1.size4{font-size:1.6em}.katex .fontsize-ensurer.reset-size1.size5,.katex .sizing.reset-size1.size5{font-size:1.8em}.katex .fontsize-ensurer.reset-size1.size6,.katex .sizing.reset-size1.size6{font-size:2em}.katex .fontsize-ensurer.reset-size1.size7,.katex .sizing.reset-size1.size7{font-size:2.4em}.katex .fontsize-ensurer.reset-size1.size8,.katex .sizing.reset-size1.size8{font-size:2.88em}.katex .fontsize-ensurer.reset-size1.size9,.katex .sizing.reset-size1.size9{font-size:3.456em}.katex .fontsize-ensurer.reset-size1.size10,.katex .sizing.reset-size1.size10{font-size:4.148em}.katex .fontsize-ensurer.reset-size1.size11,.katex .sizing.reset-size1.size11{font-size:4.976em}.katex .fontsize-ensurer.reset-size2.size1,.katex .sizing.reset-size2.size1{font-size:.83333333em}.katex .fontsize-ensurer.reset-size2.size2,.katex .sizing.reset-size2.size2{font-size:1em}.katex .fontsize-ensurer.reset-size2.size3,.katex .sizing.reset-size2.size3{font-size:1.16666667em}.katex .fontsize-ensurer.reset-size2.size4,.katex .sizing.reset-size2.size4{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size2.size5,.katex .sizing.reset-size2.size5{font-size:1.5em}.katex .fontsize-ensurer.reset-size2.size6,.katex .sizing.reset-size2.size6{font-size:1.66666667em}.katex .fontsize-ensurer.reset-size2.size7,.katex .sizing.reset-size2.size7{font-size:2em}.katex .fontsize-ensurer.reset-size2.size8,.katex .sizing.reset-size2.size8{font-size:2.4em}.katex .fontsize-ensurer.reset-size2.size9,.katex .sizing.reset-size2.size9{font-size:2.88em}.katex .fontsize-ensurer.reset-size2.size10,.katex .sizing.reset-size2.size10{font-size:3.45666667em}.katex .fontsize-ensurer.reset-size2.size11,.katex .sizing.reset-size2.size11{font-size:4.14666667em}.katex .fontsize-ensurer.reset-size3.size1,.katex .sizing.reset-size3.size1{font-size:.71428571em}.katex .fontsize-ensurer.reset-size3.size2,.katex .sizing.reset-size3.size2{font-size:.85714286em}.katex .fontsize-ensurer.reset-size3.size3,.katex .sizing.reset-size3.size3{font-size:1em}.katex .fontsize-ensurer.reset-size3.size4,.katex .sizing.reset-size3.size4{font-size:1.14285714em}.katex .fontsize-ensurer.reset-size3.size5,.katex .sizing.reset-size3.size5{font-size:1.28571429em}.katex .fontsize-ensurer.reset-size3.size6,.katex .sizing.reset-size3.size6{font-size:1.42857143em}.katex .fontsize-ensurer.reset-size3.size7,.katex .sizing.reset-size3.size7{font-size:1.71428571em}.katex .fontsize-ensurer.reset-size3.size8,.katex .sizing.reset-size3.size8{font-size:2.05714286em}.katex .fontsize-ensurer.reset-size3.size9,.katex .sizing.reset-size3.size9{font-size:2.46857143em}.katex .fontsize-ensurer.reset-size3.size10,.katex .sizing.reset-size3.size10{font-size:2.96285714em}.katex .fontsize-ensurer.reset-size3.size11,.katex .sizing.reset-size3.size11{font-size:3.55428571em}.katex .fontsize-ensurer.reset-size4.size1,.katex .sizing.reset-size4.size1{font-size:.625em}.katex .fontsize-ensurer.reset-size4.size2,.katex .sizing.reset-size4.size2{font-size:.75em}.katex .fontsize-ensurer.reset-size4.size3,.katex .sizing.reset-size4.size3{font-size:.875em}.katex .fontsize-ensurer.reset-size4.size4,.katex .sizing.reset-size4.size4{font-size:1em}.katex .fontsize-ensurer.reset-size4.size5,.katex .sizing.reset-size4.size5{font-size:1.125em}.katex .fontsize-ensurer.reset-size4.size6,.katex .sizing.reset-size4.size6{font-size:1.25em}.katex .fontsize-ensurer.reset-size4.size7,.katex .sizing.reset-size4.size7{font-size:1.5em}.katex .fontsize-ensurer.reset-size4.size8,.katex .sizing.reset-size4.size8{font-size:1.8em}.katex .fontsize-ensurer.reset-size4.size9,.katex .sizing.reset-size4.size9{font-size:2.16em}.katex .fontsize-ensurer.reset-size4.size10,.katex .sizing.reset-size4.size10{font-size:2.5925em}.katex .fontsize-ensurer.reset-size4.size11,.katex .sizing.reset-size4.size11{font-size:3.11em}.katex .fontsize-ensurer.reset-size5.size1,.katex .sizing.reset-size5.size1{font-size:.55555556em}.katex .fontsize-ensurer.reset-size5.size2,.katex .sizing.reset-size5.size2{font-size:.66666667em}.katex .fontsize-ensurer.reset-size5.size3,.katex .sizing.reset-size5.size3{font-size:.77777778em}.katex .fontsize-ensurer.reset-size5.size4,.katex .sizing.reset-size5.size4{font-size:.88888889em}.katex .fontsize-ensurer.reset-size5.size5,.katex .sizing.reset-size5.size5{font-size:1em}.katex .fontsize-ensurer.reset-size5.size6,.katex .sizing.reset-size5.size6{font-size:1.11111111em}.katex .fontsize-ensurer.reset-size5.size7,.katex .sizing.reset-size5.size7{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size5.size8,.katex .sizing.reset-size5.size8{font-size:1.6em}.katex .fontsize-ensurer.reset-size5.size9,.katex .sizing.reset-size5.size9{font-size:1.92em}.katex .fontsize-ensurer.reset-size5.size10,.katex .sizing.reset-size5.size10{font-size:2.30444444em}.katex .fontsize-ensurer.reset-size5.size11,.katex .sizing.reset-size5.size11{font-size:2.76444444em}.katex .fontsize-ensurer.reset-size6.size1,.katex .sizing.reset-size6.size1{font-size:.5em}.katex .fontsize-ensurer.reset-size6.size2,.katex .sizing.reset-size6.size2{font-size:.6em}.katex .fontsize-ensurer.reset-size6.size3,.katex .sizing.reset-size6.size3{font-size:.7em}.katex .fontsize-ensurer.reset-size6.size4,.katex .sizing.reset-size6.size4{font-size:.8em}.katex .fontsize-ensurer.reset-size6.size5,.katex .sizing.reset-size6.size5{font-size:.9em}.katex .fontsize-ensurer.reset-size6.size6,.katex .sizing.reset-size6.size6{font-size:1em}.katex .fontsize-ensurer.reset-size6.size7,.katex .sizing.reset-size6.size7{font-size:1.2em}.katex .fontsize-ensurer.reset-size6.size8,.katex .sizing.reset-size6.size8{font-size:1.44em}.katex .fontsize-ensurer.reset-size6.size9,.katex .sizing.reset-size6.size9{font-size:1.728em}.katex .fontsize-ensurer.reset-size6.size10,.katex .sizing.reset-size6.size10{font-size:2.074em}.katex .fontsize-ensurer.reset-size6.size11,.katex .sizing.reset-size6.size11{font-size:2.488em}.katex .fontsize-ensurer.reset-size7.size1,.katex .sizing.reset-size7.size1{font-size:.41666667em}.katex .fontsize-ensurer.reset-size7.size2,.katex .sizing.reset-size7.size2{font-size:.5em}.katex .fontsize-ensurer.reset-size7.size3,.katex .sizing.reset-size7.size3{font-size:.58333333em}.katex .fontsize-ensurer.reset-size7.size4,.katex .sizing.reset-size7.size4{font-size:.66666667em}.katex .fontsize-ensurer.reset-size7.size5,.katex .sizing.reset-size7.size5{font-size:.75em}.katex .fontsize-ensurer.reset-size7.size6,.katex .sizing.reset-size7.size6{font-size:.83333333em}.katex .fontsize-ensurer.reset-size7.size7,.katex .sizing.reset-size7.size7{font-size:1em}.katex .fontsize-ensurer.reset-size7.size8,.katex .sizing.reset-size7.size8{font-size:1.2em}.katex .fontsize-ensurer.reset-size7.size9,.katex .sizing.reset-size7.size9{font-size:1.44em}.katex .fontsize-ensurer.reset-size7.size10,.katex .sizing.reset-size7.size10{font-size:1.72833333em}.katex .fontsize-ensurer.reset-size7.size11,.katex .sizing.reset-size7.size11{font-size:2.07333333em}.katex .fontsize-ensurer.reset-size8.size1,.katex .sizing.reset-size8.size1{font-size:.34722222em}.katex .fontsize-ensurer.reset-size8.size2,.katex .sizing.reset-size8.size2{font-size:.41666667em}.katex .fontsize-ensurer.reset-size8.size3,.katex .sizing.reset-size8.size3{font-size:.48611111em}.katex .fontsize-ensurer.reset-size8.size4,.katex .sizing.reset-size8.size4{font-size:.55555556em}.katex .fontsize-ensurer.reset-size8.size5,.katex .sizing.reset-size8.size5{font-size:.625em}.katex .fontsize-ensurer.reset-size8.size6,.katex .sizing.reset-size8.size6{font-size:.69444444em}.katex .fontsize-ensurer.reset-size8.size7,.katex .sizing.reset-size8.size7{font-size:.83333333em}.katex .fontsize-ensurer.reset-size8.size8,.katex .sizing.reset-size8.size8{font-size:1em}.katex .fontsize-ensurer.reset-size8.size9,.katex .sizing.reset-size8.size9{font-size:1.2em}.katex .fontsize-ensurer.reset-size8.size10,.katex .sizing.reset-size8.size10{font-size:1.44027778em}.katex .fontsize-ensurer.reset-size8.size11,.katex .sizing.reset-size8.size11{font-size:1.72777778em}.katex .fontsize-ensurer.reset-size9.size1,.katex .sizing.reset-size9.size1{font-size:.28935185em}.katex .fontsize-ensurer.reset-size9.size2,.katex .sizing.reset-size9.size2{font-size:.34722222em}.katex .fontsize-ensurer.reset-size9.size3,.katex .sizing.reset-size9.size3{font-size:.40509259em}.katex .fontsize-ensurer.reset-size9.size4,.katex .sizing.reset-size9.size4{font-size:.46296296em}.katex .fontsize-ensurer.reset-size9.size5,.katex .sizing.reset-size9.size5{font-size:.52083333em}.katex .fontsize-ensurer.reset-size9.size6,.katex .sizing.reset-size9.size6{font-size:.5787037em}.katex .fontsize-ensurer.reset-size9.size7,.katex .sizing.reset-size9.size7{font-size:.69444444em}.katex .fontsize-ensurer.reset-size9.size8,.katex .sizing.reset-size9.size8{font-size:.83333333em}.katex .fontsize-ensurer.reset-size9.size9,.katex .sizing.reset-size9.size9{font-size:1em}.katex .fontsize-ensurer.reset-size9.size10,.katex .sizing.reset-size9.size10{font-size:1.20023148em}.katex .fontsize-ensurer.reset-size9.size11,.katex .sizing.reset-size9.size11{font-size:1.43981481em}.katex .fontsize-ensurer.reset-size10.size1,.katex .sizing.reset-size10.size1{font-size:.24108004em}.katex .fontsize-ensurer.reset-size10.size2,.katex .sizing.reset-size10.size2{font-size:.28929605em}.katex .fontsize-ensurer.reset-size10.size3,.katex .sizing.reset-size10.size3{font-size:.33751205em}.katex .fontsize-ensurer.reset-size10.size4,.katex .sizing.reset-size10.size4{font-size:.38572806em}.katex .fontsize-ensurer.reset-size10.size5,.katex .sizing.reset-size10.size5{font-size:.43394407em}.katex .fontsize-ensurer.reset-size10.size6,.katex .sizing.reset-size10.size6{font-size:.48216008em}.katex .fontsize-ensurer.reset-size10.size7,.katex .sizing.reset-size10.size7{font-size:.57859209em}.katex .fontsize-ensurer.reset-size10.size8,.katex .sizing.reset-size10.size8{font-size:.69431051em}.katex .fontsize-ensurer.reset-size10.size9,.katex .sizing.reset-size10.size9{font-size:.83317261em}.katex .fontsize-ensurer.reset-size10.size10,.katex .sizing.reset-size10.size10{font-size:1em}.katex .fontsize-ensurer.reset-size10.size11,.katex .sizing.reset-size10.size11{font-size:1.19961427em}.katex .fontsize-ensurer.reset-size11.size1,.katex .sizing.reset-size11.size1{font-size:.20096463em}.katex .fontsize-ensurer.reset-size11.size2,.katex .sizing.reset-size11.size2{font-size:.24115756em}.katex .fontsize-ensurer.reset-size11.size3,.katex .sizing.reset-size11.size3{font-size:.28135048em}.katex .fontsize-ensurer.reset-size11.size4,.katex .sizing.reset-size11.size4{font-size:.32154341em}.katex .fontsize-ensurer.reset-size11.size5,.katex .sizing.reset-size11.size5{font-size:.36173633em}.katex .fontsize-ensurer.reset-size11.size6,.katex .sizing.reset-size11.size6{font-size:.40192926em}.katex .fontsize-ensurer.reset-size11.size7,.katex .sizing.reset-size11.size7{font-size:.48231511em}.katex .fontsize-ensurer.reset-size11.size8,.katex .sizing.reset-size11.size8{font-size:.57877814em}.katex .fontsize-ensurer.reset-size11.size9,.katex .sizing.reset-size11.size9{font-size:.69453376em}.katex .fontsize-ensurer.reset-size11.size10,.katex .sizing.reset-size11.size10{font-size:.83360129em}.katex .fontsize-ensurer.reset-size11.size11,.katex .sizing.reset-size11.size11{font-size:1em}.katex .delimsizing.size1{font-family:KaTeX_Size1}.katex .delimsizing.size2{font-family:KaTeX_Size2}.katex .delimsizing.size3{font-family:KaTeX_Size3}.katex .delimsizing.size4{font-family:KaTeX_Size4}.katex .delimsizing.mult .delim-size1>span{font-family:KaTeX_Size1}.katex .delimsizing.mult .delim-size4>span{font-family:KaTeX_Size4}.katex .nulldelimiter{display:inline-block;width:.12em}.katex .delimcenter,.katex .op-symbol{position:relative}.katex .op-symbol.small-op{font-family:KaTeX_Size1}.katex .op-symbol.large-op{font-family:KaTeX_Size2}.katex .accent>.vlist-t,.katex .op-limits>.vlist-t{text-align:center}.katex .accent .accent-body{position:relative}.katex .accent .accent-body:not(.accent-full){width:0}.katex .overlay{display:block}.katex .mtable .vertical-separator{display:inline-block;min-width:1px}.katex .mtable .arraycolsep{display:inline-block}.katex .mtable .col-align-c>.vlist-t{text-align:center}.katex .mtable .col-align-l>.vlist-t{text-align:left}.katex .mtable .col-align-r>.vlist-t{text-align:right}.katex .svg-align{text-align:left}.katex svg{fill:currentColor;stroke:currentColor;fill-rule:nonzero;fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;display:block;height:inherit;position:absolute;width:100%}.katex svg path{stroke:none}.katex img{border-style:none;max-height:none;max-width:none;min-height:0;min-width:0}.katex .stretchy{display:block;overflow:hidden;position:relative;width:100%}.katex .stretchy:after,.katex .stretchy:before{content:""}.katex .hide-tail{overflow:hidden;position:relative;width:100%}.katex .halfarrow-left{left:0;overflow:hidden;position:absolute;width:50.2%}.katex .halfarrow-right{overflow:hidden;position:absolute;right:0;width:50.2%}.katex .brace-left{left:0;overflow:hidden;position:absolute;width:25.1%}.katex .brace-center{left:25%;overflow:hidden;position:absolute;width:50%}.katex .brace-right{overflow:hidden;position:absolute;right:0;width:25.1%}.katex .x-arrow-pad{padding:0 .5em}.katex .cd-arrow-pad{padding:0 .55556em 0 .27778em}.katex .mover,.katex .munder,.katex .x-arrow{text-align:center}.katex .boxpad{padding:0 .3em}.katex .fbox,.katex .fcolorbox{border:.04em solid;box-sizing:border-box}.katex .cancel-pad{padding:0 .2em}.katex .cancel-lap{margin-left:-.2em;margin-right:-.2em}.katex .sout{border-bottom-style:solid;border-bottom-width:.08em}.katex .angl{border-right:.049em solid;border-top:.049em solid;box-sizing:border-box;margin-right:.03889em}.katex .anglpad{padding:0 .03889em}.katex .eqn-num:before{content:"(" counter(katexEqnNo) ")";counter-increment:katexEqnNo}.katex .mml-eqn-num:before{content:"(" counter(mmlEqnNo) ")";counter-increment:mmlEqnNo}.katex .mtr-glue{width:50%}.katex .cd-vert-arrow{display:inline-block;position:relative}.katex .cd-label-left{display:inline-block;position:absolute;right:calc(50% + .3em);text-align:left}.katex .cd-label-right{display:inline-block;left:calc(50% + .3em);position:absolute;text-align:right}.katex-display{display:block;margin:1em 0;text-align:center}.katex-display>.katex{display:block;text-align:center;white-space:nowrap}.katex-display>.katex>.katex-html{display:block;position:relative}.katex-display>.katex>.katex-html>.tag{position:absolute;right:0}.katex-display.leqno>.katex>.katex-html>.tag{left:0;right:auto}.katex-display.fleqn>.katex{padding-left:2em;text-align:left}body{counter-reset:katexEqnNo mmlEqnNo}
/*---------------------------------------------------------------------------------------------
* Copyright (c) Microsoft Corporation. All rights reserved.
* Licensed under the MIT License. See License.txt in the project root for license information.
*--------------------------------------------------------------------------------------------*/
.katex-error {
color: var(--vscode-editorError-foreground);
}
/* From extension ms-toolsai.jupyter */
/* These classnames are inherited from bootstrap, but are present in most notebook renderers */
.alert {
width: auto;
padding: 1em;
margin-top: 1em;
margin-bottom: 1em;
}
.alert > *:last-child {
margin-bottom: 0;
}
#preview > .alert:last-child {
/* Prevent this being set to zero by the default notebook stylesheet */
padding-bottom: 1em;
}
.alert-success {
/* Note there is no suitable color available, so we just copy "info" */
background-color: var(--theme-info-background);
color: var(--theme-info-foreground);
}
.alert-info {
background-color: var(--theme-info-background);
color: var(--theme-info-foreground);
}
.alert-warning {
background-color: var(--theme-warning-background);
color: var(--theme-warning-foreground);
}
.alert-danger {
background-color: var(--theme-error-background);
color: var(--theme-error-foreground);
}
</style>
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.10.2/dist/katex.min.css" integrity="sha384-yFRtMMDnQtDRO8rLpMIKrtPCD5jdktao2TV19YiZYWMDkUR5GQZR/NOVTdquEx1j" crossorigin="anonymous">
<link href="https://cdn.jsdelivr.net/npm/katex-copytex@latest/dist/katex-copytex.min.css" rel="stylesheet" type="text/css">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/gh/Microsoft/vscode/extensions/markdown-language-features/media/markdown.css">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/gh/Microsoft/vscode/extensions/markdown-language-features/media/highlight.css">
<style>
body {
font-family: -apple-system, BlinkMacSystemFont, 'Segoe WPC', 'Segoe UI', system-ui, 'Ubuntu', 'Droid Sans', sans-serif;
font-size: 14px;
line-height: 1.6;
}
</style>
<style>
.task-list-item { list-style-type: none; } .task-list-item-checkbox { margin-left: -20px; vertical-align: middle; }
</style>
</head>
<body class="vscode-body vscode-light">
<h1 id="fastbatllnn-fast-box-analysis-of-two-level-lattice-neural-networks">FastBATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks</h1>
<p>FastBATLLNN is a fast verifier of box-like (hyper-rectangle) output properties for Two-Level Lattice (TLL) Neural Networks (NN). In particular, FastBATLLNN can formally verify whether the output of a TLL NN is confined to a specified hyper-rectangle whenever its inputs are confined to a specified closed, convex polytope.</p>
<p>This work appeared in <a href="https://hscc.acm.org/2022/">HSCC 2022</a>. Please refer to/cite the following publication:</p>
<blockquote>
<p><em>Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks.</em><br>
James Ferlez, Haitham Khedr and Yasser Shoukry. HSCC '22: 25th ACM International Conference on Hybrid Systems: Computation and Control, May 2022. Article No.: 23. Pages 1–11. <a href="https://doi.org/10.1145/3501710.3519533">https://doi.org/10.1145/3501710.3519533</a></p>
</blockquote>
<p><em>Please contact <a href="mailto:jferlez@uci.edu">jferlez@uci.edu</a> with any questions/bug reports.</em></p>
<h2 id="1-prerequisites">1) Prerequisites</h2>
<p>FastBATLLNN is written in Python, and it depends on the following packages/libraries (and their dependencies):</p>
<ul>
<li><a href="https://charm4py.readthedocs.io/en/latest/">charm4py</a> (Python/Library)</li>
<li><a href="https://www.gnu.org/software/glpk/">glpk</a> (Library)</li>
<li><a href="https://github.com/coin-or/CyLP">cylp</a> (Python) / <a href="https://github.com/coin-or/Clp">Clp</a> (Library)</li>
<li><a href="https://cvxopt.org">cvxopt</a> (Python)</li>
<li><a href="https://numba.pydata.org">numba</a> (Python)</li>
<li><a href="https://pycddlib.readthedocs.io/en/latest/">pycddlib</a> (Python/Library)</li>
</ul>
<p>These dependencies can be burdensome to install, so we have provided facilities for running FastBATLLNN in a <a href="https://docker.com">Docker</a> container.</p>
<blockquote>
<p><strong>NOTE: A Docker container is the preferred means of running FastBATLLNN; the rest of this document assumes this run environment.</strong></p>
</blockquote>
<h3 id="docker-prerequisites">(Docker) Prerequisites:</h3>
<ol>
<li>An x86_64 Linux, MacOS or Windows host</li>
<li>A recent version of <a href="https://docker.com">Docker</a> (Windows hosts only tested with the <a href="https://docs.docker.com/desktop/install/windows-install/">WSL2 backend</a>)</li>
<li>Approximately 25Gb of free disk space; however, the final Docker image only requires ~13Gb (MacOS users should allocate >=30Gb to the Docker VM to be safe)</li>
<li>The ability to run a Docker container with the <a href="https://docs.docker.com/engine/reference/run/#runtime-privilege-and-linux-capabilities"><code>--priviledged</code> switch</a>.</li>
</ol>
<h2 id="2-quick-start">2) Quick Start</h2>
<p>Exectute the following in a Bash shell on the host (a WSL2 Bash shell on Windows):</p>
<pre><code class="language-Bash"><div>LOCATION=/path/to/someplace/convenient
<span class="hljs-built_in">cd</span> <span class="hljs-string">"<span class="hljs-variable">$LOCATION</span>"</span>
git <span class="hljs-built_in">clone</span> --recursive https://github.com/jferlez/FastBATLLNN <span class="hljs-comment"># --recurisve is optional if using Docker</span>
<span class="hljs-built_in">cd</span> FastBATLLNN
./dockerbuild.sh <span class="hljs-comment"># Warning: may take > 1 hour!</span>
./dockerrun.sh --interactive
</div></code></pre>
<p>This should place you at a Bash shell inside a container with FastBATLLNN installed. If these scripts execute successfully, then you can skip to <strong>4) Running FastBATLLNN</strong>.</p>
<blockquote>
<p><strong>WARNING:</strong> if you exit the container's Bash shell, then the container will stop. See Section <strong>3)</strong> for information about how to restart the container, and regain access.</p>
</blockquote>
<blockquote>
<p><strong>NOTE:</strong> The Docker images/container have a number of features that are documented in Section <strong>3)</strong>. <strong>I ADVISE YOU NOT TO SKIP THAT SECTION!</strong></p>
</blockquote>
<h2 id="3-creating-the-docker-imagescontainer">3) Creating the Docker Images/Container</h2>
<h3 id="i-creating-the-docker-images">(i) Creating the Docker Images</h3>
<p>The first step is to obtain the FastBATLLNN code by cloning this Git repository:</p>
<pre><code class="language-Bash"><div>LOCATION=/path/to/someplace/convenient
<span class="hljs-built_in">cd</span> <span class="hljs-string">"<span class="hljs-variable">$LOCATION</span>"</span>
git <span class="hljs-built_in">clone</span> --recursive https://github.com/jferlez/FastBATLLNN <span class="hljs-comment"># --recurisve is optional if using Docker</span>
</div></code></pre>
<blockquote>
<p><strong>NOTE:</strong> <code>$LOCATION</code> will refer to the FastBATLLNN install location henceforth.</p>
</blockquote>
<p>Now, FastBATLLNN comes with the Bash script <code>dockerbuild.sh</code>, which should automatically build all of the necessary Docker images:</p>
<pre><code class="language-Bash"><div><span class="hljs-built_in">cd</span> FastBATLLNN
./dockerbuild.sh
</div></code></pre>
<blockquote>
<p><strong>WARNING:</strong> The first run of <code>dockerbuild.sh</code> may take <strong>AN HOUR OR MORE</strong> to download and compile all of the dependencies.</p>
</blockquote>
<p><code>dockerbuild.sh</code> should create two docker images that appear in the output of <code>docker image ls</code> as follows:</p>
<pre><code>REPOSITORY TAG IMAGE ID CREATED SIZE
fastbatllnn-run USER 123456789abc 31 minutes ago 12.5GB
fastbatllnn-deps local def123456789 32 minutes ago 12.5GB
</code></pre>
<p>Where <code>USER</code> is the <strong>host</strong> log-in name of the user who ran <code>dockerbuild.sh</code>; it will be automatically detected by <code>dockerbuild.sh</code>.</p>
<blockquote>
<p><strong>NOTE:</strong> Henceforth <code>USER</code> will refer to the login name of the current host user.</p>
</blockquote>
<p>These images are described as follows:</p>
<ol>
<li><code>fastbatllnn-deps:local</code> contains all of the runtime dependencies of FastBATLLNN; it is a separate image to facilitate re-use (originally I intended to host this image on DockerHub, but decided against it due to licensing issues.)</li>
<li><code>fastbatllnn-run:USER</code> is the image that adds the FastBATLLNN code by cloning this repository; it is the one that will ultimately be run in a container. <strong>It is configured to have a user with same user name, user id and group id as the creating host user</strong> (placeholder <code>USER</code>).</li>
</ol>
<blockquote>
<p><strong>WARNING:</strong> <code>fastbatllnn-run:USER</code> is derived from <code>fastbatllnn-deps:local</code> with a <code>FROM</code> directive in its <code>Dockerfile</code>. Thus, <strong>DO NOT DELETE <code>fastbatllnn-deps:local</code></strong>! Because of the way Docker works, its contents are not duplicated in <code>fastbatllnn-run:USER</code> anyway.</p>
</blockquote>
<blockquote>
<p><strong>NOTE:</strong> A subsequent call to <code>dockerbuild.sh</code> will use the <strong>cached</strong> version of <code>fastbatllnn-deps:local</code> but will <strong>rebuild</strong> <code>fastbatllnn-run:USER</code> from scratch -- <em>i.e., re-clone this repository</em>; <code>fastbatllnn-deps:local</code> is the only image that requires significant time to create.</p>
</blockquote>
<h3 id="ii-running-a-docker-container">(ii) Running a Docker Container</h3>
<p>Once a user has created the above Docker images (only <code>fastbatllnn-run:USER</code> is user specific), a suitable container can be started using the command:</p>
<pre><code class="language-Bash"><div>./dockerrun.sh [--interactive]
</div></code></pre>
<p>Where the <code>--interactive</code> flag is optional. <code>dockerrun.sh</code> infers the current host user name (placeholder <code>USER</code>), and launches a relevant container in one of two ways:</p>
<ol>
<li>If <em>there <strong>EXISTS NO</strong> container</em> derived from <code>fastbatllnn-run:USER</code>, then <code>dockerrun.sh</code> starts a new container from that image, using the appropriate options; or</li>
<li>If <em>there <strong>EXISTS</strong> a container</em> derived from <code>fastbatllnn-run:USER</code>, then <code>dockerrun.sh</code> simply attempts to (re-)start that container.</li>
</ol>
<p>This should allow you to stop a container (say by restarting your computer), without having to figure out which container to restart.</p>
<p>You can interact with the resultant container in three ways:</p>
<ol>
<li>If the container is started by the command <code>dockerrun.sh --interactive</code>, you will be placed in a Bash shell in the container (i.e. option <code>-it</code> for <a href="https://docs.docker.com/engine/reference/run/"><code>docker run</code></a>); otherwise, the container will operate in daemon mode;</li>
<li>The container <strong>always</strong> starts an SSH daemon listening on <em>localhost</em>, port 3000; it also attempts to copy the current user's <strong>public</strong> ssh keys for password-less login (i.e. it adds these keys to <code>./ssh/authorized_keys</code> in the container);</li>
<li>The host directory <code>$LOCATION/container_results</code> is bind-mounted to <code>/home/USER/results</code> in the container (the host directory will be created if it doesn't exist).</li>
</ol>
<blockquote>
<p><strong>WARNING:</strong> if you exit the container's Bash shell, then the container will stop. Restarting the container with <code>dockerrun.sh</code> (see above) will not return you to a Bash shell, but it will restart the SSH daemon: you will have to interact with the restarted container via SSH.</p>
</blockquote>
<blockquote>
<p><strong>NOTE:</strong> You can specify that the container should listen on a different port by calling <code>dockerrun.sh</code> with the option <code>--ssh-port=1234</code> where <code>1234</code> can be replaced with a valid port for the container to listen on. That is, by default, <code>dockerrun.sh</code> infers <code>--ssh-port=3000</code>.</p>
</blockquote>
<p>SSH is the best way to run code in the container:</p>
<ul>
<li>It allows the container to run in the background without occupying a terminal on the host;</li>
<li>It allows SFTP to be used to transfer files to/from the container; and</li>
<li>(Most importantly) It allows the use of <a href="https://code.visualstudio.com">VS Code</a> to edit/run code directly in the container via its <a href="https://code.visualstudio.com/docs/remote/ssh">Remote-SSH</a> functionality.</li>
</ul>
<p>If you see either of the following lines output by <code>dockerrun.sh</code>:</p>
<pre><code>Copying public key from ~/.ssh/id_rsa.pub to container authorized_keys
Copying public keys from ~/.ssh/authorized_keys to container authorized_keys
</code></pre>
<p>then you can log-in to the container as <code>USER</code> (i.e. the current host user) from the host or any computers that can log-in <em>to the host computer</em>, respectively.</p>
<p>That is you should be able to log-in to the container with the following command:</p>
<pre><code class="language-Bash"><div>ssh -p 3000 USER@localhost
</div></code></pre>
<p>with no password required. If the log-in is successful, you will be asked to accept the host key of the container using a prompt like:</p>
<pre><code>The authenticity of host '[localhost]:3000 ([127.0.0.1]:3000)' can't be established.
ECDSA key fingerprint is SHA256:qwertyuiopasdfghjkl.
Are you sure you want to continue connecting (yes/no/[fingerprint])?
</code></pre>
<p>This host key is automatically placed in <code>$LOCATION/container_results/ssh_host_rsa_key.pub</code> so you can verify that you are confirming the correct one.</p>
<blockquote>
<p><strong>WARNING:</strong> if at any time in the past you logged in to the host via <code>localhost</code>, then you will be warned about a potential man-in-the-middle attack. In this case, simply disconnect, and remove or comment out the <strong>host's</strong> public key from <code>~/.ssh/known_hosts</code> <em>on the host</em>, and try reconnecting.</p>
</blockquote>
<blockquote>
<p><strong>WARNING:</strong> for security reasons, password log-in to the container is disabled. So you must have keys in either <code>~/.ssh/id_rsa.pub</code> (to log-in to the container <em>from the host</em>) or <code>~/.ssh/authorized_keys</code> (to log-in to the container from a computer that can log-in <em>to</em> the host).</p>
</blockquote>
<blockquote>
<p><strong>NOTE:</strong> The container is configured with a user that has the same user name, user id and group id as the creating user on the host (<code>USER</code> placeholder). The password for that user is just the user name, should <code>sudo</code> be required in the container (i.e. <code>USER</code> for our placeholder).</p>
</blockquote>
<blockquote>
<p><strong>NOTE:</strong> The container has <a href="https://github.com/tmux/tmux/wiki"><code>tmux</code></a> and <a href="https://www.gnu.org/software/screen/"><code>screen</code></a> pre-installed to facilitate running tasks that persist after disconnecting an SSH session.</p>
</blockquote>
<h2 id="4-running-fastbatllnn">4) Running FastBATLLNN</h2>
<p>This section assumes that you have successfully reached a prompt inside a <code>fastbatllnn-run:USER</code> container. For example:</p>
<pre><code class="language-Bash"><div>USER@0123456789ab:~$
</div></code></pre>
<p>where <code>0123456789ab</code> is the container id for a <code>fastbatllnn-run:USER</code> derived container. Please go back to Section <strong>3)</strong> if this is not the case.</p>
<p>FastBATLLNN is already configured to run inside the container, and there is a simple example to make sure everything is working. To test this, execute the following in the container (i.e. at the prompt above):</p>
<pre><code class="language-Bash"><div><span class="hljs-built_in">cd</span> ~/tools/FastBATLLNN
<span class="hljs-built_in">export</span> CORES=1
charmrun +p<span class="hljs-variable">$CORES</span> example.py
</div></code></pre>
<p>The shell variable <code>CORES</code> can be changed to any integer up to the number of <em>physical</em> CPU cores on your system (e.g. for a CPU with 4 cores and 8 threads, <code>CORES=4</code> is the largest permissible value).</p>
<p>This command should produce the following output (abbreviated here):</p>
<pre><code>Running as 4 OS processes: /usr/bin/python3.9 example.py
charmrun> /usr/bin/setarch x86_64 -R mpirun -np 4 /usr/bin/python3.9 example.py
Charm++> Running on MPI library: Open MPI v4.0.3, package: Debian OpenMPI, ident: 4.0.3, repo rev: v4.0.3, Mar 03, 2020 (MPI standard: 3.1)
Charm++> Level of thread support used: -1 (desired: 0)
Charm++> Running in non-SMP mode: 4 processes (PEs)
Converse/Charm++ Commit ID: v7.1.0-devel-154-g4fd8c4b81
Isomalloc> Synchronized global address space.
CharmLB> Load balancer assumes all CPUs are same.
Charm4py> Running Charm4py version 1.0 on Python 3.9.5 (CPython). Using 'cython' interface to access Charm++
Charm++> Running on 1 hosts (2 sockets x 12 cores x 2 PUs = 48-way SMP)
Charm++> cpu topology info is gathered in 0.000 seconds.
CharmLB> Load balancing instrumentation for communication is off.
2022-05-07 20:21:50.290119: W tensorflow/stream_executor/platform/default/dso_loader.cc:64] Could not load dynamic library 'libcuda.so.1'; dlerror: libcuda.so.1: cannot open shared object file: No such file or directory; LD_LIBRARY_PATH: /usr/local/lib
2022-05-07 20:21:50.290181: W tensorflow/stream_executor/cuda/cuda_driver.cc:269] failed call to cuInit: UNKNOWN ERROR (303)
Max of Output Samples: 4.524217171074326
Min of Output Samples: 0.43370844553525956
----------------- VERIFYING LOWER BOUND: -----------------
Total LPs used: defaultdict(<class 'int'>, {'LPSolverCount': 35, 'xferTime': 0.001024484634399414})
Checker returned value: True
Computed a (partial) poset of size: 5
TLL always >= 0.299 on constraints? True
-----------------------------------------------------------
----------------- VERIFYING UPPER BOUND: -----------------
Upper Bound verifiction used 8 total LPs.
TLL always <= 4.51 on constraints? False
-----------------------------------------------------------
--------------- FINDING TIGHT LOWER BOUND: ---------------
Total LPs used: defaultdict(<class 'int'>, {'LPSolverCount': 35, 'xferTime': 0.0008916854858398438})
Checker returned value: True
Computed a (partial) poset of size: 5
Iteration 100: -0.135 is a VALID lower bound!
Total LPs used: defaultdict(<class 'int'>, {'LPSolverCount': 28, 'xferTime': 0.0009856224060058594})
Checker returned value: False
Computed a (partial) poset of size: 4
.
.
.
Checker returned value: True
Computed a (partial) poset of size: 5
Iteration 89: 0.2995703125 is a VALID lower bound!
********** verifyLB on LB processing times: **********
Total time required to initialize the new lb problem: 0.010710716247558594
Total time required for region check workers to initialize: 0
Total time required for (partial) poset calculation: 0.21567153930664062
Iterations used: 11
***********************************************************
------------------ FOUND LOWER BOUND: -------------------
0.2995703125
Total time elapsed: 0.20470857620239258 (sec)
Minimum of samples: 0.43370844553525956
-----------------------------------------------------------
--------------- FINDING TIGHT UPPER BOUND: ---------------
Upper Bound verifiction used 12 total LPs.
Iteration 100: -135 is a VALID lower bound!
.
.
.
Upper Bound verifiction used 176 total LPs.
Iteration 76: 4.538595911107734 is an INVALID lower bound!
********** verifyUB on UB processing times: **********
Iterations used: 24
Total number of LPs used for Upper Bound verification: 176
***********************************************************
------------------ FOUND UPPER BOUND: -------------------
4.538595911107734
Total time elapsed: 0.022965192794799805 (sec)
Maximum of samples: 4.524217171074326
-----------------------------------------------------------
</code></pre>
<p>That's it! You have verified a simple TLL NN!</p>
<blockquote>
<p><strong>NOTE:</strong> The file <code>example.py</code> is (somewhat) commented to further document how to use FastBATLLNN. More documentation will be published as time permits.</p>
</blockquote>
<h2 id="5-running-the-experiments-from-the-fastbatllnn-paper-fastbatllnn-only">5) Running the Experiments from the <a href="https://doi.org/10.1145/3501710.3519533">FastBATLLNN Paper</a> (FastBATLLNN only)</h2>
<p>Each <code>fastbatllnn-run:USER</code> container includes a copy of all three experiments from the <a href="https://doi.org/10.1145/3501710.3519533">FastBATLLNN HSCC2022 paper</a> (see citation above) in folder <code>/home/USER/FastBATLLNN_Experiments_HSCC2022</code>. The FastBATLLNN paper describes three experiments, denoted Experiment 1, Experiment 2 and Experiment 3; each of these experiments can be run using its own shell script <code>run_exp1.sh</code>, <code>run_exp2.sh</code> and <code>run_exp3.sh</code>, respectively. For example, executing the following code in the container will run all three experiments:</p>
<pre><code class="language-Bash"><div><span class="hljs-built_in">cd</span> ~/FastBATLLNN_Experiments_HSCC2022
./run_exp1.sh
./run_exp2.sh
./run_exp3.sh
</div></code></pre>
<p>Each script takes the same three optional arguments:</p>
<dl>
<dt><tt>--timeout=123</tt></dt>
<dd>is a user-chosen timeout in seconds that is enforced on each verification problem, with <tt>--timeout=0</tt> specifying no timeout (i.e. FastBATLLNN is run until SAT or UNSAT is obtained); if omitted, the default is 300 seconds;</dd>
<dt><tt>--logdir=/path/to/log/dir</tt></dt>
<dd>specifies a location to store the output of the experiment; if omitted, the default is <tt>~/results</tt>, which is bind-mounted to the host directory <tt>$LOCATION/FastBATLLNN/container_results</tt>;</dd>
<dt><tt>--cores=1</tt></dt>
<dd>specifies the maximum number of CPU cores to use, which should be less than or equal to the number of <b>physical</b> CPU cores on the system (i.e. not threads); if omitted, all physical CPU cores are used.</dd>
</dl>
<p>The output of each script is a pair of text files whose filenames indicate the corresponding experiment number and timeout used:</p>
<dl>
<dt><tt>experiment1__300sec.txt</tt></dt>
<dd>CSV file containing the result of each verification and its execution time, where each line has the format <br>  <tt>NETWORK</tt>, <tt>INSTANCE_NUMBER</tt>, <tt>RESULT</tt>, <tt>EXECUTION_TIME</tt></dd>
<dt><tt>experiment1__300sec_log.txt</tt></dt>
<dd>contains a log of everything the script outputs to the standard output (i.e. via <tt>print</tt> statements).</dd>
</dl>
<script async src="https://cdn.jsdelivr.net/npm/katex-copytex@latest/dist/katex-copytex.min.js"></script>
</body>
</html>