From adae7fda25f308bcaac27c10b4fb3c1997eea108 Mon Sep 17 00:00:00 2001 From: ebhardjan Date: Fri, 19 Jan 2018 11:17:08 +0100 Subject: [PATCH] typo fixes --- README.md | 2 +- report/report.pdf | Bin 325247 -> 325265 bytes report/report.tex | 8 ++++---- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 4a916e5..a96f943 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ # Parallel SAT Solver -Semester project for Design of Parallel and High Performance Computing class at ETHZ. Includes two communication models for DPLL algorithm that could be combined with local CDCL. If you want to find out more about communication models or other techniques that we have used please refer to our final [report](https://github.com/limo1996/SAT-Solver/blob/master/report/report.pdf) +Semester project for Design of Parallel and High Performance Computing class at ETHZ. Includes two communication models for DPLL algorithm that could be combined with local CDCL. If you want to find out more about communication models or other techniques that we have used please refer to our final [report](https://github.com/limo1996/SAT-Solver/blob/master/report/report.pdf). ## Build Please follow these steps in order to successfully compile the source code: diff --git a/report/report.pdf b/report/report.pdf index 4ef6733e1bdf134b24c940aaf3b27b6c5d911f5d..5491c40e90c520a546164745577ac2c2cf3382f6 100644 GIT binary patch delta 18649 zcmV(yK=Tjg6R>pu>;%Wh%RQjd;xoL`^1NU6K&OacRDu}HCb)bUl3`cA>0zDvs_EABGol3d%n`toUEt8f~3d->(P z)=BAPzAxWQ1?V>L^sx$Qb8ajz!s&btge7_OZ{GfhBUZs4iv@sM75-+%bP=BA(8p`VzC zizlKzoxA4L^m8?@t#n{e{`LL6)_V7uYtzvEj6*f!l*qnp1y856yL)XClchWnl$s>6 zhZZKg?lQ}kDed|bBv}R}2HBf=Kt2xo z2FTdWj$-YxsjCInM-`M%>cYi&qAUGTKrl$RH?CHvhqYf^g^K!VfjMZ zh}5~Qzesm3w#(*?*ZRVkz$vL`(N3Fe7)=5Eu8^p_?w zP0Puz!SAw4(tpCqk~9C?IMZ%HVJ!+W97MD;%7aOFAD@^(W(J9Kg;tnZe3JRDorF_; zLBrhiTonU{%b$-%ZR22$zhqrsSL~@^@4KgCyNgp6;@!W5<0L?G~(CnnkG0@0HdeSf}(O`IF)$MT8Blk2ppNPI&q zjLJYP%KuR;(znIJCRXQnn@;GtO}_hl6omu7k)+ODt~l%!nM><7ejDg|=;yXyNQv{j(*#3-~kAI_l=*T9s-ATjlMgqi(5|HQ@lv$|(qwKGDh z_vi?zM%V|+b2ZLw)p6xQp@HKzx<8@P>4F?8wHyxZ+=gEn-jYGIV78quh0}*-7j-$>D>^6rb*mCzK3pfH+p? zb0f4EeWDsBrs^bAJ)9ofz7jJ44BRy={YFJit?XW@x4Xv-h$WWJSK6M@8|cp5p8Yp< zkU;6i_PW&U#z8ikC>CA^N!_&hPmf@BxD$&@dh7GAHT!aH zh4R22fRF$fWL8|Pi{c*QgRq?pAN(8ILl}rqZy`GboTp`8;>-3HZF)fSl7rR8GGoVx zhOc^M28kHqX6Iy)zzuPVWBq7wd&sj;=mA~3jbh*6D+yT+grz8Ed6k%_ue#TN^MCKH zF%4Kvh(Dz3%dzRVpj1BO;$pv`v;U>Bsp?~Mh)Ny#B{*7CO!9aNw1(`~#0?(4D1k4k z^wJL;nHiD{Ndl-SynROl0E$lt3V$ayi|xd1mZHw}1JRZtPKJvJ@y|h8Ub$uKve9mo zq?J84@^mte20>uRy8%uJkXet)eB=vqz5i-6Xu>$v+hvd1>|z1cS8K{f+`3?Ot& zFD{M_gUq^K#<4j(NT^Ti5sC@#J~>d8*z{`Bw|>&OB+GKZJ`hHwf{QG!4p86^_j$T| z|CjflKKnMLLoN)`nm2!*tDJHK*g-@!W`AY1vC ztv~d6ly6~Ps~GLWOtvO&owij5X41i-tSZ~RGQX*&7U+ypPie-ulv>uMdmo}$m$8xc zLLvO)LBS12!?;JBCdCUn-+w(JCacI=Wc15yIdD&KfygDRsdI02GFUp9W6c|g95nwA z%zEMAaQorLwd=QBdpA_%mS8`tuIg*aNx%`1Ei6$CFsDVp68U}82*p852C_rA11Ld> zrI=gav0hQvbu@DXRTTj6Kjvr9aqHc$N0{qzMV=SYC&VRMd!R;Q2!CIA#7zi5(H1DB`4H(gmv{*c{&%9@6~9_9OBKV$LI zD*UWN4-79^jPl|dlYi#4Fn+RS3VKLW%Ja~Lce$$P?)A;!jY8w0 zk!slg;r&urcj zAb3D-WF!U5t|1@>)HIwL`I6IjJfn-WMDbYHw1Z zbIop)Yz~<>;K>#uvtmxz2j+5zH<3)P*>vX$4DT7Vf{`ZjX(N#6hl5ZUR#AkStAGh5 z#L5{*V#%w^L&A?bM{z`mlQqZ5xO%0{UhdE9wpMIoHxc>yan*x z9G5~8TebZa1AmT##SYk{S1Miig=9{lqH)iPt7~irl`B1hUSx+uOSeR&a#c0~FhRyK zy&j3D3!5kv(z@#upgSe6BZk*mAoJ_H20$aqYWB>2HlO(l24u2*er~2&{KOIG)IUqx z3qvfRmMOR;!7;!@xWyD-*kmG@F(BZ9K8=zKI)hTYUw^Jv@0YMV@eF}r_cwllT2=-e zOrJ=P380Ixny(AlKWUGOw8n)AXAe3aO=$f9X` zDsl&9A>bvy3|zTsYUd?fFO@5@f~Jiyl;Vwm%Mt;^L44qWkxw4vA%+IS5yH-rM>1|Z zMOK@%zER;_U>f!DaE7kct4jAH2(kOh=x7cQEv@f?#>@$RoD-tTjaazo{Ow6db zI91b3POjWc76HV_?XWecrElwMA9a-h(UVXUgB8o8BC zU4K%n7iTiR$USzRXdP^`EW3(Ys zro~O%AYcRV5xNE6UGg=ijNb<8tfV`7neEHE$?$)QXLWVH-X5|ygwbEx4sdWMDSy0* z&adt|S7-xPh1~rKh0~-W7zR->2;hNfFMn-ZV_U?+VJ@WC&|P80_pVq2!FVJ4fYRc# zqG=Ee%<=^snTkCmh)t3qsQE3S$X(*HBC>zc3+GiX#-$f*E>?AqH!?X4e(Bsefd>NO z;~c{5oT0OvAwkZihD=v60$D6d5i3frAWwiObi39rZ1vN#bQu=eO|m_<+!{~ouYa$s zzq7LCCVyi2qQ+QnTWz`9=9;kn+7OaSwfMjF9*pzRSO6Y4fIo>Sy+_o!yIm9TcyhV( z_sB#JT#^V$H!QZfci=HNB9fgMQZ3CD@2VHc^~bRyCXQy0&m=|TqXM>>Iz~Op+Jj4yupdY8NV`6+CVLA!s{) z&te0RE9|Oy5{>#WF0wqGLpUFHwcp3yJYgW1q}oOtHwr=OpDkRCZHvS>^M8LBZ5Vv> z^uj{)`F`dfkVI#CiAXuU&ep}ntcy&Ix}7R%VHB{>;lyBeSCIajO!p@ zNK*(VeFGN63MKEMT%B8vpo*Ez={$$_xAV`e&sGI}Mv@ci9wP&>q7&t4zDQ-)lJ7X7 z2x|5tC&Bqa1{OCuqMY0fOn=cJ4inbyA^?Y~kI)^z0m0Hgc$m1#2qt{VwB*0Rpf&wL zI?AoLTSfH-sreBshpAL@5zHV~{I=Otz@HDQv5ilW_r+z#?@Odl#B`5M-E6YAbfdx- zR9bILu~w_w)+L)&;KA0imw?XT%Eb+66%uCJ=kVHTma)muM)pEZTz{wW6L-q+{e(^> zNeo0QB?2`%o^7^a-9f$XAb!--9@6LXO*a70h)wG2(k!SqxwgAM;i6vJiJr*FZx`!< z2bP>s!E$+n5d`w$t?|pTrPGH#^q#7n-nhnEH8Nv&oRw?7D=RtW8Ob`73Fv?~Ky>F5 zfB%`L<@RMHjk#W|Qh${k0F-=8G!Nesli2dsPHUUw?g~b8h7@Do)wM#XTZB+I$7g+Y zb69*oX5%%-x#1@_So6y&NB<+&441K&b<$BG_ zc{#|Hr0672+h*7_w+UCD)s@GO|@?+lE(lk+-{pOac^?h6j7d?o@p#uT}`bY*6f3N3K zoDY(uroPorOM-KJIIZv^?W&TaY z)Bx$qs|+AMBY$3AM6JjDpli68h1k00VvVA#mB4S%PF_cxnc7QXV*yTe!^;{~t0Nj7cjvzt2LgExaB z?SpPBIZ5jk1Q=aae_pAt3d6i2BpfDdl z`(!PQ41qfg&KdbN1%`Jal%b+rtxtYclTWen*Y_yu)iceb%>5zcY_|7tl_m3SAF~^B-g(ir?CH;zQiIk|pzb{8VC(0 z%{W)B#QOb$4}j#}?MXTy%y{5u=4;BaaO(wODjI(Sfro+p)oJ0>O1>u2BxifC-FJJ!<&iP3rm-2e}CWV<4b%`lVSvt(sj9<~DW zxtS#+N+Wn9m~C-lCK@qCU!n2&Sp&*QI3IK>yyr)DD+$i3n+E2rLV-zq$$QRznCb*x zXl9zy>ZHuDt5NyiY<0oc`nCwV0Gt!Y>45d}-47_N0YCai>Bueynay1BD2Ixv%mJu`TZ2?eE@4V_&z!qw9OOzkf)IG;;Sz7X5K=vdHzH31y?PIXUTn ztmWs^y@{i)|42WsmqA-Bv^%&#Ms&UW_U@mP8^%G#==7Gq@#+4|gP=~Xec)5z4DqH&%ge)z zP1h1xZJ9*%wxiiXSVEcTlasDPeV@duo+R44U9*>&CK@|If0Vx()q!(;Qs zh3F}}k4?1ePN%7Db~SBEP+MYeoJ7s(d~~OK6JaGG8IZM%nK{j^VWBEo3wy4Azxs~9 zTI4c>zygBiYLSCHs*j4?b-hy@1O@2NI-uR_tb^;_BSs0Ho6^(hytWJN;8bI;{e2oo z--A$~>_4Vq1hhU93-7SGe@OEzdO=&VIQUh!%-MDASU0VVz$Thrz>WpEl|jSElCj=R zF1z{Ej0fyCFIV!NS3;dZI*7}EgxfkD*mpZO3~rD8S?urKq0x~d2ZIb3{sIgBJ_HG| zV!EktvPBB}gRA#~-FnHV26Kl1?14U|WBhJ;NUvjuu_Mb7`0%mY2|ulch_#?T1dP5% zZBj1!9bCI-d9v2fSx$mxkq1V^oW|iZfpPUXW4<;=G7drO?uX zmX5mq)nIbFQxtEQ*u-qGpgf;Xkj!`iw~+EH8JOuIhtHyIeT1phZJwTRq`=pQX$u8psexf-+lF6}9sq-@``tm|bG>uEpT2i7vLh87 zMC(Il_;t&Q+>DJVb{Ua>+R(2MfS?rts9AfJhArrh!WTdCvksA;liM9?Z*l#{SEp>7 z0g{oVX+*LoatVuHu3caW-p=Yon7YVYd>B8N^hQ3aFymYUQd3t9nzid8OaIW8Scj#pqgRKX%8X z*ofi3;TOt+8BINZwftOBKCm0+gH14lKA9AeJDtbRg7P*4Shg8tc+!IDPTfLx?q&;^ zlyVF~2?=>+K_KATcPE(GkiNU4+l_oYOi;=acr7}Fo8b440{X2mb@s#Rd!=V5FL*nX zG$H7LnBg{ohd&MqDUBc&-NYsy6vr^IIRlM3dZ6AF57Ak|m}rz3C;4lB>KX*ME^O8Dx-WV4B$I)1f))%FnnW&v{d@ ze#)UtE*}SS)*C{4PfHzqYT))lMl;KSQOzOL*qsHC)5aZ%Z9!3z5$(cj2V;zi9yI+YvA~hWvMb7NRqgoV>CE+{*2(6 z0P5p4mS~hz)?D~OM8ojeeY2%-dg9LowjnV^?6+N!R5ZQfgvbCm*s8q5#2o0H&*HLx z-t`S4i>4+5W)+;?YDog-!_Z(kOkgWFW*pKT(+>=PV8bCY5MwRyyNbv5s$zH3t43XYsQVm7v$KP?pheLj20F zeQ_EuaaFaLdTP{xkjW(Zrd%SR0a5pDkc4ooD04rC#fCF4=qm#MQPe{DOj~j@hm_#T zaKv?HlNZG|GzE4bruc;dIG zLC7^7$L4(0Rv?F<$a(SJ{OGt?)iJkHIgEYfR# z|8U|6ptNF75s-Ehkq;56lqejMa5C#8Sov)giU!8=b4IpEe6>FQC1CL|6isi#P6}Cm zFmE6ou+=wpAgS^zQc%()0tcXZYPI6=Tuy~#eq*3)7fIFsO&k{|(QfK{P(d1tDWTR9 zEKzGA7-^qo|A_=%1ZWhV%vG(gWK~pu@Io|fGZVcgWi4WnyQBaaTPfMZSi0S_O9Bk? zGy{>l-U`b2|URY8-M=o>Bp zXr(c*Hgq>EA7X}!fN7rd9Re5iHKngw5q>T$Xn0rqnI~o|ugrFv!@5II>Hj%@xrw$3 zXFxhezp`&rExzBZ34n%XAv}qtkpQ-mrV3a|LP}5w=n;-}BNqI1`+SwLSbI0(`Knx4 z#IsLGicE4^8ZmLzfqR7l1S^q7FD$>^ml6O0-gh#l?Z$BSbx})Ax#n!CARuK@#qCDU zVA9lELm;Wfhp1|hmRgNel~d<`v9;v1Ul1Q#%@#v@5uxJjKx!-GqUtA>uq1M|N8UI$ z;5h!wthXHYq7X`RbQKsA2=i_fEZIvO|KXX8P{^Vs&7~m9Q3};BFSUtKUTeMkrZOf^ zkuum#T{%>Q`%jAauP^L;sA69fhz@2u>?OmN*<$jfaGp|+oRmmH;q&Dw2sKWmN?}GSda!R8`Qa%xV0JsJZj=x||eOK38y(YZS{M zJ`E=r_3^2Ly*`|zLlcjG)lg*K(p60bxhevT5Rh&ORD$9V9&h+~|70D)GhW(wlvE28k8 zq zE1ERbnHr9};Inog)rBUkV?hn_il?`VNvXVKOz#jj4iYz0nMR8MGE9aWiUqnIYn!&D zdzG&ceqWDu(7BBLv>T`1iy!OqTyO*8;Oa989He8DXDZzOXR+ zG~3tRLI!kwvjs0^#WQQ%Jq(i@zUqY%2&|Ene(3uC9&sB~zQyT7ZYV=$RHfH$D9K^( z;E|c~c`o@2AqTn!Z~e_*?#*UiT$p{HB2M(7Fwl~#`{cva?t8b_i%*uxB47Dvxgq74 z5YQ*RGj)xBmT3UbC1Y+qxz>?|-RpvVxaQw|)JSMWV8LklB29gi_4dWRF^KNpynd-8 z{GEeM$qgT=D$Sn#A%h=!Uwx2avrGW)>tGzA@e+cr)jbBqMSV9tY0noczwb@_K`vVK z7KNg_6Wod0`&mu^NGvjDftjGPN~l;Tceqp@X08H%kjY#`Ei|J6cDX|ky)7jv83eox zPzl3Ezto#wuA;)e?p^;(F`JE6X*@m3ge6XJ^c~973M&^>=#(IcIu}VBq^oz(*fwPE zbGtD`v9kBUbT=`ZteitJH7;ULlIUCygM4?fnPs{uV6m?fD%rdciD{YZ<}1lk3AoS_ zraWzbeFzq-pwQK~6ZO2DwO3@sTdQQb0PtJ5{YsH+D*K<(N78#s;cjvzTUrQs2}PU$Zw;cac$QC#AfMT!cz0 z7;HAyR=0PC{M6&%b|3ZW#-m*4s;4W~&qPFjxr!^ph{1Bd$+yIGDz{%h1L2n>@N=Y$ z6yU0R4X82akMV3L<4leOjMOw@GE?n8I!@kVUsVUz?~!nRje8RvbT(q&r$(xValSH9 zapuF9n~R92d-OGW!QM{_G@}nSykSG*i@myWUwNy=`B=7{45(B9q97V(_b9E)pned4 z#_#~dqOI4Ymma|f zMlaycPxC`0&r2;B@=K+)!;Q^tG80Q-dJs@IMM4hu#Vm;V>M0!S)Xmd@%hv3Sq|U+t zeP#V-Dyy5RE?96;n$xXRn(kND?;|LGE=n%S^5|~55M^Y-4TGFjp4-IhYZ4}-$|-l% zCl6h7aG18|zC)0D3Z8oo8!f^X4)F340o)_Gx<`84Bb7W@ z@iyezAI}BvrN*z76=1YPkUsbLC-r)gX#l*w3h-}o2+419f>e0Piq5aKW+^k3@p0N9 zTFy_k7NMX4N)#^kN3+s(u_i{KM64G8>*5!4hR=+O;$cqyAZ3QyZ3uY>x z`!z2lWS&-QntvPIr^Tj<&D{fkQq8I;Ws51*1L8P(_4i+1{rdXnSO5F&9*27IMi%__ z)!Vm5QB~Ib{Xa2R3)`_!<1-+mtT`iadfI!^A? z@%d~rsU#)f@!{eGvBO>OsNz(F!$8^04E2ISqc@j%=oZ|GSgw#Qes#>xbumE_k614|Y>fURXtc z{pkx`@>0XUFi5M#(-1aK1*yGdl$k^)zZ8TdnN{@TkH4mZfjorYP04K)752I%gkpQB z*3XoAu5o!{tW_(ZMj*-aT%ezS`ttAU{7ZPy!>Q&A9O&g=h^_O*T_8n>W4^3Z#s6{Y z^&y2fM%7ik$Ipd-pex>);=tL)*eviwhc4guP9){&Ngt#b|1v1iN5rd(dye9qjGBwl z{*8d*d&e*3_kLnMhICG*6%%UG^Hlof!!qFCgHt20Oo-3ACh;weQ*ogL za6~}BFg2qTMyd7a2kM)*nqwY9C}FA0RwU6YakRl&O7p0HH|YGj83AguiqZ3Q9n0rF zq9wd4pbYbOWWZ}s38+4GlZ0>f8Fjv>h7x<=yXVq%lKZ+TfK@p)S5ukfMhELmW-NNU z?cn<5*(=SixrX=TzPbsY1=0OcE5DM70nop_09tgs%rq&1vzQ;{mlFHYFW>s^b=K#3 zLhyFGqeK9IW{G@3T+HG^&x_}Js&ugljmwMcxMD4g)VbAlNEib`y@;8-hcDtp9{xS5 zk@SB^@ug$J)bb;#LaDYK2$Rb1YD4JtPt}4lr&l6HkRfjVt zy_)`6NG{Sm{@p!#{OMa8GSK5GdPOyU1wd>_8<-a}@a<-Zm3w7O|EG2>S|_|&-L zE74LQuSC;$%}jo}%`8gk(IDTm+iGDJzWd#)ci;U#oZ7t{mjOBg6ti7>x0M1mH;y$PvBwSMZ3A7-CR`!ZtT8R!lo&OA~6x97aBXKy?!q77B|v{rAqT0FXq7 z9TPlMR@REj?Pc=q{g zzhUEebWJ*YKOe6AEQb2T3Ep32=_ExS+;cF*goedZqT#?$7NU0c5}m2>k%k9U9O zPSL>!`EVH(dT*zZnPo>;3NA0xb~qfS-t#>?N7Zs?Jm$h~rsBxdQ{OdAmY!*MtY zse}(@=1{eTbvp?$*u00WHm)$7a-1Eefmfkik_=dNH43ZcHs_}8+Wpj4A{CfQPnW;k z$B_qLoCJaQNOFRq4pm3=DMu~C4S0WkHR2bnFB9`+#;U>9CL{$5jTW&3<5JWEGvOjk z$TYo@C9)S;Vozj=(<<3uICdntcI#>AK>bEuUU!DmJ~me17c;)`gud;?Hr zha$mAZO5FtYoAF^fqw3IY&voOe6+9JqUdcth(@kVuAQ2LvpHvvqI<9nxPyOW@7mYUSo@6-c~~c{zC_%0Qta!Y)Q1U zv>@=QF1K{A?7^|XW7KHdIJJMbcoVmg5P8#0t?Y##jcsxHj>!5NM8V-@wC)~#-VXaM z=|0&W&VlI)uAjx;!H#EZ(Gg_H>`9EtyiZflGc20apWquo&)PAsnae(O;B}{dWqdqN zFR^hxM}jn_FH|Tc=z%XHzXI&VK!{H+3fRshkQd_(RpNbM7bSbq&~$$~k%r<%)8SN; zyW?#(?lRk1V7!@n7S@j-uyyaEh3AAvNzf=*UG;@SirkM!kH2y@zD%-fNB2Ybx%;ytj}b}H_*%zAzs|1me%^L4P z76_1l!PQb(U_6mAu*4f&U`6_lt-wVOsl|4IIOgCEhz{rX)+DciN&4W(1$`h&TU3l% zX$_!CH^Hqw+g^WouSf}8FR3nHc3_VY37A7F=VoZY^OJ@_XEvK4S~(AT7+S(!3KmUe zX$cHs502VznbmSOqQW5b9th~UP!2>b&)Rc$@s**3c4%jp3p98~t+Qplb9U?bYy9=9 zT`@3A%ykS469=vm=Tm`Lfve;KTqS0Iq|LYShBs8%NHmLwM_{kw@Qv01q~1Ux-{fP@W~^dm!7nKBUq0 zVaqQ?Yc`)-piLOZOMC*F(bL*>#qs>0KoWcaZ;DEUX%YmIe2`gy0pMzG*X_Xi#mfD4 zsJ+l9${^85Je|`D#@adl$kbUn~0(6gb$}1lzufwoM>I~H2bObw;gr}(!z0Bw+ zu>lJFc;Ds4(GG4Ga>w&R;PjO(w=JM&mjNNNo5;lmh*$q(i;=lAM8b{(b^%V=Ji?KV2yjqNHY#WdoP<$TeJj{s>v<5xF zRb7OVK+ebjN%bJ;@qgxJns4;}^T&_-ckkbQgbkGTetkLg`0Yr4CN;rynu-!id0z;2 zkPB1rjhi`J9Qc8bT+a6UJ>=n*_dBj)BXfVM=2VOC+N%UE7iU*K6dVq{EF{4>1InkV zW`MeQ)ftKMci_+rkevBNVdgzh=x0!hXsTuK<8}g}Ziwt6y%AHC;!LI%yB+dIs1e1- zhN>`gz)Y_PpU&|#b9jRGu{=v44~}hCZg5L3C9oC)fpSAi@gq`ph9-rdn!1Vs%o~5~ z_X)i=IeM7w-~n5oAsDoEBCQ9J%af{L{iHN9=f2osmm&dAQ7+u_$h_0VO`tDd0F$e2 zpt=4mjI^3T0uqEIkl+w5?}Eg^w#Bi@slLW5nyH3hmQ#_;#NKa`X2D>akDFm*>NzhL zI|jjI;$w(K5E~syJw40d>^LqSDG-0Vg&B2MEPJ}iqCDA6xoJxvcqmLgbRFqJCV(u= zQcp^kd0SYli$OZ^=!RU$j24i;gqFP<5S8piZaGWcju|{#y(tobj-cMZKt#*1TGg{^ zN-Y)Ierj)2wB`0RdlT$o*`kuglK&XzaSbLeBdXKJEzZXZE0v*=WLr7Zhy;JXC3Y@= z-8~jknd?f+IQ=ZkPF3-Z>mu0WM2&|x&SwOG$Dz-Zf`&>>(N(x5tk{kftNt?IbvgT4FL^Xed_(mYntw170 zhE4w%ETw+>|Hb{MfY0SK>B=z5qq?bte_SiLi`R0=&&n7h|GU3E-YK|Auv5D*$owGM zMS%a}FxwT)-S;~`GD*f0RwNC%Wy1LRp)tGn-Q92Sb3=RCa=+U1E&cPfhBWTnDDxAo z=F%R%1*IODXEsoZHokujV+T?YokPt0%x|Ab(4bU3_0|b}{%m>1aI%o6ow&m}dwKy8 zvvtA>W8nFgw0JMaUnj=|v(ii)rv^xT8QXbum4rf%fMl9pL|3kSn`-2Y5?M+i^uk0Tc!faLhF-k9UV zR&AxX?hnzXv65v>r`J?KsSIo?{0k}&zp4VOJzrIUEb$W+-Dp6ZdGWReq+z<&fHEkktctVAjvY0SEi2T9fX%o*m&+`*|Q_(xdgGriBsge zuEm>Z{yW!5>Gv{JF8>3=`09UPw{RBSe*wF-Q{0yk2Lcqga2x?;+5$2$myzBAD3|~C z0TTlhd2E*z_W>h+yt@10;#HKNxJpr-R|rc=W*qGPTTc* zwGKny+3W7U?P}E&)DSpBsT%Hjloq}6W9N^(E(X1GSL-;AoV!w{cUtvr!{cBbZX8O} zul{@Y_RKq5`@WmUF>ej6>(I-fA7^_x%&4k%6~xY?X&!!mT&<%Zb-t9k;bGm_G|7eU-${IWz?!pA-h^zSqrqY3sqz6gXbw6maN4bGaU?!R#xk^)-yr z9ar{UyRCHHCIZRj zxT=$7fYio+9zZp_#l4ZasvmGz0P7DefBUxj9hcP7Og!ciH6-}Je?oi);=b?(LBDql7>B98WFp#kQ(zd9GL6SQ~J61a^W{%qJ zxUJEDr0LvRw9Qw~3r#Wf+zZzpxa(1OvI;SaJApdBBh99nT6qT1XORpd(4Hk4i>M#D zc@)9O!1XgRi(gimhZ}@37&WqhF>VMa7770jR*j5NES3?zJJS~<*qj|#jZE8ssbo?? zC6X!3h1jQK<0;nDF=huYSD^RX&LGXw#M!HV4y_JeB7LfE>o7~FgX8dB%U>oO%rH$+ zjXUXuTd`Ha%Kg}}X7Mo8@xXHyiC8PXO^}65`z&A+Pc5C^x81e^s8VY>LJ;RU|n4j(`L zOIDa8inU!La8pm1^oI5gtx&{Bk-{E-hrKg4ineg$zU_Ontu)sdVhp-L6C-O7?Xc6- zpuISNS+-u1lN#vX9}}z{J1z(Zzbz5u$Q0P?z6x1H5s1R*n_ipUSnqd!1Ry3JAbPLsJ36`!R5TkF;~fjof4QO&>|ZKI{V=Z3*9bnsc& zJ#_j7!#e;41JBa6R~4!SG<tk7l4ieeKT1#lC^!>n1U@8Y0bbm7FASl#q1?A*mVvvB?Rdr&M z1*Oid%|vzTZ%!t30ukAS56|P0O9Wg28q}72N$|uTqW(!3G!s#nv(?;80t$8AloI9z z7GUGbgI3l0dBtGT<}m$#9xcN?+OUHKY5+u|D-RQAg9}ZgC$Y$dlh9Uyj1rl0J{*3F zwubO)&;XGaNDfGB*VYn&u_|H!CwD}5+)0!~mxM3cqk5}PL$H229J%FT(13dT7r31B z6qbnluC2N8DR)VZ2)jaeIWr=28G|miUsyth8@n{C8+U-sUJ6}*OKn89sHrNGFQ5&l5D6{kgb6ry<*={Pa_nq=(a>{)z#h8?9z4Ao5Cf#$jzJSVR*I|} zIQWBggY9S=ywcNujX*CVHwFqFU1e;Rw+tdTjib{oF>v(QR|R=~q^i&^-ULb{$MD^0 z1OhzR+;bb*9V|SRLKuZHF40{MaN=6Nvuehk5Z0Rn{1hTBdgsf=M&dDW8L$mNoIwJj z{20ISm?M9gu`z;?>@72hKR6!)MZ&NzSRjJ8=+XmmZc*re3C6~zDT4r9&7#bCGw_Jn z0dQCcAl-B_yN8II4v#(H4i=LKs%r?rrJ++)7}xX|bE9MBtWA&xQ=prMY|+w?RiL); z4?Di|cOueG#O&1nKL!00dIB?91BNL69?DPMEY6Q%ekw5k`s0V|cb_+JK7LpP_jcwC z-ES^eKES7cJJv>woJ5ii>Z|T0;}n9w|AX7Wr>dP6w9oemNN_+#4*r9i5iT>Vp(O^x z4i*+(;!H`=Em)zU-J61o1b5+!?quY{pqVO+29Jjh3IgvpGKPr?g&8Ey1<>HCogvQA z21{(Jju7|*PV;=hdRT%*F}Fm91*!#f^jsv(113Cw=;3q{ADk(RYj9e0IX;zyTs~(; zcEqQAp1lmgIZs&v_CFFcYH@Yqq_Qcs$6B?R4Y0|&B)2&Y0De@<%5pI z7pF`(GXW@gDQ&7>&fZ#oeu@Ptg)80%yNwOWl^_K;L1)AAS~cq7fB}lZCThQWu{R-w z=?p-B1vgC367Vu`#OWX~*hgPygZrE}%cCO~d4xFf_~0TVi-4&pUlBPfw*2k%ZY=aO zcmR=G`h=)K;>=)SS8BE6feZj8sh2vnX-qv5s)FF|Mu4165w_z)`CMu*#9Yx1Qymzi z(UDV34PuQ{&7h=*X~d~8=#wM~lqizHFTsm{G@g(T4!4U_?r&jpF$rOq3qZiq0MT;G z#daJdL1gP47miai`IL&!4rW>{$6`!VAdm=EWRo&s)9K~a*h1xezg3v<2W0rLxEha|+H^xTEx!-W@}N#^@8eBE~7iPS(ZOd%N? zFF{40dm=(3UOLaz!63{u+_#l!xf2n8AHM(`5{SUb^Hu8MPSFB*JR$R4sat+@@Wg;X z;c~yPM2{^{6v(%M#vav6ZB1ncnusc5$Dbk#9&ttb`yk@Z&fT4wA_f5?(Znrw;f#3+0_0Y(9pfLD=YUs%|E zhW7CbS{^#Hb6;X&p14soVfxDz0?_vtZ*FdGcqItV!QHLEtY}V<;Hyo;-_0o4Ru(xj zGkcts&b+@b?`WqXTIz=WoS(>liHV<73)6`~UMLI#70mtcgh8P&=p9asLg$~R!kJO* z+!BJ2=2sO07wWOeSSW0a2)^kQk9+67cTvEigxGdlv!&a zv2gZE!_7PN6yWUMjtqX~Uzbk<0&xLjm%#%9Cx7EBP482bOC@sB8wqs$#OX&P)s5O} zH0@a)vS~&VPCOO10Dj-|!jVltE@^bBdXBpAq1JMMuHXd|E(l-31*zQSJ*GeD5iFYy zOz&p7C?B-HHWmFf1IxGL&?x-7LnPN=p{2fg)C^S!dY`vR1w>Sxq~G`z1P=4ts3e-1 zQhzHs#lr~F=nqEEOPe2NZV>oK;^y)Kf)ExY2BOI@n+pt#J_rmRDJ8TPI88fIGjkKq zKi19giE;6KbRB^oOV8VpbE*L0^2B?IGnsIPZ2s*VsD#tg&sfjcop@+`L80}JJg6Lo z{f`$H_1>)Saje_2WM04-e2k_qi`UN$Zp`|xu?T`~*hZ39Sh(s8V2Dy`*KIY{TchUc zkOl}imj8^zRP%GsQtk2a5k<@`dUxCwZlNx|2BBBBZGSPl+r^e{o=hj02f2jpZQ@`McTwBIGvO7OvOuiVsWO5cji*HaEzASyEwsj5 zYcDS9p1+(!2E!+@7>gUvfBF=J*?%)w4lQRf82*=}WHa#5tGyo{6=8Ud)S>_NrH&tQ zA}Vp-V5+~w#c23T;U2)4o~vx`p>Sz4-_((be+{QBd5&8_ zyfhXT#VkH{MNtNvf&jdy7xak#@`kOO@8H1sKW?Xv&-2|7czQ5oQJ$h>s(%=NK;^YI z0Ias+tE3T8&$*>IFL4|muW}5~f$7(mn}2xO#SORIVuj#(A|@~JoiI$%hSwEHj^o2oh=IWvR(=EyY!3aM0i%0X#T=02#M?dtU znX)f%^F;N3xVih`exU5s0*4U?1GfdQGQWX)DqU`Uv{`393<-U`dGv}O{1VIoyb3uXGfe(W8P6RFp zGV#_g4DllTqLb+2B2M%Uzc9VcD7*_|JA?yd5S>N%ZG?Y_6j36L3tpQZK9^Rcb3w7l z@NIe#BcfgKb__F^JRgqj37pF_B77vb$mD{Qw&C0CB35K}!NOrYyl65kPJ}Na#n-ST zDSSAK$SShAU}*uqSh^j)Ob}OK+550OAFP-MU+;yLzr(6HSYzTCtjjD`Luw;fUs0@s z4e{a}Y;1o5n?8iiqhMFb*i{5}N5h`aVQ+ERw+8m>v;9B7!TxY) zEgW77M=A(?adcU@w&z3+7hG=6XaDO2S2W5M&E@J?xE2>a_q@m{a`D-pd~sb%{kf<( z2sduR&36TGoGqSA+)m<8An}r8o|clEou<+zXzh z!qfl4-^Jh=aUmPTPH>OGPC-Oth%5_H4C>OffwVtDI)d%e6GWGRQC!BW5PcS6xh^ef{GoW(ix~iTwK*MP>tPk)oVdKL3A}*31Z+9W<#w};u+MQ0(A3A7Z=uhd&^I=Gq>z6oEQ;{i7QX10EPjLjGhx6=7}P*$%LXfw z?`ft(MnZ}vG_(o~>juL~TQ?#FM%IH-l&Kp{in=lTVXXf6I8A)qHW;s9kEhh!#9T0m zN_LaUL^q`eOq~iJC~DJ^U`9Fd4b0RkXKBz`8(~hoP+;f21M@V>eA3o^R9PH?1wDV^ z7=9N<;)nkeer0ml~y zC}($&I(LVZ5l3RhDmX^Hx#QZw5=;dE{|a|eD!P@G4@onhnLPE0J79iwxXRD$Wp>7r4m$S(Y{)JaTlsjg7`s#F7Iow=e}lc zF#{6VUten%)FBUiUBcw+H5AvNK^|!M2Q=yfjVV*#M1wX>5fp@P#_szTRiPycjS5xAC4gJ)w)w0%-iGCe<<-g4kK37##6K^=5s{Kga z4C|GI>wkicTnPLo4llo%L(Xs62U{P)HVwKXjrbmR#)B) z9MDD`RBjwrmK@fKj^=+9+J$4BgZ_ld;3QqopHgtX*Py3si_hSU0((|Tc#gK|&ugaV zIVJste&LFmi+JZRP7B}G5j8|j=O1w-_{U1+C#sJps*k6tkH1>O-%;T&5=1Rg+xcf& z)-w)V3+f9t)OfsIkaf`l|3&TFo1~Au#Vy0S zlGOH29zo}_ZWNexC*|#3j(6*!fb}9(tTz>JeYhA}U+yo~?*a5@-)um#xD5lx39c13 zm?F0KO282P@f3Qt4b|oiqXF1(MQB84L1(a$+MdxGbhLj0JGO`5nr!1{!32#mk)pFn zT?N-Xn@j~5$EOz9NHlgfms+rS|J=Qsh^C?$pD8%=HRwkQ`vSVMeH<+`(@zG%r%^&1 z@EMnA`}`MJsFYe9h$FB>39^K1vVEyt_^Ptd;jpZhpaIy5NbxJI90K2P-M3YoYPOn0 zx3x6|HxGYXr;JTiTBK@!H)y;KoMpCAbJ?UYZC(yrwC7tm_-yOya9J%xOVLVn6s<*~ zXyfd=BjIyxon6WnzG~;}NkaH4$wlPY5x#2gBAPu6Uv+R13l@d1l3m2@%;A4Pks``P w++r~icUA`f2M1Mc^$KNfWOHpPaem)lp|^~xG&BM5nz!{HJK5CQIf*xQ zs*;ljYKGFVmP5|+a%B0}r@Oxf$r(Xjr&J|28z2T~^yTXY%w0@><}N9tthmeKG|G*; zJDfj!{}81`Y!YeTkkVxID`oud^V!_})PML7`twbDjJV$n`TMUQe)q>Dzke&EGPBv; z*C+kev~W>grgvYDcmK2dWAl7((p_}Fw`I9A_y7C#-{_-q^N~#=lQ{Yj=}#S#wAlS? ze{a*>3%>g4=PzIG_b!fiHIMbzOWP0ih_>legBa^-IGoUJyi^Be_fL3MXnE>~^W0WE zjk~@6^4^%JOm)65%|wIPG=JVrFZU+i^?3P>r&A40_1MxcV-dw>5jjaEN&O=J8dzo) zl}X||RNXN!h{>WN&wZcQz#vJK*o~-U6()93S(JBsXQMQ8Xq$%W@U7{d_m9h_3~Bu75h-q*urd8#dM5 z*!0~99xq;q=6q@EbKOnVw6@BI(ep1K?~O6LuXr2#_BS4?9>z%JvQ<2jh;;YHMm9?@ z5!RY0AVWu!U8M}&vZY&pLNv>=#xQ#`4|=-{J!!xhJsw}dJom@CC1K;One_V+`;*Yl zTXQWW)<&1^j`g8o!GGXw8tVFi$TYuEH)%ao+O4K-s|V1JHJ;TtHqRYzv<%b-l*`6t z6vvrg_cY9PKsct1Tv7N=*x{Rj_SP1WE0gOLJyq=(9I%KAQ*Nv~kKOJwFQqV~9kfi{ z*H^H{slI?xt0!t28j%8%J)XbDv1K)4`c_!nP4t)kL|J{cw?@d3GGt6c%0v~OU#ZacLlsjVOb(k;=Oef*ugwAe82)+*P0aYgENoG#Pb7l3c?1ckOMgTsUiA5%ggDjO5BkZ@6YnBa zCVrq6HqJ;b%70KTlK0iZMb6}Rn@$|LZNB?@QiG$o5hZDQz2Zey;x1jfiQ7aU`fh5v zS*(~|XL@TvR@%95=LuU!Z;keQ>Syr@dUJ@U+PHw; z{+m(_lpk-fBr7g~-$#k4OWT5U;%j?cF^&zOn;*tkg&3cH`V@|@2|*$273?p~xoN9` zokSv*!A};$!{P=5F{ZRpo-IoHsqe`2TyvQAKYtC)Z*2KI%BNO*GW_gY3avDO(7t zI)C<;X;d1I%P@Bh&5Z^#J2qBFp0z%ly5_rha_Yh{6QHBqwJPi=^qUg!$z^Ix_s)}^ zfHg#%s>`KTTAjX7HHfh~D|P74k4;yp8z2Ttjh|jnL07BNE6rAVU{EeGxBjK+fZoV< zrsm?mIV>8e-QcfFgD_6IQ3tW`I!Kb1zW)kUm7hPQFc5v5$VDb5p+zvWHU6Qvk z|JJgv*H*+H*b@*^0K?1*k9AS#p)rWt#qrUMUhj?7ci#q#X8tUqBs*gdflek1%%Z4ctFD9!Izcr%4 z!6Pm?#;x0?r=DJ>J2Z)pLB9{E;s4cH( z*@kTP8>Lufhek{%LpDeXvwz17#D8UG8eH>RQ{d2QODuv~tF}e=TV&5|h`rf1QcWEWRk$4TblFb_k0e9%;1)}s^%A3l+&YHoTn>9=t*O`|N!3HwkQl_)N9ygEXG zKi}uc?&E)c{PN`wUq1i$=Rf}o#uS(MHbCu{p=?y7Zgr!W53q=_A-EH%?`nb*mzB?4`KeG7CTw+6+smlaQ+%G+$3PcDBX%5Zwiq5`+ z4?ILR`YpUa^?B59X`yWq1yj2``Yj;x$d~y-r3;7k6wR zK<2Rfe*o(R$>H|HO=vgoh4!|uBrK6UtG4P6T9cqH5MNlb8gNZZfF<+0x>gEFOGdgQ zxPvG~iKV(*-|?`buG?(pM5d|$;2*5daNst(-w!m`(~3N=vQNrOjDPV!P1KOS@Q7Ow zKrAw1_JYj~u(>fFK*XD$t6EjB(vWH0Bq%HF%gjx=kvZz`EC(sVM#xPhe@>>rua7 z{AVa%T9qF*^ZXwXg3c zZ;~4K4YJ*0u@BTuydrGLa*e~x6D5)%34zCccB zyi29d2ZT}aIpW@kry^u#1}K)7sc^X)?KGS-KBUPaJ;D_GQT}*AT$y?gUIY>^A$%hq?66_b3INPCr&)4 z?pfPj0I`Ug$0aN&jv*$)El@bH$y6~zK)?fi86{VAMt@I@etEn`zXem8` z7V%UP4$4BoOMacWqG@cVc{yGxS7b#^8)Yap8W9&7LBvsG;1S3tU-Th_2A3@)$x1}B z>2{7*0TyweX6O`efrl53?{m^m5B>Qv!zD5Qf`1)G*w8YOxQF(=n8hW9G}V(9N8WiJ zK&*?Fw;E3hZX+!eJ4f%!*(bkLm&?#|iaTnf^2Odl!q`|}?o##7ls2wNsMNsexZ*N` zQQ>i}#z}%)xtS~jhym>+n)BQ>hiV@Tl?$R5zxIHrrkl=e{4BfU!$h$uiFeW`^DZ=S zDu0`#QL!GJ>HGrc*m-2k;$wAGpZ#>6)WPL8D(#Jj8)=5B1I5N^ zQ>HA78_}R(gYXfD1>arkHMR_&2AZstGkTrv%PM60KZdKiCSOkv5e;edm!>5g+-k|6 zkD~LNv(6RTkXMm#e`e*hi7JL=R7?tZ1b^+d4R7#8P!4;gy;jZ&E1bLX8!5&+)d$uV zUlmOj#o#L6f+G|4hXS!hGZZzyrxbY_rCAY>U+}76q~D8-Sde|PJ>?uHx%$l zL42Mgm>m^5hYAUEt}SG|$q~e3Nr^a?;tKN=h*Gy(>*7{FJtv1@0cncwapl%|I)8tB z<@}kID>wBMhl3jHyl-{oZd+^O_t#pGOky<8(rf!00`q&eOMRA|57} zr~VvS$R1BoA??PGZS9?S07pV1m@(DJT=}ee)>?lUD{|pz^7u?kG(L;aLQSvL&)9EE zx?+^Sn@2PJ(meW4-eD%32+;ht4u6w)f8sTSQfm{ZQRbFY76}!JQ_w)fc{A`EPn;|s zR)Jw0rG_oX2qY4*UC}plo!hxR2MweF5;!E;Bf;f zLDTwk7PkPo!mXC4*{DzB0?RWwrSpqayM5@+6DNXEVq73_vl1l!+QQA)u78MZYX2Wj zn+D%py>OI$ew^?FTIfu!5h=>+@Gfb{yXe%U+qu#fpn!c&J4Um+$yC^87zzr&bh-6l z+${RVw4`9#cfo@EBE@@puE8y5Pz7dvzD!H|`}Jqovx^sdW)cN;kCBO3(Mg=je3{B_ zH9ti`k<9ED6v1&JgCB2fB!5ozY+wu~aa^!YuM%*2^%;7KJ0Se@7am5u0>La_g4X&s zIkdVvYDYcwPFGcZgVg*84r!`9@mSm-zj(2^M8Tg=s<{oj2)U%0^>PXH3ApZ|KGd7) zt(>UffXbMSD>m^OwoM7QN<0!Rq6BrOP_ALX#7n`<_!?d_PCB+Y+JAs7bjM8+-tjcH zIG-?y7Kw>y^vOU?wr5*ySS4sy3Gzps$WT7lZ`z)KMrcys=Xz$l$&K6nJ1^>`8Rd$M z{&ul$_`=dXDxjBdFoHr}J~e(hHM0BENA6QK<2%P#t3_rA$62}7yRs4`&p_3ojK~JO z1CleJ@cqvuDYrKxWq-`|U{ziv0MHZLB=hh+xrnWI?Tm3zp5DM{R7g4JT|+CSy2X;} z=6tR1P#xYW3E!*BjN3XzD`+aXuNj*{ZOR#Mx>my<(YS!@rr=xXHMcE z`S&_BYVcteMK8Xbht?ySeR9qhr_0;07znJf53I51_?weSe{$!`J-*#T&38{OLsvm< zRFwG-4bu>$D}Qe)fP9TKP3(0A@Rw5~h1ErN44u8~^6YJ7T%k2Li@6c2uEtj#r3Z&L znZz^cb?I;&aJh=HTql0O5gsn$N@7^+wGDr!#pgGhQx+U~ncZ=ynDN3#-lCf>@zqVU z;DdLQBIA>8r!`6E4TKo2Xb7{=IaVku#g{>_kzS0w`hRS}NbYSlMA}yjemkd5E3bOU zKor;GCts|kktuPf!BLT4OJIB!A{8pB)%xOBHTn`8zP@KwubyQdW$rg2huhwVO;+4% zlKS(AB-6Pu51dqED>YFTuH{!|Yo;U({(d?0Q7Dt_o}GG`E%y&^yl|&C(fKppo>A^F zC9(c+jDLe33Jg4SUaGfDHhv+|)Q*YA`hcjA#NlfgkNq^Ybytfb6scFn z0vAk(aj1u>YBbmHX1)NV=Wb8hfnml2u9>eT$0A)12otsVHxRh*5wFfON-OzVNYk1b z$Gr(pL{uR~5ENj0ed8&MZH)_28X3&c4iPbaLG?|x=wUGSrC)Q$)-%&eyhqZ}(x znGH`IKm6hAhyMdc?#P*wVd@jJmLiTt0X3Ik?gS}+m0L-ZsR#cp~GrE6n4DZ zj5N0T#mH7@+95|sa{$TeCOjZOV^OQ;*Za$*0FbPnu}{p(T2PgHW)!!SA;w4Q&5Hs5ltw zqm|BoN`9ViO&E0jC;G9y4BBF$-N6nrqU+_ixBr^#Fb*o#=i84D|9=zS+!?be z(^R%|s`|068jMTB;MnbLv!P))N4`3TNj7DYU}mz3LY?``ZJzR;?xHviK8&_%>h_6R zN$}%(p*2CubW?;0Ho;50wYzE>tgO&I%G~jPpoo265mlbI)$Y?EsH1J~_!KxpxXF{^ z{4itPwM5pqh=OX{(QF|sp-k{>rRz}LM&YU_3ifta?`5V5#!isn(6rM5RjZvCXcI)ii&mkGCjwK}lxc6J!-9{Y>2zlTGuBSj7d87}+<7W}>Q z5@N-4Q{rTc6!r&O?FGAal1~lh4guH$eM-l;-SUuL#|~phmc#SmrrQZW;}{~=g8C3J z`X04Ox#)MW?VjZ+jt!mVC}iAY%p zEo0EqQr90fCbv69@rH>_%!U}0=kp1Y886@#Qhp%=Gd<++X|Sytm`XiPw$PsXhVEzu zeJzLR-c_vti(b;$PO;ni=?O>je0`XiSy-USyDe&NCV&Mp=gr zn9<|ZRDyl6#BMk2<3#=J~uyM_Qi+zeQ2P1S5b@IdO=3X8T4swf=;E?7O2t zaEa1OLP!YSA0y;|guAxUQ5msY@x=^cDoF)YQR8yustBukQ?PlZ-@Rqtu#d&)N@qWI zO(Qm9_&@lCB4b5d1{t0tXS!3j(4D*4 z0!D=#Lr_9OURe+bxc1!r2zp@ee2(fx*E!jq zr2E1XsU|7m3iXz80Ws*t(IHu4io%&*!YH|lOLF}W`I12fIR++C96TTDMpu5t6*9a%A4D_^pWWA63a2OjoM#&nQ-p5YB}qlyD^7?EfP<~lNleIr&gmpB z3+P>6BeJL~B4Ap=>8+L|U_J~Dmcw|qa%ILL-68$J0M;CTA_Fm2(l2<~G|+w5D8$Zu z-KAj60=&^wo87&uP?^v)1V!GkCpW0R#3&S>z=e=j1+LK&i zGi=;LJw$AON;w3f*ovESvEt!cV9|2ATsrF$g^RHcuZ=YZ{uZX;s}dEV*RW6)!7oDm z(ye`V8YgjOxtMxtRGyH@MA@cTBA@|L_jQnja4at}H-^QAGcV{X0{>CeLitQvvNMO2 z;L32sb!L<0`ByXrb|9qqg#zUR%Vo?eI!K?2TkI2mH_e`@7u-HgqhdADkA)y?CxI2G z=OOjN2bi8Dh?Vkb76)$x<@AsubFpGn`k+vyVgW%@5}3ppHwd<5JjpsMNHp#B=&8mv zxyCgJxu#~UPmQ)bIRvHD^3_~9FR+*KNw&$&*BGB}OctLpURNC5_jETyb+pRk%xsE0 zx%3ZzM~(oBSnMeR(rzO1AtIF$g+&rhW}O5pyRJgfz)*fp$QFsOv5S8RSUe0x(_6oj zLYD8%8%PJ@@~b)!mDvR;C}|Rb15iJ;TJd--r$REnF;KR%r0Q=I$Hh^woBAG9kj7$4 zsI>%3)LIBe+NarnB!L$J8ihx5RqG2`6&1XH5Dmwv3GPW*^HAh2%0b3fN;V;uZujhx z0E0aBK;*8rf-)}oV9$W2R)|)9)x!+uWr<2^%2Q{`0Zi@XchcFur)ujsDMDja(4-~$ zno9s$Y4ofO-Sx|dnBm-Gn&*6nz(svc;i^`IpGylG-c@eqk=e>Cv)$&f?%-AWe@%9O zqHV$%kdD!>?Aw%!?>B1#prKg^Phx2#fUTq{Jyw#C5)=Y@gk#-^1;1}!uQKLq??yad zl?(H5_6bp*N={27CayYguTX$sCDQ1G<(Jz+0wBQqPR6v|=+C~+YN-j=oMS2oNSRb| zyOA@PByrXdNUHH6sv4xFRwGg6)Ol=wEjjHM#HUuXMc-aTs5m>2+6uX->WL*R3T)+& zSI!MMjz81bS&sOu5K41&6&Mo;^KKL@*-IS%?v;#C$f709r69^t3e_*qwTVzpYn}V1 zGA2)vGT2pJ*;j=7Z;JT$XLjCKvCnfv2eTb^k`Wi_V)CSLo=}o^kgkiw+Qe^Qq!G>EgsuN`c2(mLFuV1E4RUVvYVkL1!IuWZ6;%=bUNfA7=k zIkcs5WWfjhJv$a5TKSbN0bur&Bohr~RXIK~(*@mBRnV!-Y5a<)+0*N~9OV~2S8$SR zV}~f`NWt< zR^ybyrBO_CN_S4xzS`DJ4TG0S?H4(^lEm|Q*lDlF4>xICI7$26vdy>_$O!RIG#3;} zZKFct`Y3Xi87O8KVPFH=ebw&;-PGHj!$BV039`2*D7M%`nqfyVFo^4aH(7QexGZ!? z!*>mNoIx65sVL94qoUlnhMa2E3@j?)N>swvC}Hw&6XtV_2fvFr#_9(UX!&ZUAYQg2 z3hzk{5f__0&Tq0f#98zf@^`YL6wRCgi7q+eC`%s7Wf=h0hZC2U1`kB_ zPWop>lcqXT!*LgU*6x$K(1>-+t3gij^j0w{l$VU@EyBh@;$|w-Xc0h$$#6rlK(}LU z)0T9v@)g4GtFiJrm$9FArYzIm8LM;fAWx?Ah;9_@Q6Rk1}kQ3BY~jjUzN(LeRCk$Dp{V@1`g1`5epduO|E` z7cF{=Lebq3?!@lhEGqyc78$d^Oi)?HSFDpeTq+MUR{_X>WGW$(S|Ze%uTF^6JmT*RJ4!KoSs`R-yfi)53-VqYXwvUwpA(=yY|my)Ft zaHb_pdD{Aa;4M}`q06r)>RB;sugHkAR?%_+;I?r6l|0&%@qbGnN$+C{ccTm0(n7!^ zXKZyNPG_zUD2>w4(TK`w_v(_A!Q{ry7@V3fF}U31CjJVM;9sL`&E8bqMM|lil=4z? z5h|%*u-U|Md3|TdPdyHH_eq~_Jj!*hdb)i5OhlA_E59&|7%cajd`nEHvitQj5PnGl zKS#<)0j|1Nj~a9S7|wPwOyx+xNKGRoGu8gHWyuvF+2dVXzMlU zrHA){(Hr>ly9t6})k&wfEF$+Szdh*9QRsD3}vNby+ zsk3lEU&d}TWvrVi&scC)n$xY6n(mje+lNK^HFk5ndOevBlMV5WH>0i3pG zQt_hqP2ITKGw^Puc^Q19-@E5KuRSs|AliE7PI1TwpRH}BF}jhiI(Ak))v62i^JWQu zSeI7gv$r9a{&+5UFExIxtN^1Wg5L;(QpTrZUe(@B@?GzKmL*ly@fd zX!zLi{U6|yyfevoUCNIk4cLKy@1{>b?5-Zz9hhQy19GhXsE^Z88tru4%B@5(KQURY zQ0*wI*D{(Z^qv~T7`!${sT`ZcJ%k;kmCDbh=>|&6EcEhLzMsIt?XAvRTnQTL_5rz( z{J_&o{Q2Xh+56jN0oZr}gcD=4hSGrID zZ-ph^ZY=llYc| ziFi-~I3OTknCemLqSShH1NF&U#UT$Nl(1w)@+f#Ge%4z`sUP)!0-YZ>BR;KHA$pdq zL;1`Fw1ijvlVR?P40w$x0aeFtlIV@gDV}ei6+?+VaNTp|I?7zx6u_#Qik2An%;;d9 z$&5vBw;gQ1yn3bC6_@ay>=!rTk|4T1YUNiFF#!6n7eKReGn#XfyTr_I@(T(5=$9{j z_d4rkp5QlTln20nDv>J)^I2Tzb@5zIl`ggxVR3dFm#>A9I=8wG38P1-7crCP@Oc=? zyFa;8T>g*ZD#wJW*D%45C z>LEDQ$`(TfEH=oAf5sKX*K!4NMsgIBo;kAg+JmKRD+JPi*tFS8bIy^t#W9uDuF9V{ z>D9ztoS*4dJ{M2{Ig#w9L2d{j47$HO(R*@&+{_cwi1w9t6K;oEl0z(bSHu7Hda0r1 zKr63}saOYUcJx0CH-pOOmDUuW`s$<=L@GSu@4?UAgFHP;m~l5w*S5JDnJq) zc5LW@tgJgT>&rv$pYDGCq_bV-XC^eer{|r{e3R}H75G7v?4HWqzr3O9+WUPN2VUNm zOq{E_W~#OKVeI|5SFvY%W({4F$}o<54<0pxm_SF!t8^_y2zS+fHde z(|Wg8p>I^i=XeK;L~#tK;BRk-sUClVMykBCWo9>xC)+=FeZy_q35g~jM%)VN^Sy$t z`)~MhJUS-ry`MK%eip~P`MDa8cuwWcu9j7(1*_+E)xL0xSL0#x%&x6pnacU|Ou~OV zbED|sLOvWuMc(^qWMkRwsrPaZ;;33~jK^Hq%~TwjdhWZ1sk|)tbl4AD zA(il^%p9t=ux=$G2AlV=)W#8pQ;wsfH1I0aOOgSru0~#z_!(PoyX4>dxc|2(xIpw7?-LZmk`DoubMbX=Q5Q|(rxpry}?#;RPD7FX7033fLD>&GC zhabA80c{rfNWc&o?S1*d@;%zTbjz$!MTL>CvJ}opD|~4!&m(ogm-S#G50Bin19Q(u zFz;7+lTqp`9bP?3n58l_x3TZasjwxtbN(z!#nz%!Y&Etx=4~}JfFEHX29OWj$uEgk zmM?0gD|-MI5Jrt}8;5`P7Ej_95+ZN9sgbXd0(cUM_7DPe*iXuowZ|LGnX-R;CZKh_4v4- zB(bqSdxF%^4Haq$T7X4_E5KeJ2=NJ`fbE_H@(i9(CEh27C|QfTrqh3kEEE@-4yT&n zj+fau%lys)?HT?M4#Bq|Ujf8H`m2^D$1T<~Q!>CQ3Td)VT*WDBQx&W|JS(C@m?qx$ zsTxHN$Li(COeX@lWHLJ>WL`TY>POf?>&#;Ba32O9`2^@-e86ew2e#aUE$lGleT60& zg{i{=!k2^*W6c)~N<@DO(BUuwX_7*itT5vG2|OL?=5YjL+F{Jwky{6Q%<p*{bhrIa4J!2nko~tCprd}put6~NcY%sTqMX)-YyWw9N>WHXqIGEL*MvPd3Iizy_3=JSZSr|0tXA{IL@F2m^6h13HFbw#;{6w;sQazutUT z9GE5g+J{An3$7A}sX(lPtK=fMO7#5FfaExG6s+T6B)DkC!jfcT0@sHvp|8Q@Bz>ijR?~ua3uL4qaX%=qq$YL9qXf&^M_IB zMLyf}FB^YPnFi#PM{p*F?Xnt*XM^Pxr%?_8&3Ivx<1=&0G}#fC1wX%r5|Pz zz+*CEz<+#vc>M6s$H#{+|JVrG_iiSH?s1s%%m>Qr(Cv{q12s4s!3HJaY3fujBRWcK zfC3!vySzBs!L34YJWm8pU)gf|1@sIV;3B(;AU42w^*^>4nLCF_*l>Ye07ogAMe0Xl zg+_k?hy2KO;c+oqnb65D=S}?_b18)oc3}Bp>`tPu7JVDP4M+{hKaX=B=2Qn(gGg{y z7ojAOGct&zdQkNEKl8GXPxSHE&!6`nK7RNN3#ich<@M0x-I4y4%mmYEDoQBjJyO^~ z5T@Xcn>m{a{2+{7&i4B~EwcFh5jdwy}0c@O0JIVin79wS5_@wZvsjC>kxWRvZ zpAfYP=wY-A5BT+I3WK(Gr1_w75vdB+BBh==_r(T7ia0z)xp2!p^GX*dfwtTL23OmG z=K5ObX+sVYkf2Bc33lNk7bFh0Esjl2^);T+Of@*OoQh=Hc)v-S1)Xg^Zn}-B=e%6r zF(@Vzj3E|<*a#%`^dg-za9ju}kavFzBkHbL)^vl#c(R*v)0RSTQy6;aIvAPCnm~97Uq&||Dp`qOIZNG&8HlakREdO+VBUWLkCtJzs%O)b zS}J_|sl74LmcOSNO|XS!i%KR-{-Yh@YD`>4G^dSIoR1Y&DkCMywsKJ;5-fj9Y+M9( z_gF|}t}89$@Uu)iRmC^1i(rcrHSXTnpCbTFmJSdr(NU6+@CjIj?ML#o$eTlZ=$I2M zKuAR4or~GBRGgmu}lVTwB#{#b1c>Z zn9&umg4^*|9zBdgNo>53b+Lb5OSv40^RcUm)UGhke0rwqfn8s{R4vt$ptWRPICGii zUX76`Y$}w+e|B zJ#6~NU@7&}|1a)81r(Rhq$|THkLsr4{&B9vT|AddepdQ8^1u7*)188o1Ut2hg3J%% zU7UjZ56rG;?!Mpou}(4`up+6;O%uk?4~^b^?CySppX=JolKa(~@9CeXbx7m(jZ;5J z)48;VvY-nZPj5si5S@P}O1U7#=aSXq$wKmV;#nM9nTx+`3}&I|OWZ#;W`$_jV#Gtr zIb{iMWWUQ7>>L}#ZF6F|4h~ly6Wh4F|Aydo82cvv6LOE=l>4&en_|}iTr3K2#2#ud z-WGe5>9yD)Vt#iIIOqPld9ghE=Kq{9j4%KFz)=$ThLXvJ`u2a18)R}>IMfmilg{D1%Ogi8Vsxyw5$ZMc7q@Qh$5?yn$+_&_q^uNP*-->R1M*8RoVG|n`p(_03h zLdez3pLu!aO$%79`KAeEnIGxfhi5X+Y+FDYrE3c?hW-ay6b&<%B26X{9z;7JP^wHw zB_4V5rw5X(W0N$^I;MgR28>SGxbI~lvm-cM+|mNepGtQpw&{$y>xyHRA{sQ zXV*=fRrg;JDn}ZZu~-5Ww}Ko2W!eHUHkV=U1Sppg_W=_F6?rU|C-(s(e|&ZK!^P_; zKg-=b36itB`?Dx_lk6<@J=Y74D?i=7d&iR=s&=cY>ia5*opWdk zLOv-B(tWR+_0raZp(${@$SL5^gXVHQR)g7BQtN9Nr8}DN5{$om#7=KTHIY%W+jF%K)j3e?5R|c8hx>b5%d! zumIK{TK@KJ^*b)9rI~olC2C4QBFuwnRK?A5Kd#V)u%P(E*Ew3YTS3h|I#I$WdX4== z5ihWe51gx?uHJEJq6k+>mb~yVvW1e&F7eW`PTNa=KW_1`i%cgD!Kg%N=%r564&2h{ z0;ENC-?=KZrCY3{e>8VCZ7oyUdmb`vn%GUBlYrVhl(0>Jd@6>KB@b&`BzDMzglg5w zs8V%1Vi_@?cw^-UhtGI(kiB!PrLg4U)eAM!VM(_J6tN%?qC!)xc2ZJ(Ki2!f5Z$4^ z{mw%bS4DE6w9|#@r(qyr`=xDB5rZ^#igv7aTvR(MM09DWe>a*G-i~X&dR}OXf$MPj zfk!{GB+Hz3>eroYVHzIDR7! z3UpwR^Y38W$Rx#LAK|+*eKCUN*>Tm#v<(2z=$zH9kAQOz_(HSVMrZpF3*EB9l^`o+Ug(*w_0Bx0@j zHbE9L?X!RlJ+*Xt-*y9+w_2nRE2upMfTo-Y{@;qi&L z3Q~`kPklSWBZ*zJdBOH0O8Q5X^yZXYl4UD_Xm5|ae`Yi}Nw{oF97X4$e;aj!j)v=E zUf>Jv@bS~XWQ94dSlcB6H}!-`H?(hPg(60Z6!tjm zqp?x6e}xDFO2i)`4rmDs zMSBDCOlXTOL>9Wf7az+=KQ~Hb-XbtWox+C4f2}IMVT;FmLJv~`3Th8jRERmSdpCAu z&9H|hE1Jw5I)`es@&toVA;&~>)sLN?k$zvQUO&SH*!@?y+JXg^#ZFi zf9Dp0P&Qgi36T~K0O1`8Y(SghPu+Ghdu$AvFKz}!SQO%+Gg~~wDBc6W2tklcv>zLK ztvUjZSZ2$L{i<%sIYH|*)XF_caM$xd#;DLs7G}xXi}6^80DUJ67bGc&R6mIQh1#Qh z`%*l9k~u;`_-V=RVz(JslzN#aejJL(f4GGM@OC~pG5mTb*Wf;~GqXOHW#}N0O{}$q zhDzTL+ytg_kU{q+gARg1%~nuO4kiW(h+S1DHd(Oh+}cc3r~c+-LMK3xP5AIUF1bY5 z6`(>=u(1Vb|sg*jWz%_N{u*G(zGUSMH1t~_W}t)Ev6CT$MW@6j^cf1?dM zSfB==G`jLIaW=TnG3ur+Vi*Nm3x-^lZ>&dq+Ik7l~8KHGzAJJlm zdFB*j*RgCtWx6=j(m6SykM6)lgWMEpN9{Z{w&yQ3U+QpkdiR2i*JB>hq2b+6tBfEozr&0)`Fw!Nu%K=VY z%Xe1I*b~BflYpN>q($$1+1PkI1}+1(0f;k5K$IWjHy(53FEchqFp|Ax2Jr`HWuQnH z_5}+>@D^QqAkHlcJ;B)6e>CM0fU8-QIX453m>mFzbpX;$C$oEqyXo-Q1MXlkg`m2I z5L_BMMTK!qkC8VzR?gi7X>bU4L$+vX$SP1<_=g?e`8yG5Ct`N$|DS^X2|aW`xTOYiNnVu!Dt#mpD^WbPHB!X!oYzBEenwqB|M+ zFleRmmdoeN$d34w&vTd|IOi!#!2U;KMlG&RoK!X? z_*knJvjH|`m*h650l;sHNwIln1SyF3fTk1i#VHfcOaKaAN}KAJbGX)@pJG8uDsSe>`h2vIs;I_4b!s(f4mGFaXJVL_R-hb;6CTg z^61D#9wClAKDfxpB48@YS457AEq^<`8w>pm9zf)lJ|Sw5I5Sw-m0In1AOk>2?WIm_ z8dHyisvx+#79eL6h3)uIK9}GNF;}$1R0qarbmSBhgjge0Gbrg{8gVKN`Xot$NxFOa z61+&`3Hjh~f4lgj?iTMXCLs)S0SH(cAX;v@*p7oFh-|&%!f|RQpAz!f!Az^=Sd3{3 z1QMZ&Y*HqS{DbhupjL-OcZ8WG${t6U4FrYe#u*5}1-1PyUv_3*C?bh1C`uBxAW3|5 zVXk*PV18ljkc1eNp1W{-xbUJg$y`4K=o6$aSO^}Qe~B~sbp87J)Afg|>&-KnB0uI- zQD7D57yrLNG?;pa2C1!)CP@}LuT=HD1^1dlxNxgU-?4cEItBnoI!NJ?EO4$=2kOXx4#JTV|pxZLk6(PIk~1@dj6u}Ae%TT_{VCZdhU zc&tYSI3U&|*qcXgl*JZ=;+vBnN@QNS0<~n!(eeE3T%yvw%LPA9;AV-R2GRrWDYi>k zg6FQ6gu>xKIQ#_yS93xz?Tg1H}_FenrTy~Bx7=={@EI5Uc!TS5@h{JKKmLOnJa3x$ml!8e`aaqrys zE(%zb5Zi8R)-+TX88NBUbKJ67H^#P@dPThG=j5tjxfgkp1#T84mNaisWWXBo%MUKq z@KR4SDW*qcSkrmcwt)5<$+_}!N9TKwf98IQpQb#}6>*K-?}85cp6eeDw#c*ORNK;! zl+E)Gyv(e!1&N!I{LGmd2{Zq*@*$LQ`90^2s?`p4Dad?hBaLs>c8hL;>=oslMGs?^ z1o&>0L54@d%J=eOBn(YF`;rF?J-ikzG1OX6%r7a)PMy47y~I)wTQ6H?DXzq5FDF2j zt|cXQ;4G%lEpyQgA2C-J{y#AnR4hn>zsuQJIQvS&%{%lI;OyRx41VRmmuCY4aRFwR z*#iP6e`Amce4nCRDv^`kNTA~2#aG2jlCDF{3e_F{Y9!8Kxe=~Ys+WatcgTOx$H zgs>nn5KV^JTwq}IL16GmDWSE%Y1)aJnVWe2v2KP>jEm=^>j?Z8J)V?ASc;-T>ch1NgvpmG@YKVDqad$YdBv2M$fc>!neF`B+CUSbIT ze{}*qi;pnV1!aOuq%WN`pPkg^JKo*Ag3Xc`{Skfx(2u4lYlTJ#>JU&!F65lDFM;#9 zG3&p^A_%r&8%bVa;Zi7{Sq7vr@Q{@fW7S2IHNY25+bAPwt2qMBP zM#EnU_W;K9TxD|)g-e_HrjAVfYdB@ebKDBzrLnLmX7RBriZb971mHcrphx`2H*DQ} z2M5mobUSr?p6`ah(}N+4@)R9Yf5rF%DsQv_V6_!rC5?!B&Mn1xiR18im1BSoOuxF^ z{KLyGuDRtFD+JdQF?oUSgkg#%FN{3t+3Yc^FSPwPsSun`>K@ZlT zFARD!R}bZ%Zc$!5ns4TU&%-jWMJFf%bRIJbW51d#$#H#j*(L_{}1I7C4*GdM#x zHa12Qy9% z20=oQu8TAV5`ut;fI}-tcL_)-5|>sH6^6LK=iGn3pZ7iIynFUud#$z41VIoycR_)9 zfe(T-P6RFpGVs+e3GpJl(M5D~k&|u08>X*mg?B;5j^O|=h^`{M8xbjgM3hMBg5tBn z=TeE(E{IMYeoZ6Ni*zn{J2Nwwv;dCp3!KZ-D|{rk$l!uu?ZU6wL`IRx1xrTo@Y2b! ztPL!W5^Ld$4&lR@MHZ3O1uF`2W5q65Syx9Eu=6zh@D=PX3VYJS-p^rQDcHXO z4(Qr}pWx5{IJ^;#tc0VnLN|`B4%e1l;Z}dRogMB>hr9X2D!8ZdeoGC%*M|qWgqHPxu$a&Qf4>9&#EFye zsIzzskNZIKCU~+0o|S~>#Ki?A#BOlOU_U~n8KkHPQ4H!*wuMx`Kx%^R(hx-V0;9OJ z*CE|`NZ$i8q!W6sQx5pJQMl-6k;l1=Ps6VT#7iQtb7kM;xfs^#%GDIVLHPyYbN>?g zM1JQgG~h;sTTroo7gS6hQs7`Fl87_Rn(?6gc*gzCoog1oTWi$t$^93g#tS#9_DJ4`Q>3j zF|h>}wueQ3rNi|W6|XqAlZT!p5!eM2^k!Ns}+IPn(9Ct!HctXi~vL~Ec1g8(c84ApuRZ^c*hW(@& zoSzC8HStTz>`SxYa(U2(aw6>e%5ZeG zH#gi{ES|u9x}N)8qx`WP9xQ}Eqs0+;xHw#DDN)k7zeqEmiD~!*62#AEe*PLmSwJli_*pdN>`Nv>seIxflqO4jnWEv(VnjJn-ubeX zxlxvX{^w&l3IglP)5v^K4;wUsq0gb5z--O=eo7RA48npQvLUCy^30hHfzBPI8 z<22JacE-m~4_8!CRC2!iG_Ji%G5H?!FyAwOm!KW`UYcL;SaCD_MP(5ysyN?=rt150 zK>Eazg6;AB?m&Oe3O|4>@dIbTAZ^c})i7AA9LmY=hf!dDcy2*U^Y0fI8eo)SFgjkG zf-zkLmFz$03u8CKIBM08=XCKC=(c`hw4nd_Nu-aTq8Lmiv;8zhZMp`XLDl-1SKvQ? z+MZdYxBp0^%%*+$Ih-keE*0SCr4LtGRaA5Sn+#lApI2yE8^~S1v5xpNeC}0IUA*Re zlJ+BM8EjG#ZlaF-mbYLl9mH=N4cphj4jPpIUW4wWmHJ&Y8NWLa9KC*Tb=X%z&_Vou zZTJ3TaDX=K4{D_AMtMCA1jrURUgT!k0+{+r>}|o;VgJm8FSxnHrEGzY9*=VYky&mKsB=#a5-EvYhmg{ZEO`_XNLj-}a zycDtJ)1djDLVhA-1*lak_#JQt!QW7LJQR5)TxA2%&{=B^0*fQC7S9o537SU2*U)A# zw59T_T_r&)u=dn~bzpz3W0c^3{mMF#w$}M{IOyx5k!b9!3;SkW>G#%63w(pxw>L>2 zdyDrg`!`8#@1ziPF6&N#*}J5?_23QEdMaSONfqlu#amxaCQIbq!unl;{_L9#s4sZ` zvw^(@FP}D;BDNtpVW|H2uu<@yHg7l$z(y!SBVQME1{m|HjY!$ z#%q)b6rD|MCOBej5*1*Rf|D~ABX<|r4Ugra*M@8?#>JT2cLg*W(s9)WOH4k2{t(jB_%~q FMhZiw?HvFB diff --git a/report/report.tex b/report/report.tex index 6df374d..384db35 100644 --- a/report/report.tex +++ b/report/report.tex @@ -174,7 +174,7 @@ \section{Parallelizing DPLL}\label{sec:parallel_dpll} Otherwise it sends it to a worker, which finished solving a branch with \textit{unsat} and therefore is free and needs more work. This procedure is repeated until some worker finds a \textit{sat} model and sends it to the master. The master then outputs the model and stops all workers. -If no worker found a \textit{sat} model, the master has an empty stack and all workers are free, then we know that the formula is \textit{unsat}. +If no worker found a \textit{sat} model, the master has an empty queue and all workers are free, then we know that the formula is \textit{unsat}. While the master worker model is easy to understand and implement, it comes with several drawbacks. The first of them is the lack of one core. @@ -239,7 +239,7 @@ \section{Experimental Results}\label{sec:exp} In this section we present our experimental results for both of our parallel DPLL models. \mypar{Experimental Setup} -We ran both communication models on the Euler super compute cluster \cite{euler} on up to 48 CPU cores and requested 1 Gigabyte of memory per core. +We ran both communication models on the Euler super compute cluster \cite{euler} on up to 48 CPU cores and requested 1 gigabyte of memory per core. 48 cores was the maximum number of cores accessible to us. Euler contains 5 different types of nodes but each of them contains at least two 12-core Intel Xeon processors (2.5-3.7 GHz) and between 64 and 512 GB of DDR4 memory clocked at 1866, 2133 or 2666 MHz. @@ -331,7 +331,7 @@ \section{Experimental Results}\label{sec:exp} \begin{figure}[p] \centering \includegraphics[width=\columnwidth]{figures/scaling_stealing_subset_dpll_scaling_tar.pdf} - \caption{Speedup of work stealing parallel DPLL implementation compared to sequential DPLL. + \caption{Per formula average speedup of work stealing parallel DPLL implementation compared to sequential DPLL. \label{fig:dpll_stealing_speedup}} \end{figure} \begin{figure}[p] @@ -386,7 +386,7 @@ \section{Discussion}\label{sec:discussion} Smaller problems for the DPLL algorithm, which means they are easier and faster to solve than the original problem for a DPLL solver. For the CDCL algorithm on the other hand those subproblems are not necessary easier. Some of those subproblems might actually be a lot harder than the original problem, -because with the made assumption by a DPLL decision step we could add a new conflict that was not there in the original problem. +because with the made assumption by a DPLL decision step we could add new conflicts that were not there in the original problem. We ran everything we discussed in Section \ref{sec:exp} with the hybrid parallel solver. We do not include any further information in this report because of space limitations.