From 562b897277d1e827a223ce07bba2ab87f170d25f Mon Sep 17 00:00:00 2001 From: NotXia <35894453+NotXia@users.noreply.github.com> Date: Thu, 18 Apr 2024 21:28:53 +0200 Subject: [PATCH] Add CDMO2 CDCL(T) --- .../module2/cdmo2.tex | 3 + .../module2/img/_conflict_graph_example.pdf | Bin 0 -> 38080 bytes .../module2/img/conflict_graph_example.drawio | 84 ++++++ .../module2/sections/_smt.tex | 276 ++++++++++++++---- 4 files changed, 303 insertions(+), 60 deletions(-) create mode 100644 src/combinatorial-decision-making-and-optimization/module2/img/_conflict_graph_example.pdf create mode 100644 src/combinatorial-decision-making-and-optimization/module2/img/conflict_graph_example.drawio diff --git a/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex b/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex index 2d48a88..d6d1190 100644 --- a/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex +++ b/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex @@ -4,6 +4,9 @@ \date{2023 -- 2024} \def\lastupdate{{PLACEHOLDER-LAST-UPDATE}} +\def\calT{\mathcal{T}} + + \begin{document} \makenotesfront diff --git a/src/combinatorial-decision-making-and-optimization/module2/img/_conflict_graph_example.pdf b/src/combinatorial-decision-making-and-optimization/module2/img/_conflict_graph_example.pdf new file mode 100644 index 0000000000000000000000000000000000000000..d623059862fb05d884dba1c8f9eda177998d1388 GIT binary patch literal 38080 zcmaHSV~}Vuw`JS5ZCkf(+qP}nwr$(CZFk=`Z`+#w237A(O-(8%Cu=LoK9$OktV1d< zEK18r#|}jr@LQmu7#Rr|2Z2n5K+VClZUKQs2Od0SdU~)MJG0_1XMI!}4 zzJRm5g7}3;CH8X1%g)R0$cxuh4%fs>UFA(xU2ENU+1xn@h<^Y85&Kl2->yWu9*L=Ise0a^Xhq%71>G) zK&FsCm!0QQpz1I&2mx0~+Idr|G_=Nt5q3Np>{+5#>8!4H^X0m5{~2hrkXB|^X|Cq? zBr$*nV19l{Ne3l&nhoH%FaRZO6FOb$7!q+m4FD#q)xYG@<=5m403C?^^9`9OEtN87 ze86HpfT`@#jhVC;nQz2+O~BPnF1GNBAtkJ;(i+MMOO$3HgJsubTOA9~8SOC|I)oOKsHw2u}xa1?^UJ_HJkx&&Mt zi{|1OPz2i30IJ0;o zELalC$(8AniXjY?9D#bJN=gQR0ibb}t52|mwlYW?7l0eSx8VLWO0eif@?_~Req$mh zOE~Y>AyH2hX;l9POJV_*M~G7C=wAJvNB}vJEHl1Ii{`Gqd_GSiWbrcQ*G`KEHE66 zjH67)Y{m`kFh{)PLWyEfsW#Bpoz$F0aLRbv!<}Pkz(Y$m0wV)o>yoG*wL8VQWoGA4 ziaIkvJTZz)zX|c_LX#;B0gYk+R~os{sJ}hP)sAg2bTJKgbsBz$L%7Zg5n(npYE-|j z5Y!AL?$ozJe1aBkp60(C(fKsNi`0$C#!L?Z9anUnQsT9(F0-ERUj!r_5ea$ouvN2_ zbyYPDW#*Yluxu+)PfDV3G!*=KZC7ui9L2yz#WXlWuU!iX2{mW6Oc|yS5KVCrFB-A3 zdz5s&oG-|b+}Jd}+syJ+SvYH9(dZWPwK{BJfnuJrqver7yJ_}od<3E4L8pxvP>fuh zhLK8HIoQ#$XnCCoUT{&3aioC1Ng}ekmc`7>#N55iR@`6{zP99?)fj$q^}8M>ZxgBj30AGD6{fQ8<9wJ zI>D{v!dDW~m89ut%bVrjEHHNyqQ=;SB9-V`+^B58s7h_Q-6o1!&8hX(SU|0o+l1ca z8>j5IW9aEFIuqWwaP^#@OKO`_bz7Q%1qpNVF&|>_@tD}Ks((Hzr;J1?xack_>m}OE zPK!$_y1K;d1x;jNO6;N*T>_avlZ}1sPq?mnSriqX_vSOkDzQ-0nbWb^HItc`S|j0) zMeEjl9mw$sNh_;JMWhXXf?u5Y_jayo@^}j7lvLI*wzsYr`6)r2MbTXZa@r}2;6{}V z;KY~-UdB|XyDz9yE}wTN&QNbG6D5|tvu-Z91Yj9r9dh-(>XCFRwnTeo0T z+vrSBb=%aa#Gtz_&$U%YyufwT>{^*y6Ov|N;-Vbmsybet!NGU5xC-i|0oHGGwa$t` z)|k`O-G~#m#nxUn0^lh~rD&EYQmQ8dRZ2XibK$Q*eZ11a*9)4HDiBU8eS#FqdKJX# zN9KWDzy!oz6%xZ!l)jeuk2(!#4x;q2$+r>dUqfhGF^<^DvuN={5+nx{%ZrSxcj}D= zaTq^kRJ!=?B2N z8XGcD=F9eiMu>~yf#t)nAKGq*#fhU~jysmnrSA(McZzdF5Kb8X@q=J8Ue+hF9k5Z4 zD{Fx63YQ*Tv|cTLx7u?EHlj;4#9ZA6_7)PHKs9E3YBKwnd|l~Iy77+|OfEngs>hhJ zr^g#ha>v_o$MhT0P2?9%@S32sD41O7YP`wm72*!{3-TQw=D4dc=Ttq!;|^52WsKdY zNeE9Bj#o2>`$`XyiYu4K@lJ6kn;O;E4j54n(Q=^fyoJ&wMmr#|ZH)I8AF|-%iqe&1 zU#wfVTpi#|>)l8Fr2MAZo0H=Qrmn6xf~g&0svf>>$DiBhv<}6uJ0y`kgqa{$OJXe! zvL@r3H-D%3;^(T{tm2x%KRHDVMOlwW{De6hFlon8(}%YnyuQBs8(S7a|CP{N{v5dKh_iQe$u=Cji?#`?eM6n(hLIg9w z$Yex@w#UUAJiPr2YCUH0>F*>=q%bU~I1a!RN<$_!A?f(XBl)UG=zPVQ&c-B|l!02x zq)oE1S;156UEL+eQYNpbF4s&TB1;~oA3!^lYuNy))PSsZ$VENq!!P#T=4^EDj!gCw zXJ+p&&Mcy&paceEB1xiTr8p|4SS^9e5!Irw<~Y+md1HdNw5$R!>yokOpPsDmh+e5a z{fBj(D}mLCT_YbPwU7#JsY55*5tJI|ZT9`JW(pV8js z-p$^u_ttwZU)a7>zR|p+xqH`LTzCGV9dZB9ho(-@it#~tWh0K-L6YfVZWAPi{qt9k|tOdC2Nt_V2^km z`8?v?CtMe0b_s40;>L9y!*PiAlJLhhuq2Ai*=UPX9+|ijV+)kbnQcm@&V3#Q-qGKI zb_Df`yw1WNi9M5_8@_1*R2mAZ19V1C8c3~4y`p>icg^tYd#)J%OudsxB$kj&P;C?= zS#&xVIg205t5lU%)~edb+sOA6!YS$1*s8fzx>dwkEn|h5mYXJ@&|~F=9^y40%2xk8 zAyaqca*HgUrLZJ2-Baxd|0C+Ekh>`OTb!#s#?M>=(;bV2Q&g1^17jE^!QD$}<-lp8 z9%=v1&;vs`xPqZP7(*1T(nF3pkp$2a(yWj2>|cmQ*^a8Ef9Qo6z;~aqE-hVOl(82# z)exwhWSdR6bk6Om$TbIJOvyR@oZxVT!AW|Y@N}V*E}qkl58MFANFhoErw`dMPb1y` zb)~u;Lo!UHlUc$A7jKsVFSqpM%(^q|rnpaC&LGek&Cdl=zDSrve}`i+fc?nRnQ5K6 ze8k9_NF>%0#kIR;7NQjktQ5vHty+} zO7a)45h#U2vbR{w&$ssz{BLvGj;z-B<!f{@uw_h^@|l#?DPO9nXJ$R3~7}s0o=l~ohTQa~f z$&SN69NZWX&rI*Ikt0`WK`1Ilw5^5M^CQajf

jc6h#p7_3`n3o-faN5|%BJ0QP_`eNB2U2u}qCeL;FLqOVH?w^%B` zk4xvnQDst6nl-m&sCbDegy)31^x^A zuehI~At4Y5bfB3H17xaK0ZQm!JUX z^GMj(+E-E%U_$KxjLHEL4i0@md*R`}K*RE&n@C8)-8!0)kxUQ>La6Dv$tc^yQWBy@ z$pC*9^;IP$|1*4s^npn$WV?Uu^71~Ju4H6P3?hJbf8gWe|3q=@&=A`+C^Qq(Ft!IJ z#lgWGfc>D=<5S2E4i=Q0oC?3Iuac4s%yOrku$4plb=({X64BPyl$2|Ol*e-i=5RQZ zM?_CcZEPGyr_dOnS8VjJAQla8Z*M+wG=Tu1+t?J9ad2IW98j>PW~;9; zH`8hevr(~i;aeNGrl#1E+)9ATaBHH|lkPS@eo09KX9g7skT&xyz1-iIKN(w_hM)Yb zhK}X0k`+t6eBAe~mhu1})deu1_qPDd=oxMuqKt0+P+Zi}x$URV8ExD z4pW#8Q#~0XJPE?`QYVLNl=YtB8qgpo5pFE=&Z|k)GsGU3z6UUN#s9a66ep`oN2|7Q z?95q|)T&4iaYII?cg2#H=jO&XCgbFChiV+4ct_L~k)8~AXS?}t%Ejxmc_)oDe<|Sv z$y^RrKatk|ix$Xd)!(K1W5K2wS9dd3sM&}4p}zPxh~JimA^zFssI5F*vU!8X^Ez24 z@|Sgq-GOpiUfxBsNk`EyYGh>AHKZ1pCo^tWOuJ^H=v+|ibcTw>xRzACZNyS*KQIjc zvplEjDR`CEL1csKGB|$fNNwYN{!e_Q**>4zky`{!pAI#Q0US|PKR@aFw#Se$dm73RNz zf=?8!Si|-=jaD4l_BV;vZMB2e*NywxM#5TQ&?YJEgvc_QHi}X+u+D}q(h~Q#dTvl3 zA>oCzBestX$2huy9P2rUj>PMKM89c#3f|1ws73JdPOQ2nZN&+uRij&Pxiy{$Y2?z< zDK*75|Fa|eB5wg~Wwy0}M>bX9k%8s&%)KF3}2tQcqEQsf?n8&@J6nFFvc^5p9cZ!$5H>E?{XZ50V-~HL@)7HIpk`^xKOQ?pyYlbeHEAc25 z`9<8JHu18FpKt^9YAb~(%0B7axqwW%r=LSg--wr>b=`GbvHEte0;mS7${6S{CS1Wb zA{QZtcaD}qd=+^}@z%I~evj}W+Ck*j#y#$tqD}Ncdf%;`?I=vw9NF7gUFhLin77Vt z;F#%Bl%3h7fTz|T^9hT!2nOrm*~l`*`oO}>vc$526;~>*ls~adVwK3Uuqj?6fL*&{ zA=IK-qe*R1fwpPR$9LpF!|7_B&wsaCNSRVsd#;z8+b8+cJtDr$_I(dGf>r-ifm`hS~-@Q)gvNH-?Jje z&^jyEzIbrreq7Z{hj7s0VbdM>#9miZCpOJ$a?&_1fH)#V^@F>BkvyxHxbe1SEPGp9 zS6lPInz3X$%Cn=;kN)2;cTH| zf_?=>VLFvio=%uRgKnw@I&Iu3&DcblpUwlSkv?%mIWjF5Zn)Ngv)l`Z0tq2@t^%v%qV^_XOXY zd?1`wy@YCxcNwfWCnu+6g?`UC`O9ugs}40ITJ#g(#Obv$y9EARq!X@R5x%ks+$>IY zISGVH`#r0Ryh*Pwzv3s_y|TPXeX196^|8IGSCi%Cr?F`Yd(VQLsV4QML2agj25S)$ z1axw<`9dKmG#Z^^V$-HoUClEb4o^YtkZs-lD4Xi)pQ>qQD)et~Xn#vPPn(uDX^Y|o zWe=X1lqYC34v{})P6`A~<_Y89PMR3y$ffpl?dozUeb6ZMvWkoivvcsyWY6gA`!lj_ z8~>c$?v|`g#EP{TYssOL?*=;b6PVA80&cqiCZCnLawZLK;LG2ulG#9qzslEGX z%(dsag&x1Y0mez7>pTljBX=|t_@swiBpN-q{GEvHwii*$z8a@yj$x5uY6##IK9z7i zI_GY9(_#F$8oQ2`mk^YWo-l30c6m=l#B2Sx!DOHphu4*)We| z!@Az^?d@Y`Y^2$mYvg`!=MYM7=r>@;dbH_8mjET1Ob(-%)UD^UdL$7|#r*2tLbh!= z9x!J(!PvkRHGF(P?cMY~jC#Z~u1^UU2DrlRH9Hu&E|iizhMrm->2_mXbeyUbPT6-7lKex z$LTP-!7z8uy<~Lu)hl*BJRj4jC=}$vQqaXxhzc7s zGG1wyoVAox4Z{9$Jvxa8^TUVp#i{soSNJVFSlPt^ z3^AJ+HjxfpP|#2^mMyFsxp`{p<*Oi$2_c}iYS9()N!1EUM$HUUb4^WYdNBqCnmN1a zTpS%2vjVba(RZVq#9?~APtRRw(%2lE>GzptXU(uFm`!TdG-g#^I7r*#~kz!sgK)aUBozNE&U-c(g$y|0Fb4nwK^rq%O@b1iYD#R;k6{!Y3V z!jfjjFSHA`wDcLPp*8v$<_6-)S!?SCM|;Mn)WBx$UM ziCsSZm7t6mk*G)%^&_DprIEIC3ciG$G>R+*^926P3Ke1Y;DG(5cTe6qWgyUf^?1G8>Dm+{mp&zr;@@MrYiBWQgSm$MTJ zdKeD5zCNdfzN%xZ?;}yXGB>_+Qea|y0~aE89S@g+GxOQ06Hm)QB+|pBTEYU z=278l)ku~%(yjxV@aFN`*Ax=#U3LEm=WKiXkge@>1D_cSIw4GrXk0^FntgfP6c_qJRO}VXialvPDWv3R*g%^SVqoTM zWnJkjV&mJ|E6u0KCqe(TH04EF{$0-Ws(W|eC=^rMk;BnZONE~lcO?H6JJ>~BK@akhJ0b7;Z5Q937&U0 z69p?QgsyBP2?PkyG^M()vUTA*6gj?M|x@_OaH^4dhj7@c(`*T+Jl1{Im1`;z=ZR z-#1H=(GYT1Dy`&gP=1-(uh7n)D_hodB0iUq%gh5d;5I<4psKmrB#Fv_ST)!*J!=w* z+wRT;bUIk?ltSpe5sSO2*kAz*3%jDL_Iq^jcUWj8MqNkrMHcfXP$n){t zdMiKXpBKDxFtO=+&qgxvVCTrHbJ6>ZL` zMCi5`?C_(+A{mOTsYcIbhy{4h16{#IX-4Hu3*+!q7l;0CvwhmD0b&(AW@#aun{ ztUN%&Xe*;=ATS^zI}!JL9D_CN=VW%PvU(Z$d_DQVXFIMOY2z79RzaRiLEB(tFIpwi zLV7rX&5UQU`b_UnIhpmOO{wB*G1^>rfBB3seto=$W*HtqWXVuz&YG@>j*(j`dKHDH zO!u9}P!^5md`az>Z~+rbDl(GkhGnSeg}5A6rwT#C-UvZ7cf%Jz9Q!~BVcdkkaqU9) z#Q&Xt(0vTb%?ktkdi4;7z=Q1EtM&?iK;`06$;$n^uaA$Zb1F-M>#j?VOk*`6>m zM*zR^i9ap|_X7?UOe0M910K15uowAKvsVb>@u>yF&#U%5SLyE;6+p4Sr;h;j#!exG z_ydNQd~3&mLHfxu$>^Ua3M%<#p=?ON7efVeq-O*%`MTB)gZIrE3gy8G_Mn6j>gWr# zQoditfRplxVktl3#Q-Ga4ljDZv>T)#7&|KejXJ82@dMQ&7%Rg119ixd?H6%Z{#Wk+ zitv&l(J#U?`asVRNc178U2!}DV@R$Lu;r7ac2M0HD2X99kDqw-0oi;I^%I2b5Xu)v zNq#KOh>Gm?(0nxIlcV&n>_^QxsNW~ZFVSXaUh`;oTNYn4^3j!UY9gOA+vZfEl7ih(p`DWIR_wZ__9_#VRpsLTy7oDQs4}S<1X2d|$K-)02*gW{%7`h(&( z4Ew3HO?jl#p5PbR<$$~w=Vi~l7x&a2ax>PWJ_5hbyFJM_@+HXYzw)WX9nSjO1aH0i za?>0Ut53Zc0k7VDxuaaZlDosW-OAl^e2?=DAkLwSWdv0GC`yG%Ud{>A!wC^|FbAD7`R9lEQxYk>jJNnk^A9r~Ad$-%(c>I0RZ#v## z*KaspL3TfIuRA6`@Q+(4KXCj*m2Wm)L`Oc?+qOGO-9x)WfbZFt{rvc_TduvJq4kNE zedg|gy}?sKyn(DwTAUHvZ?ss*H_+XKE(aX1SKI9VEpK+&1Ke-2-r+89^xi=)Z*zP%9qTS`A*GY9{^0DK4k zn_)SQ@x6XdoP$3Ocwuj{j|a@X$Ud*xHy~q(-|u}KUws^9ev}+vQUmAYpk;X|*}jVQ z?-IWNq%031+gH&39rFJIW1waD=-Iy7_U{e@=XwybKfgBUflGbA*3$Oxj05LmAZ7T- z{}U(-oQwThqh|Xm+rK0Jf?o|{wy&`L`)S}3AA0t8$Nu9SXqg`w#~1U!c^;(f&u;{S zf%C9mC$wx|b^CY1U-0XMl7HyQTKlc%J$HY9({fe9{n8N zf7-JDeWI8BL@oVH*}s3K4WHwG{r2~cAAi8~vmzj&Ol*z+H?ixt_aAl`6eH7r;fekK zh+#}@Z2yfHrjsyd8%%&Odc!?};|7mCzi9&>T70=WEc8?CiVtAWOo9q|FwkZPV3mYN z@Mh9$mu{D@;$##3%)hroqV+g$RfIFUbU-2)7Q{v}C17#R9@&NyLfULud(GvAgS{kI zOapiZ4(Iu78#0uX$;FNIeuBbf1IDpk`7CbUrT!5^j0GQU4+rHXScPt&HxkZYbiGW$ zqWkgWT(!wJa%zcqKdzA}Dhp*sO~PdWMnY;7?LcwaS<5L<^t}>wbm93%s;#`|K!G`h z39qb8l!K4VL*6OeDK`m@_F;?Lxaa%vAcANz!s*c@lXGE^U*FDCqn#~uc<5?07%zjp z&DSr>);{x0F)u(i~IK%|KiXo6=50!XOfByq+}4nil}W1wP*V#jaE z5UuAIqTRFs5bc4{(NIy8ah&5902T37a)Ry0Iv#fVoPPFRK6EZ+@+!Gbl~*b%mE?M? z_yN=*@&S}e&5l`QKKFtBUjdh=X>ycVH#+vy_!l$@yj{KyHcJ_=^GJY~q4uBOt2CE~ zJDl+uNC4|UEp?YZN1}XM&-vvk5w5cIwzh*gH~^5SG&Aa+1k$!SD+ctd&1(WN&e5VJkXUdbOQ$LFKLct-%@%AiAI$6_im%q2#Jaj z8CE^ilx7%78xnOWA;S8|Fmak*06Mh@5_TM4K5bJgiz}Zu!M5MKxe&2MolLI@c3w%mBSsyaBKw?p|`SF<)nJRKVTvX#! zaC!`=c|5gr0!^f^P7wG+QU*Ej*bWCvKFp-2RXTxIJ7V&?m8=kLssW_NJRnk(X25$x z3iU}nkc?)m@w;{T8!sGDT@-ft&PULzJ=%e*mA?lM! z1(-*v=n=tlWe7xUz8O-?NI7e@KH#NFJ=#uQZ=p`I(dy=fiVQz?5* z2hx+t1*L^WKJr5aN-?tn8n+UhJ%vW^pk?!Z!{v#ETZwws1S2uW~O870k3lz+L@_THrftHheOmTG`e)Yx`J9y(c|Qa-NA)4l;}x(PQ%yw z?t%_Zp~faA=0zThASI>kT4S?Bp%!>a>H3i|4I`sMBH}^X69y%7ar^j%{58sGq~bKr zvE}m2E>WfJS%*U=;a!a?%YU1I(O5DyDlLrYm*$o+%1ZRBkE@lN-9N?Wu;!j0tPvu# z`~sq#nkULFIwi6za;7phj+L9ZC9-*yIq~NbOg)mNGQVIbA)&U?WEHfeQq*#p$!1yw zdUMKBl6g@=Ox!-AshE(17#DYdkaRXNKHAy5VYU z+9?exn)$Sf>L0bLbWIgiOD7I*%yTTt3b$1Ydo(N4IAwtdYtf}NbFhu*PWeZ$whG+y zo$Iy_+VZNq;8~a1njD>y2F*Nk;_adlE~%Dvt2lLfW9G${@We_jFiD&0p6O0`)Q#t7 zEoGbQ<;noXuzcP;R$`r^T1M7uBNn^s>%-rflvOoVv3MrcNfNWaF)gYrz%P{X-(Y2% z1S&O&uLNd~%z|D=Sz4;l_Ua5ZAIHwVy5Fe!V%(WndYPmw6`*cr_iio*$5J%QY3-t( zsvOd#8W+2%4+0NuBAWh_3C;u~!+JMiB3%)w^w#`oM>0ro>OQGiSoTyIYNjd^)gcD4 zzzBGLM`R0w;7v@>t)0oyRB4rmrmC=LJKDm5i=wDI*G4Pb{KjQbJmkJx8Oh$%jomeQ zgCnBsF5X*UQQS&f<;J6>mEj045MGMHi%xy(j()8ARCZ$1Q07~iRE9-W!K!#VHq&5U z#D!z*X?yD_pAvU7w^6DB@<4TIm3438=8ai}kZ{W*@eGY`ev){PTI0aQJfE9PS}>nE z`}f1FWk@uIc4S3z(ucqfa&)|ubF5^hQekq<+GC`p>!CnLfWJV0DU;yOUqmP4VBxvu zZkFNlw^>6aP(UYhmUUF4wca#)j&L;-O+#_SdKq0@0Xs>>0+F=o!wM~xj%0 zwOLCWxE=}iA&%10F7IeXtVNwg-P1!WSDB?ltDT8Tb!AUQb*bI^m-m(po6Yn!?~G!T z|B+eopOE4nA6xMBsz%9&O|Ech82XNxGMT&AY|Wgpb9+_RSEj{3_lOte)sz$BH~AF* z>=U)hT-_&XmdsRaS^zF;QdDx1=Mysx^~9JuTr5{qQEw&bP_+k8Fjb7@Whcv2Toj9z z+iZCJT2{zPB8|trd-C}2qkXsoJ^5g7X#zsG8wu$tF1{rB53ZL~~8Jtdfk%USZIq|;fU08hI-z%AQ&R^tym~YT4UKXnPeKj ziffFL*IHFpS!&dpV2i@{Tb>?1Q3P%HMR@h{i`r(}=YuetDmz7s;@3%@-n>VMAi8NP zsyS2pXDom8?#3#_$`0t+HJ(&u1ZVog2kQg-5TEvrU{>FOd2+J2Z7CnyJFL z*2tT)2mcJi{3ww!@k{LIR(J0(Rnm)jI$=3kOs~|=^l^0M^ZgP1v}74c!Bi*6JV@<5 zpGVth7R@WuD^azoQrc39V%Bqa?4{vW{WZ$5s$Nyqqh4*_W$oRqIM+sQZuM-boISa< zh}62GzBbINtD6yDLvizy+Dyrfs&uZzs;G7}UncD=YEda?yyRxZHd`SAm1&%^EUWf=N-i=-vb?Q{T-@U++HyueS&cJy*f9 zzP_Gyjd^7mVHM3$tFq*3D|L%QPnfM?^~i34Jzz1;<$$(;xQe&*(svfNX=N%KQrpT` zNW+mDsd=Zo0I9G;C+A#Y#gjROvWqiU6Khqo5o!UI-+p4Y;+74wR2VCFthBO`4Z{e& zBRa)SNx+kbafB3+IZgDlwP`3T+T8E#PwlRL}WE4tFXREfi;pt)jhLazum8HX-n0gPSnCD^1B}f8 zWZ-kI+re^LsD<~#n-%Rp@=45w3H~mLp#Po5hDq;QmxmDOZ{KttDC6UV#$vA<__IKE z{!jqy{N2MQ5}Ngq_3n@*=zrVW+?xlQ4z`NoZD8{~i~u7nrb)NHd@4o=d`gNE{wc>c zLC6F@|Hi(F0;O(5^pSP(QZyg%fCM)DSQ7I^)9>gYgD!I{2SL`4h92|Hy2Nf~U;vyv z9q-l)wn-93;ph)H$WT8n2Wd*MfaWz&y1$R#FafmwzBuqjGp=?21I!izXlb||VpBL5 zNAo)(koc8U*kcozw0ZwzROvlA2=qP%%1<0yNEp0)Bna47x=h0lGg}C7ZSgSlmT;b( z7~Eruxpun~?&2I4LjfQ)@wW_{2#^J3EOh+#sn`Or&j?iUV~N+XV>lA{8Nr3&%R3|? z*0{7(FTli!?sNn$2mKwtrrzfE98z2iSnzt(&Lw#;2LUKnVyz5k2ni z98ehbkB0DO9&CK@Kbmd^P!PE>HEF zeF#DS-_->AvriZ?!s!u=JQm>eKdG$`jsErk)?( z&u9C1BH6+0Vn4e^a2_)+{z2@S(FcsO{=wF@oOzUt6#P$Alo#@lC{hxX8>E9D;MxpZc(!fT1h6Y-2b60i;$u>J88B zkyRsPEqGAVR=nqj4w_axC6F*1ee7HGRyYvTRyYl7+|+uP_NbbmK*?toh+2eXo)I)c zNLSZCS~2G98#Y(En0y2OM7Xc6+^ku_24?Y$UMAgT?7rKqTax*fr~Kk;L}9M30(M`0 zUFogsn?BYpF@H+g{ZOq^jx{|GTdF&p;&&8T!grukcA~6Z=`oaBu{Nw(yRBQ=Jx!_v z)?=y_T9*f~5}bCi(ZCINXKF8jeE`A9j7YWlBjL9oS$tywzPdO7B&okM7w z?GtAJ119OhCQk^mW&+Z5=xT*GjsdcOp|gT`t{ibpo$`Z1G76ZO8#6Gy(lNs_G_+$F zo065YPnQ{(Gd)Y*eI@iT3;Yzt(>1J*Xka#IU{Jy|Fk~Z9pofAVcI~)szR2WF1)-kj zn+WRXo8-?ml;@lD6W!8tQ6I$So~IhUj#(dR9u<8RFCHhl3u$;RW#rEBq?-qfuk{-( z8Sco{Lh_Ume#aFeM;4dM0EKNadYR&*dnxMDPZ2K4MlE%=r^W@dgRLM=!$_vq|)d z<_#E3)ZFqe1=Or$5x zp|R*>pEP(MFnF&TdW;!*3?FJgx-R|e zs+17HEg7jV*ialq(gG>j>$9qDDLVgfq?J4>eZsG}ZF?x^+{Kme&BpBA@dNsZuy{)K=0=*& z@FmIX&yt_b?~7{*``Xu0txO7|y}XHFMi)i)gg66g$Fse>-q_GC>TukhWl(k$3@Xi~ zG)l3g5Ri}Z+!?OnLn5;N9`rys#Cmr3JUK@?SV=Vjpp0b`EG>E{Tm#EaFflqNXBPX) zx6p6ZW%#=-@Kj{%4wuo5*Yf8Plqq*Q7&kBeE(iO{t1a^HMe~j93-TJ;N7n4=bsfpa z#I&rJTj!oQ*EM~~2jzzKjX1C2T5IB6vUP)ZZFmM`P2n#XQ5`tO!G9!&8{maRGCGNvh3DV8XvBP=G^O1!x^ zgD@s>G@4O5<1&Ud3)Yk9hHyxen9n_Ug)@_&+|I5OJb*PsqxuZ;7`2E0y-1V z6&2J%{uASzfMn_y5)_=2k;rFw=$jM}m}+EjqBJ&w6fFOBOi6Jq?h2M1vsc?_u7q2& zr`)v{xN-)az8fIjazM1ZteENu1N*;AdE#ILX}DX$i8elmWG3!e&kl~_>iFt5^X zeky*E*ie0IHdNGASTPW8s55pY_*Y0cfJmys$`)3~F}ld2S(~5$clp$612wJ$arfFR zZ`NSyh$f{Vsvw$xKp9`iaAzo6H}3gG5oUw!QK@F^fM)e~*3ey_R!e>JXKj0Xdyz)m zs;aD`qoiboDuXuHafY!+8=H8Sm|`AklEqG@A};*R+~!HyBW%WD)?r2>r%6`hK>I*5 zvC}w*X@qlxmDFXDt7Kl|j7pkTyUdugNn4{r;}WH7>0e{n<{D)U)2n1hI4Z_{{NQ9gn{`t+#&F#%is?qY6m6H~X$CBsxeZ@aTCC>y# z6*@3^b4wSL6;zUfJW~ia-AypUjW8S<@c1=j{Wtqrv~6sgW%QSdi6P9|4aqM9@pb&cv$JfzGp665$3L{x^w5E31srn4g<%9 zLF`#rJi8P48g{U?L8!oYxT6NKv=w$>nm|h}Y)fZqk+f-`SfM)TncF6`xaW5v&&ves zup>g=SHgW7`Qrn=HsnHnR{w+I@It#AlHLa2T>n6J%l$WmMRG`j8JM;Z1L=+=Qr>SF zJz{Guh>@Cs1O@O0yIG(glx!=h%W{+=|KH^ z%ZwO}^a;2nPMi@-ldO*;Lyp&OkA5RcqxeSGi%-WLSVWTHrjLU+UiurY<2umn5NHUx!|w2?}H=}%0MsocjQw*deqZfiswp2Oi&!pBiNb%dtCRv#kSA;un%>u5H@aKqI!&ZT{1MDkR^3AkO(b^5!j|3 z`f@&k?uzhuSgdm*Z=FlWRgN(3VByp0mjXofdo}xt9J`M)LB_iPBxOiDNl+q^=JXFt zdQh7?nrA)g#U4TI4!8GzF!qhXnFUSTn`~^`w#|)g+qSvMZfx7OZRd{d2t2`o|&#WRdcFluI{0kBF2E!=P+?-oOZ-Is}DXbX&@~ zAvqRF4zJiQ1^ES~rlgelkyCr`xXqy}<>@o~D{kPu*$nm;!cS>t3^mK)1+IYJIIMz% zep6&Ciro40Q<_&gSQCsRQ?IHpH5S6o(7J)t*l84z}8vq*>#667!v z#7vpBgzQN?5_rb~53uhj?_k#C1t>~~g%T}M@JjAg1c*fDWTO&%pINpPVE<}SFYKLZ~)k6Q4U%BP7Ie>*T8;)hoL9kWfy~) zTyKG6))!}_wz$8tRekhrxQKhqRf9Zy(Q>N+8n+Ptq;z`8lTIY*>QN}ANKZ|nsL4#m zJXvyNNmRyESpp}CQWLaHG0Mr^OhL4MsV8vU$vBg~ptlFUixVKmL5}g<`7{LE63@ij znc{k-;*sRWGmf^Rp(V{}o)u8DMaC47HwDEMtDLa$L{FE>oS>|Wrp{HKJi78<7U-P% z&?U5MLR6Z`tOZ^mUYPwucoWK(?no#`qhd{d8IK;fH>+(h;4W-DA9sayjXl#}-gpps zWPONyKs@0*jXj;gc?f|K$uq4*~ApDPi8?ikkvjn(K2@lT0^a{}^E*Vy@P#pFRY zlu${|_TVkV9l4IUtq>ZsvMV@@1g(Ro4x3TNF-vb+DU)le*gYzj`QC)Y0|DJgJ=1^$ zS;kV*F^CHQHwzTys4`ppcArcRC1e<35Z~}}VmMn8P>9W%WDvS8l6#bw4okp@)M>#| zSx8|X`vUxfAVmV|-wwU54AvMR;`8>bKRGRQi4B|}$p~eOg1c_d4{cX<1{Sp5?ai%q z*PahB&kVm-R>B+qO}#*qPzuhB547_{Y9+}O_=DaRJ(+Ak$M$DH0fRU)hzPG9OcNTM znGIUO7~#(~auhz55cdm?1}b`~B&RYual0P%;6zzJqa&{Upswn^8DEsoL#CU92~0RR zTJy0|*WXx2ZorPp0TBUs8*bxGT0#s-8CGnuCl=yURG^06WlN%>Zm4e*fJBvQp9$;f zR;-N>)(H#MXwaSR;Hfa^3whx=`kiBPH}-ZdE%x-Cx@ebXE8M6}?6{ECjlhfw!I<}j z6|gJfjN8G4Kp2O$N22cgm+=PjN1@wHq25~PDb+#iy$5o%D%q~kq7i6}A#)EvDavGX z^fFzR_Ze$B=&(a1ZG6Rr7a9P%6-Mm|at_C1`wJK1bh$rxBgu;m7j{O6K%`+dWUYhU zmhes7>Xmb|`-}S>&ksQ`G&M;OWbK0Nqv>@uVfYY=X>^3xkNr0_tAx^3Zg7sml-~AzG46IY|`?3pl zO@fBM#y*d3Y_jDb{4=>dfW8gzyD!BT$lz)O`@R~1`AtC~ ztHm|wuk?iHt^3J)3$fLgxfq2+1n@PDjUd-w2h;28!W_5np%1 z8Yavo7-%W_{UU@W7^o?F+dCLx`ROr4obrW#o3L(pC`bfy`wmGa%>%{p`SU_@NAQ;z z=obM3+1>RptNSN^mg38kWXSjz1Sa0QgClA97d&-B2}yb`z_9Jvs;GZTVK5NQ59d_! zaGUsN;ETtoD9#sxR)YE9pn?(9{0sE~QDClcO_50a@K*$%>3y$pTG1eL&=)#s++gpp zl>#PdiS$ke;ZI|}`~2{7#Y#H@Ef?VZVfVCh=`*uOMZ~$=+1UQZucFyYe195ld{fA%V#xn?C)W(a1r|7(d6XX|^%{QS7%EpQE3n|tJ z{R^pgaPwV+FUIFN)D!gS2C)v|=??LRO#L3Qj^ODQ@doYcn^^VKmfIU!di%ql5ch`Y z>&J{_2XgP>^**9!T5qgeg0*K*Z!7}e_){UO&9k4Y5&d?o#Vyu$?9?;9fx>so%`@aAZPH5d6EI>pu1;!)H+RJAN14ss9e* zJN`R1jz47WuW#a&n(H?O3#a3G!xMkzuC-oo9)ERmdqCcH*I^f)Z)AIb;rT_!6IJI$ z{{q0#gXu%I8F}2^*NOQ|&=rmOLeNEe+UXg7-S2a9)LD<{zt>rBF#mK*=*ub4m-~|W ztT-S0P4_~DyrKCPw>aCuBA(gT14g#Toj1(xH+s+CTM@X=s`I3tfxUkVJrjHX&X9fJ zb-u{s4HERAj?|}K4`C+wg}1&S_y&7CBV_e;`a<@kJTQ93UiV2|?DO8h|GUS3#<>0# zv;sRDPB4Ubm(TL^3(sK=BioK~y)oBLVZAYgWFNc;_bW~ig!e0s>hmtoNxdNic)PWK z_o@6JEo8q8VonXDWxte-UolY@dgIbQgNGg%$w~-Q)BJReU!B5FN67yRB&PYv8ox4s zTgXcM8JIs@!cTK$WWT<>El?H&6VpD^haP6WO%%)@WkU~zC=0RDvVt_sA7Mieq~AbN zR*;1GL*={C_pqwQuchCO;?q9EhaMEZ8-1Hh!cPgm`_nXj9YI+@l#vyrWB#ZcdKml$ zQnG?%%pY+>4`wdq{6a3dPEG4EFn;w5KYb(rPe4|3otW06 zVEiiZZ6Pb^rDXo#4?n$@lJ)=Ab)qb6f5#9r^x*MrB4z%t3qN&`k@eRxe%<&sC8T|( z3_Y}do5-1e*A6{&qbxj0%lgY0zv_pd`g{+QoYtdZ{7Uc*zK4lV>ya>iwGTh-{I;Z| z^?Y}d`Q1rU+Goko11EV&FE#V;)S(AGlm(CP(M613<-<>Tzg?5kdQ|=ce1;4?WPkfe z%Wi)+C>?sh{|1t>+r-SjLx&zNQ5ITdWVacZe|HW&tbAb_bsT?xOzefP6~os+LFk32 z4@9Hal3eDGFVGT|+unb!(0j!WShHoD2jypZ2VSov4@|SEJozf`55pGN0q`XC=|t0I zE8U_7XkV-eaN2jf`kap)Hb9%r(9H;5-MYaeLumCqhN@r$ry4ucxHkIZbX#sU{?j2-naBBs zMEQpdy#^p}JQ;6dVnTTiig?-9j&vRQI>cIyNE;YqHuv(<_72bevqii9);3H%|JDLKu zDmX`Ymmyw+Gz4*CDm)rGw!qs$Il`xnoP&bXV)e#oSLB-wY;Tbuq(BMWVyQgZMepr? zyzEGI(0o5`h?fa%hWpO0B;e-iWpe;3zMe3%m}$>tXn1q{UTQq#l=ymR%`w66E!X=8 zhwXLII<*!fQ}V<|cl1Km_s{_zCRCbrOjX+q=vek%t>`;zp09LdwbWE1(~^up5?zk? zLZMm^Z&3GDlIRIdrxS&v1|4nPVlw7fAd+?!0w|8xedpdrMLmfJ1*doKdaWHLAE_NR zn-Ak*c1BYql6DVXQ>U47JBf112^k4_4oRX2ploMz$@JWN7FjS>xA4ojhU6Ivz7;hx zQ>ntK#yn7J*n6tV%Gx%OI)^Gf#4;kCE#bB9EM&ofS`* zq69C=@Pi-2$ZI@-h6&x`_FP)C{ds}kc4sRf{6&I4cjrhwIAe<`xXgFC$W~8b?E}D? zck?K~N?s(jaGXo@Y&fYT3E?8s+$%t(*)u28MK>YBC?Xid6brS;VNj`{$%*n~F`tnY zt5z(nSUA!|hg2<4c8h5E0q^R!N3WQYyZtzWR*zt!F%|cPlNIs{sz6b1)V(rv5dRtn${ zAoC`OMxiNvfA@)hI&??LWc@_-sw)C)h>7?0rv5aUX=|j4NIu ziNgAOR@@RJ8@PRAX0cxv?q}j?v44WnyPLNHw4A^TnJZ+bTPSfsjCjP2;osmIz2JC* z59Pt#g!&;PdNE3e%tx@R6mDnfMB;yznj&Co?asuC-42SwfH&<MsBn~Ca%o(dq|bpP=}|6T340Q`P1mKD z!PAcno_6$;u1rPmVvQmX~9Os#pX<~H3_ZZiM*BofmO-(bbSbjFzC6uDG>8jc-%>=B zL^oR}7EU>>_BY_8$KXJoyI(lXuE$p8j4jEeYRN-Ol<9Z4YV{Yn5X4gcNC@C0(^1s1 zP;DEY5m*Ca$zLW(1r-5)2zxt!|0;FoV!D7?yMuS$PY4z{q}sMbbGu6Q%=OIe4;d~q z78)JZC5ArU?i}>EESvZiFzWnk45>C@-t;zE*I|)$;}2^~EbufvW9od)XbV!ISR>V= z2b)_y_xBAfI@R@FSMfFR)P>58tQN&| zvR31^6L4PWWCBKx!d?SCZHRUqrOIP52Tvw~l750_{%5IUuVA&T%u872t=RZdL-wp( zS>~Pe>${=_896Cw+9z3iMe?P@JoM}o6d5@10H`6Iy~h3STe;hg=iBr>{>!;wuTios zS^C79v5RS7;uy<9xW4R9Xml45;bCALnTuvwT0GMjTp}vQKTGkFT;0vXvg%ft2V@nb zv@ofZ@0E_Pw30I1qimCIzfDe@($_hJ4kf)pK{N^vn^}2UeazWG_-tH2i>_{j%~Sm%nZMIryf z*AgRIx_vWz1Q-%Ean0Dik+U#yO>zyjtYC$Z@?iSc9!P0i1e6O)dj$gj#t;KZC@Cm- zr0H&xu zZ|#kXQ-&2NA6Of-^1Er9Tp%h32iJ3bOU2s+>2SI@lwj5Qtehx?7sU?qT3076y^Uqd zvw)IZN_{H}g^^{2fPtV=FR-dDt0oE0LS8z(kC$so(E&s?k^<^6kZ9CZaqUnz=LZ!?kk- z1X-%GwPes`Qs;4n?g(xMuViUjvaorH#Ho8-^t zNeaFV;SwCev&>;D&DFIB2;&J@#~ptKL-J7`j0LXJ@I&%#rf4+sbq>9x>wg-Ex3XhI zL5PWqi6kMLL7uwWV^-x;B>IIUYtwmKO@A*=zGb=oA6bUMAsu?4XrkFU_VMdW8(R!> zz&P7XkM?1?oLPrC2M%8&4cDvh`ZY{To8vXg_U5fr3Jvh$gPK3bIK_+8B1j;`lC@1l z@>h)wo#OmtLRQ@>U7N&LN;Zm2Iv7Pve%Lr$mJO>KS+i8LP}`NLQA`aPHl(Slv`DeK zW&TTpqY%9It09_E-S=+i+ezLdb4xhPy6JRTngG=hpMV)Okr-!nfwm}jqJd>@Q{#{% zzwKWJ8`2UHMvV$oHP*nR35TsGCsJ}yA@03C;q7hTg`gu}B2Y~<6UeQm#aZ0t1PE+M z!V7Wq?uuHNC`#@GiRl9(RH9F)0w20=evlNmIS&rL5lKH2VY@Aecyv8>Zg8kpWm>6M zLt7buQvJ^X9-GS*YE_6@qBPaUhb$Dy+hKH@j2SX0wtVYmnZL+&x z%+i4b4ChSdvun{Np?A0!)7z-1d!+PdE~SXYqbFiqrsroGRXqSLn4(yb*lj#-R(I0- z5vk4>md&v{8s)vqDumr^_d|!5cj##qOUqI#?*nj`Y?jzH3kB>}tv%W4hwP$cq3I*A z(6n%}(@<2Bn5gO(5tfh(iX}H%1FVq+D^H z@!)FZM#2($JZ5Vg9}OMpIo?w3?hTr_O?TbM(&VdWSuLzcuTua$p5MMS1%|(?r0`Rq zYd`3zWoc4qxokCN{9!(uqs1ob(z zDZ1%*0lh>WYa=0bx1A2YxL&c;)As2*3l|5Z);hkHX{5+Chi4;~!a3t#Mca-5TwvL# zzlyjV+HzG@SUhQC!+;Av_a0^K3aLvv={m9hw4_81={&N8MYq~5#f#cZaplRVOKh)R zed{q#!{?PtZ6hAe@2iOkpQ|bXj{tG?M6+lAAIH{cIsaP<8Rvhbko`Z?^0>MGN5+_5 z{Dk!&6O!1|YlId>B$1Z;JXjR58?*T*C`r@$LyH!Bmk=wJ@W_!0@!I6p<|ze!*KDxd7|&-wzb3tYcIM zAJ8oH{(9zjmPH-ju^dDF!$sTjka z`%e#ktcCGZcX$YHNo}$p*W(&Jp8~NlYAD@{_j@{GC0L4v{QT|$>PNApQjotZves1iHR9MwHp7I zSWJ6YX1&~HLgh+!m+rPhHY@k`G?g)to6;1OTGX#`s}|j$+H3t;?cVl4p%Rxen2x_P(RMv4UnvuSDBd(g(IqB~4C7!_HHqB~951}kNt zd?`hyv+ZaRK=(*PK9@J{TR*vIT@%#8@md!%AsJoPTq#*VEsH6mkPL&!)+|6FuB%Pc zoZ_6EA(cj&@|b8wv<$qB4ml*{V&4e zSTy0jO+$v=`5grkjC+A%&!W)xru@|vCEkc>%GalGhXg6-@ zrVGbQX4G?|ZWdKFb5sy}VM)(NF^NW7co;%~{Tn5tPPnL`TJs2gc`#a3@GkZl@(KDE8_qEH_o-darZu%F=qJj23ICeq2k2}ld z$%~$7o;UknbCSsxnXQUK(JJTN$f0Ec;sjd!W6*+&P;=FdKoazfOr%O1pb&g?Lip1D zY`3UH$hT$=4To_#teO}e$r#=mh}KT8EUor$40!Q49W?2?!bS+oAv1#zVan=*Dc z;`!kj&*LIFC;s7m#-d72AVsZ{wumsjR5d;bSrow%TbiVgk9Y=>O3{Hesar|#&PXTR z!@NbDbVjmi1<0zdijUZhwtc|n5df9O+dFsNw z=oWYtd1aXUvW;~!UDjykGc+CA7KT@Lm3Wr=rr#e?Y*6={1JbzVNGjAk@D@_;X?YAF z1|9t9CA!+skzK_~ZYZedB*{PUQe7%ji{@P>zNb5z zXq*UwEuc)2kl;(|ND@(Rshq$M0!p>=k$a0%Y;r^?BlcdrI9A^maWDSJP@8x+uTYZd zWGyrO4&YpOcZ|iv$8+@W`wLgk3aN8pKjDhju&o$<)|bqM1-Tq#l+mxzZ49Ku~8tP{`9G{7p5mz)x7?l(6&bk3Dx$|cHU zN+!_u%PP>%Q_-wq<6ld~w|3Q8&ejK(k3clgscl3O0!mep}DYKO` z0&5)vyM5yun{o}dKQ|^Adz)d`-(UeBpwq3eTY^S0L;Igm87>UlUw9PKAAZ=Fx+$#L zGQAFbejOx#18(Bt+o|AOa_W}4^3Y~&IZ9A zupmJ+5N}l~24_MvkA_6sEL4&|Lg&h?{bIwSPi8Bt5f9$b=x?A8a1;%hT+4}3qWvY- zq{!!&nfL%vBn5lDQn~Y)4(V6EmHcTC)I>a28tTDOGlFihrL0>wk(?Ts3b01 zv6;8S0`4SjWJp84k6g%M2ewjvA|!t!?wK@4vJB4qmsh*q+)UB+_TpF8pVFo>3=Hh$vftMi)Nv8&d$yuDO&oP4WwSto`I4cYrz6(#NAq#HH5tDQ7%iUbxW-J&8bS*hb^yP}gooy4e0rbo|9Wd$_r zn4}tWi=u=en#<9v%1pBl%$rRKx%#+Qm%AS}RGmho(`N!y0^#qRi@sV9G-mWJuEV+p z+7~yHNnZ6Ga!G#lXWN`8q?gO&Hmo(yS!+IWPTB(n}D-!%-rV zek>_vitKU2mW~z|KbyTI)Z+#^f5uQgWvlr!yIsRmg~NF?mr$)g&<{pE1gwU6&iQrD zti{PhVU>7){NO;>-D3YphP<53dHf-ZVs795fHS(qoYUYEfW{;Bz#rW2vUEOcT)1^n zK^06?J_KFR5kQWCdl1J_dB|a-5HBN;upt9i@`hR-{Wm6F#6_FybS+odpLY;l3W=O3 zeR3WHy<=0YkaiA@Z#iKKLM)1nB+%s>jT{cKm9%Dpxjg@)yqb6Pk(&3C-KUlSNh;jT zt|)&7l_*e|nt#P7O^h{uYg>fHijL37=VQt5w~~ICjjrFVZd_IH@njk(w_ZjLh}Q2^ z8*fli1LY%8+&}wu-0S!1e1gy@JZr@Zscm624sN`U^H$rim zU(Yi<*x~|)`ZiK(P1JJn!<}}I(PEYdcV;{ox6rWOSRyR7-pik>x@XRm%oxWJpQd!~ z=2xbjIrW~p-9U-x;U})P#{9{;GuifI+(?o6Lk4H8CA6oKbqMA43!4BQeUhet?ieRK zME+VMI?UYS6jscpzli6}8|R4oQ_uez2LkmgAH1_9=WFZ3+Cq9!T>*O+c|E*5@T5=O zp-dcf@P-CL@?E$oOl^Er2otna*_*d6nlJ-Q^U%#EX0!))hJ1A5h}s7#q)&B-))?!9 zYLMW-EB_tglQALm(q2ek;MVz05)&xoY*0MQ1?$moSxi}Lrw7Cwm`2w;jkKx2xq&J| zCd{h+zMf2c{2(m4t6yV=>5y()w$DEn4KE?bLe%P+ueAmK(O>25*UchC{R2M@<7Lo; zJhq7D4fD|0@f75NFNL_$&k||Fb?!h0CZi_qFJ<+$-MiGFb`>R(Je5r60MB{mB0kr! z(|MgO?5}RJ4~A!Vd}jkkccTexvWx&_2d0brsg3HfF7l2hqOJ@V^{fd;sHU8ypRhJi z1T>$Dx1kY&s_*%Gi0J-h&mzNw|E)4m7#5TX?@wAZBK<+z3A!^u`23nX(P?v+x@}Kf{HOBECc7XPkz1GlG-8rRUuloew8m`) zAuAoBTZ#V-sDP_~k4Sf6)tUPyHCTLa1rnH=GZ=4+U>m;9CxjNoyzze2-e8zUB>JUl z``>kAaDm`$q8;PmUsV3^j_p+q#Np)>O$9@e>-;OCwvUq93f>KJmSTq}H1D8o7Mp!{ zArLn-VKnh9H#FH5f3@q>v`#z4Fb34)*-yo_RwG&!X?$4ZEfVuB)86 zNRm1-Sr~H*cr{YczVn>%@(M-F` z_)V(aa9@WfSPka~nkbuTqf;x%_R7+7O|eo~ha{IMKL$Gv+not|>$&!Beav3V8pAjA@Jm%K zo zHn5Z5e$5qEKJrc4FCLk5u9a#LgUDjMwc4rz_w=+n)vvza!59ahWuPHgQPpSsBX%+x zr}4{mf{$Dp8!QEYGgcP)iC+_``xtQXplF%BI?Qi2(7ZZWQEBNIuhWOy`xvX6e~=YK zTvGj_7)DhxvlBRJW&2z&Cwh`qt+#`39R7a5Bi;YQ7V?lbZJXVogxpY9;`Ys|`@lT> z2S51Fy6X*S^v3i2&rHeisPhcax>&1hW5mI?HvWGnyn42 z0DVxbNUNyonq=E|;BV65ir)MO@F)5oyHGOVm$+1r zCCAe1f9X#jY*|io1onl-w1aKA($S(+nFRg~$2V~saG&Hs;x+g&{o{8rm&$_}I(Koc zpha$vBBInIIsRHzt>1C?6-5?dr$l%-m4|?Q`=$&xyGJO7RM(q8>Dv_Z z(YvDmcT*`DFx%&B;G?IMi|>~w&5((dY=-CR?L))}rNW>mQ6w~OtS4{%zR}!*Ac2rc z!DwK0X%Zja`5-;wVZP4^U)9c)1~)?3lSkhUzmsnL+xZP?Pbw)oAxJ2jfO3rAUK&H5 ztBfeUsG13hbz!agfGa^B25KDcLb4?h?iYH`T7rpKYezH z-eujKe&wK%5DErc(FI^shYOn(cP=XR4i{i+>+|+`7;6JGP9z37TCu|4s+6O`pei zO<8>roXox7ocGu`d`+DIxIF+a{+{1$P7L@xx1#Hp27%I5*e_JDLh0HiS17Hu@8Ie(yKs$Lgg)f} zJ%sSCeyyyD9w%u65c=6=cp`&6d|!=mSkMGNDN6g=(x@s|NIoZ}gAkVLPS}*w;)ukU z+}kbKM;79F3ZgHo6CT!To2R~zVUC>HN3^!}r`mo}f( zw;KHb`)~qdB(z12Hq8LpK-Qxvs%Lmm^;Suzf3s3ulQv|QBhGh&x%s&0p|y5Gd* zC`ILwmy|c^zg3AFW>bUTwJ+`gVNb0(md*et&9cU!TkYqjnYUR6s?H;usR2M2sr(A) z2-#D*9v6>BD~PryZiVuQ`e?ov8?82#KL19`FKx$OX(l!8$zLnkI_%itedlc-3&yxe z)B>=<7|i{qA?#w2gLx+}bb{-qlyoZVO(#8hR>)K^GPxLY#xMc_7?gpBU>?Ha+h=tB z_p^Imub>-Z@yxA1%AzYZ;I@x;JNz%txMUuoV^4 zX~aw!m8HOBzeXG8>eOFFq;wTsj!&Jr>>wKj9~7r~3^yl5XGd*xOhk^I!23p!bYfZubeR%7V?62w)roOkep?)<%W#Fgz)(Ng8w)a88JSldA5`P=B$l zoa(dCUIy*Ecx0p&?M*!%759{_bY@PQQQJaz#%o9r=kfV4FdnQC@`&=m5 z3fag+gd@~4B}d;q(FQekHPM;uOvpSc4<13suO-0y1}kRJQ};8U93}V6Rw{T-r=0B2 zg57l0w}m`4D_jMA+|)wiKkMO%4;^#w+~jaG-EulYp>8kr$HYbik`VHTDmZ1qTPAan z!p07lZ;V!tNNqtmfVr$nDgtdmO?4s68_FSd33Px&O>I;5b>p1p`gJK(bV2a``w?ru zynq-hA&cZygMYea0^qUut1kZ>#o|Jh`TIovLJTl~7Ts$jI>sGQ12;zL(#~TV0pXeB zj&Wusc`9%5@M11K^gTy^Ub>zC8x9^yz_sD@{&zha3R!XohN26L?8I2mNup+$W_L{f z&-#1gmhqZ-1$j{SFG~eqxJAyO`Ckcov#fEa_&G14*Vol%o>(t~qlDt0On0I2f>G~A z2Z*Hp|EXjPDlb%p5-Q-N<3uk zL9P;Nn;(~4+SjK82+G)2W>Nl6Iq!- ze9K>~-H-b?0$g&lWKN+zx^;+u6)OXeJ82|r zHI_j0iomCI>ndRdJF=rH38?CU4{`_gv!(_7Xj9gh%JbkVcw1dnTv|@?=yj$&ffN>t zN^gQyrkL0TC~D?PA^0iqK6l4iCCD5R+y)4Dl10hlA20dnFTphuEb!={c;^rD$uB75 zG>fg%FS^2pDymJ+RasDrHeix*-xp`3o2E^wHdE*}lKt^yw|Zl#mp0eejb9_DpwQdN#jtJ zW;AT3+~mPfE^qiz$B>q&3g@Z&3vOA}Ib0^%#dvwsxrfY26gV3V>2y2acXNo5$}O~L zp&oJdM|%MKuQQ&6-l^ghs@d0-v1EcNugP7JMfsnLD0knKVq@$(`PYm6%`lbeKnur! zB1X+^Pnm!vIR2j(ZA*L$c&P5~T@DamL(OwCKiAn4PNvn`kxGxmdUKb?m-7<|NS!sn zFWe(3+XKr6Nkk4n=+|=B)cU-!8VO}xI za8n~N*a)g@0l7`o=_E%);MP1J(ALsaSP~ zuR4og+6FA>)YQU`{q22l2WXg%U>iO@Y&LV!jX=;(f=?xH_A>rXQ>2h#uFWF`)RpHv z8%t5!Qfh(#gpqAnEq%14{35j)TBwFjC{m!AhAk0;oQDJyx{}=TEMoK3?45Hdp(ds^ zJ(DnItk*Z$)~{y?z8;Bw^hTNlZ~R28fcow7;I!3mG=6D^Klj|nbq7s)LUhWp9#c9n zi3db4nMGc=>%gA`UvON+j2gY&o!UW2fNQY|OFT6nhRqt^+`$KgH1B$HR*{4PTG5ZG zcpl1x1Y`)OvDzFWcXCU$CTO>L`z$el}Xr3V02k{A_kU!L`$SmQ1tG2`P{A1R^ z>2D{+pf5gw1`}ToX;Fgy%RiS-GDqG;)xfRxnhM!=w&!O_#joiFz!s!C1gZtGqLitT zuDW&7(QZ_JLIeNc9t}8`9eb%Xey`&y&rE=7hAK zYmcb@)GeEYF&qi1PO*)1SQ(GWH?MwFsH||O;!s4)=A0cqyHw7^KWIh1J?SXR_)AH9 z66`xcq>R_~NG!4B7V)%kXIe5Cip~$uLv1N>s}o;7oY8sViS`Ut(1CEmg7HHrYpr?S z`MgZX1kxVTK`v9{4|fa<#J~agyq*t*rVzzGKtn^c%xzNUs#@q8@k(hdIx%-^F;Trz zcAn>|hLNjM%^y4StYF$p8&`VpaSYrKk6gZs>;kLfkK;4do36HpGj;TsTzHgHkM;PU zFcS48Q(zrDJcpSYJ9Vh7-hRS74S6QG%4S7KoxQ}WCiHLANH_Jak0cmUuNweM<7iEREAx))*JFp zrcC*!w%swPwYHDJ$~pw(5X}62*YibloKf1aci{`ZCoBkY7c=h*D%T9X^Xeo`5mW+y1d!yOY+`Eea2us~2@%70;J~Xc0bdj3xnF zRgtVt2G~pl8HnE7rr$u$!s$@R8(8Mxqi$JggKFSy#kOFi#7q-FYd2^e-XRyZx5{MY z7oTR5`@&dWNo(fPWON!YQznQYLN=;;NQM^B1X0B+YWl<2gX?npZGcy}VA)6XC2cO^tj5{uZ^)zha7#P3C3?J$^7lL=u z-i$BXX4??`gTTtuxZkKGvwcv>00BXFf50j1TxK%9j!|r6(rJ#TY5fHyW;N07= z=`9NU!i_n@MQLt9>_-b`MJ5dsq5o3qmIrdP&6DjozxP%DPll9&xxU}Ux7gEjl?+>f zQ&J;u3?YjS_TEa=zcTh`vz^-aJ?t?=f*QGE$*2GE9dR*6&5dCfjWAPY5ZoY;M#s;U zS3=HV4_*N4F>{|(EUYz@`5n0SYD{1B3jP22Ki>_e685~`9ELIq`o8Q=AR74nPt_N{ z!6%);hFEVvV+z2o`j5fqfx*V^-Il-+-U zHSJ2s5nVGKm`qHJ*dANUDpffrvG$%)E9Q07BG_-L-tezbKd|jTr(hR*CzDU>B{nMa zHD|&Gu4%Q+uN0h7DFa`QQ#`79zte@eXiA&D+k z3sx2=`?|p)@l!0xqr7YP@w6Ci=TCWuN05#P+1*kGG_+dQ!@-pLCal$9l|THGa40O| z=oo#vXqcj(H}z~92|o%-boXvu`^r+)%MZT(Oo@uVs^uu1Eazh@nGrh8SuH>5!5bloUbfuAzoTN~r=$@!_}jhyPmtphxvnwJe+>GoiSX+We6TT`vQ!_-uvwxR;HTITop3xpfkRGp+*~d*BUk*W&I-^z<-eHS6LoRqT)3Rx{$>W}V z%+$NGsJFO$P?&{=G&)Z5SjkB%e2Py86)XIpzP?bl(9}phQ^IloWX)_x7&I9(3rq&n zkzyAV@-s8viVf+H7C)~qXf=7%BcqW2dwPG|i`*})7SFOHIM6AGLx|R-u~5FNg3`k! zTl30vyF9Dku+Wrz^>uXeo@!IjB+l*{Sreg=V3$9!1^){Ac<LvwZCYEr*?ap$=1F^=!j7W-FKoWM*g@&IPa_kHR1)C>g^5`_OU|^c>u90BW#-$;2-WoZ|hV0@0;5yistd@9Zw?D(%kk+!bJpfmT|Z>jcE>w9ho&un$j z*Jn6<8tJbbRs)#8bE+4I{4r-m6)l-4C{olEG_?*k;P ze76n>Xga1P*C%?t_GfHs4BkLLl-#H+)t_-*T*K=$&O#s-zjSk+3@doPm-qK1EY_g@ zoW4(K5BVr0BU`60BN?1BSXB7njaMMqIKR>Pe6d?-#2o}~9R>~UaUe;XiqnQr*W>AB z>xX^^$y?E0?*52xfgik5U3m74ULJc?Xs{A0!so=G_qkHzp3kLdH9ke5oi60{=A1vb ze{xm~$=g6Lw*UvNLZpj`X8L#9uejt&t*ZuM87{*_GjAq68V-u1!Ft;a_|@NrxG}t{ z6A5-?H(NJVAi$7j zDkSh9{V1Ps8hzHB zqW5_nnx16be&4o;gr{|nCY1(g-YyV}Vxxx+^%JT2hPNwaqqHGv-j$E7D8=X;E(iKj zM`DiuFmU}mvY28r6igBZu%+a+md@?OSMkbn_=Cg_FR<;8ehu&?DBQP?eIvVOdE0M zhVK3-iIgb)Opil6^)_zv#o;CR&wKA*5sW@=ks;^o&0?K+oA<2KGd|qh!HWjHWo7Lm zWBc;u1|KJY5ajX}l8~$4kdZ4kFh(kZqZ<}j{kT}gac8~d65-U__5Nm9K0vLb?oVR= zC(q9hH9-^camr%?@{c&cEUzMHayi8xwwI4|xB0bW_6_n}X zgH_F+uxT0hU$u2lqdVdAS+v+)swTNYE|D*>scNq`V#xz>pmI_PNkezhfqr}MW^=jr zv?3Q1#gft|D>I7jOlv$R26!s>1Chk-qU_?P(w(Oq>c0e>X#CF4vO_{k5mk(%4<(yq zsI8=%U>+3hXXajCg=k%TSZFh;H}j+hd)Xm`C3oTN3c<+mnng(~!)7(#DqPCYb-B>q z%4&(7`POTS)T@=UQrqUjB1DCwZDbNYtJ=YGR6%lU2zRvm6YYbW;m()lo-s=+wPnuU zGx>qG1y{xuJd!&1H#mz*I8~+fW6-Xt{f%_OJwYs$WjpoGx-G;F+=aqaqe z&cq)Bk=6~?IzWHSg+RBFRpsG`Wg+z@#nR5L9L4r@ruM^9%&=GPw0UON$;%gMCtN4mVQo8TGE4vo281=iaA*qwuT?pj1l><1+jq+}r@dPGSI0(>nvi z`_jtu9~dc-jX?_ICbCKmHB)|kXOhc)$L>uHD-&QrSds`+=}wH~8E;Z;=9ZZyJQ~Nl z7GPI<-ock0=jk8wFjpO&Wf-g3j#|54K`w?qyD%0G=2%!W29ZfzrNEMtg8W zrD3>MESoUd=Sk;qLQk-`xa??97R^r91nR}OE)cB8oB`4p`-VbBMC;3C5#$!7^)1c5 ziKjsPAd>Esds3wHE8@%iDE3*$iwplMMtUhqQmm28 zJM1Mv82u9`k3LWxsRw%Z%AMa*e*;O=Ug~0oMp=@6P9gotVm3X;(X>$Uz5mBC!wDY! z1Pv}%&J1p3xx`WHhDG}CbRp=-E?Q=<-1=;7t!-zBg#3YuCy{o!e=_Rq_$Xm}30o{k zcpOr9&91kZ-B0qlH{rttrbEL#Hhb`l4mF7H+$au~g0b`{&yD;ditIi;TTlw+^}u#y z8GWpfHhVHs-50xYg-giu-oPS-o5;SI|6^XW+|_L1*n2-iv5ME?Gu=gPC9?1DL8Y}q zg9fuNyJgBtki6j<-t~S+Gct-d_LMZ%d+<&)5(^bew_i|+GW)q2Jaax=aa9bz%DB5BTb;h=y(gZ=dJ>nZ5%Fv+kCVs-g;=aP7$j=>Qrce} zJ`Qqb`H@C0#|n^1*1(Nu*B-P5wj3Ykp2SKQ>^Rql!!p3;iLX}`@gZ>P1LRaf65kl^ zQ;}5=X?u>qv(Dz6LS=aEo{D9~jZ42IwQ8b+s`o|I27GT@M>$g^U-xB{FDdxpJi3mZQoCWG<>}ahK*9(7`JTt!hby=mj=`^nw(6VeM%{nc zD*REAXW5tykAK${6r_aN2Do#G@!IAol0U5xv{LaoiMaew0S(^4U0nMhSz)UoAMd66 zu;yNVdT$S?!p8jk;MMsM*IxDB@?Dpwc)6&$ed>OimDTwci7^^;ZFf{ejY}AgQzp)t z>aehR>%n-BHYMM7Wee*4HTT_vh>g$U)l^wv$g8E5J38nG#wyo7iy`*T*8VdYJoN2i zCKrl&WM3#1Dw)0?oghl<&z-A)!Eft#O4r1VM?0lGikc33@9b^j-o&q0S9>(35&7(UG8WrJc?aF7@i_RNQgi{K%mS-zRo?Az?HnKyJQ(J zC0d4zZS@79_ETJ@=c~mVDuCc`0z5pNzE4DW|L{ytFKZ7kUys`>3X4k!Nf5EKD`_kL E3vwXoF#rGn literal 0 HcmV?d00001 diff --git a/src/combinatorial-decision-making-and-optimization/module2/img/conflict_graph_example.drawio b/src/combinatorial-decision-making-and-optimization/module2/img/conflict_graph_example.drawio new file mode 100644 index 0000000..e7fc8ef --- /dev/null +++ b/src/combinatorial-decision-making-and-optimization/module2/img/conflict_graph_example.drawio @@ -0,0 +1,84 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex b/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex index 9bccf28..f8d8795 100644 --- a/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex +++ b/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex @@ -104,33 +104,33 @@ A model $\mathcal{M}$ satisfies a formula $\varphi \in \mathbb{F}^\Sigma$ if $\varphi^\mathcal{M} = \texttt{true}$. \item[$\mathbf{\Sigma}$-theory] \marginnote{$\Sigma$-theory} - Possibly infinite set $\mathcal{T}$ of $\Sigma$-models. + Possibly infinite set $\calT$ of $\Sigma$-models. - \item[$\mathbf{\mathcal{T}}$-satisfiability] \marginnote{$\mathcal{T}$-satisfiability} - A formula $\varphi \in \mathbb{F}^\Sigma$ is $\mathcal{T}$-satisfiable if there exists a model $\mathcal{M} \in \mathcal{T}$ that satisfies it. + \item[$\mathbf{\calT}$-satisfiability] \marginnote{$\calT$-satisfiability} + A formula $\varphi \in \mathbb{F}^\Sigma$ is $\calT$-satisfiable if there exists a model $\mathcal{M} \in \calT$ that satisfies it. - \item[$\mathbf{\mathcal{T}}$-consistency] \marginnote{$\mathcal{T}$-consistency} - A set of formulas $\{ \varphi_1, \dots, \varphi_k \} \subseteq \mathbb{F}^\Sigma$ is $\mathcal{T}$-consistent iff - $\varphi_1 \land \dots \land \varphi_k$ is $\mathcal{T}$-satisfiable. + \item[$\mathbf{\calT}$-consistency] \marginnote{$\calT$-consistency} + A set of formulas $\{ \varphi_1, \dots, \varphi_k \} \subseteq \mathbb{F}^\Sigma$ is $\calT$-consistent iff + $\varphi_1 \land \dots \land \varphi_k$ is $\calT$-satisfiable. - \item[$\mathbf{\mathcal{T}}$-entailment] \marginnote{$\mathcal{T}$-entailment} - A set of formulas $\Gamma \subseteq \mathbb{F}^\Sigma$ $\mathcal{T}$-entails a formula $\varphi \in \mathbb{F}^\Sigma$ ($\Gamma \models_\mathcal{T} \varphi$) iff - in every model $\mathcal{M} \in \mathcal{T}$ that satisfies $\Gamma$, $\varphi$ is also satisfied. + \item[$\mathbf{\calT}$-entailment] \marginnote{$\calT$-entailment} + A set of formulas $\Gamma \subseteq \mathbb{F}^\Sigma$ $\calT$-entails a formula $\varphi \in \mathbb{F}^\Sigma$ ($\Gamma \models_\calT \varphi$) iff + in every model $\mathcal{M} \in \calT$ that satisfies $\Gamma$, $\varphi$ is also satisfied. \begin{remark} - $\Gamma$ is $\mathcal{T}$-consistent iff $\Gamma \cancel{\models_\mathcal{T}} \bot$. + $\Gamma$ is $\calT$-consistent iff $\Gamma \cancel{\models_\calT} \bot$. \end{remark} - \item[$\mathbf{\mathcal{T}}$-validity] \marginnote{$\mathcal{T}$-validity} - A formula $\varphi \in \mathbb{F}^\Sigma$ is $\mathcal{T}$-valid iff $\varnothing \models_\mathcal{T} \varphi$. + \item[$\mathbf{\calT}$-validity] \marginnote{$\calT$-validity} + A formula $\varphi \in \mathbb{F}^\Sigma$ is $\calT$-valid iff $\varnothing \models_\calT \varphi$. \begin{remark} - $\varphi$ is $\mathcal{T}$-consistent iff $\lnot\varphi$ is not $\mathcal{T}$-valid. + $\varphi$ is $\calT$-consistent iff $\lnot\varphi$ is not $\calT$-valid. \end{remark} \begin{description} \item[Theory lemma] \marginnote{Theory lemma} - $\mathcal{T}$-valid clause $c = l_1 \vee \dots \vee l_k$. + $\calT$-valid clause $c = l_1 \vee \dots \vee l_k$. \end{description} \item[$\Sigma$-expansion] \marginnote{$\Sigma$-expansion} @@ -142,12 +142,12 @@ \end{itemize} \begin{remark} - Given a $\Sigma$-theory $\mathcal{T}$, we implicitly consider it to be the theory $\mathcal{T}'$ defined as: - \[ \mathcal{T}' = \{ \mathcal{M}' \mid \mathcal{M}' \text{ is an expansion of a $\Sigma$-model } \mathcal{M} \text{ in } \mathcal{T}\} \] + Given a $\Sigma$-theory $\calT$, we implicitly consider it to be the theory $\calT'$ defined as: + \[ \calT' = \{ \mathcal{M}' \mid \mathcal{M}' \text{ is an expansion of a $\Sigma$-model } \mathcal{M} \text{ in } \calT\} \] \end{remark} - \item[Ground $\mathbf{\mathcal{T}}$-satisfiability] \marginnote{Ground $\mathcal{T}$-satisfiability} - Given a $\Sigma$-theory $\mathcal{T}$, determine if a ground formula is $\mathcal{T}$-satisfiable over a $\Sigma$-expansion $\mathcal{T}'$. + \item[Ground $\mathbf{\calT}$-satisfiability] \marginnote{Ground $\calT$-satisfiability} + Given a $\Sigma$-theory $\calT$, determine if a ground formula is $\calT$-satisfiable over a $\Sigma$-expansion $\calT'$. \item[Axiomatically defined theory] \marginnote{Axiomatically defined theory} Given a minimal set of formulas (axioms) $\Lambda \subseteq \mathbb{F}^\Sigma$, @@ -172,7 +172,7 @@ \begin{description} \item[Equality with Uninterpreted Functions theory (EUF)] \marginnote{Equality with Uninterpreted Functions theory (EUF)} - Theory $\mathcal{T}_\text{EUF}$ containing all the possible $\Sigma$-models. + Theory $\calT_\text{EUF}$ containing all the possible $\Sigma$-models. \begin{remark} Also called empty theory as its axiom set is $\varnothing$ (i.e. allows any model). @@ -196,16 +196,16 @@ \begin{description} \item[Presburger arithmetic] - Theory $\mathcal{T}_\mathbb{Z}$ that interprets $\Sigma$-symbols over integers. + Theory $\calT_\mathbb{Z}$ that interprets $\Sigma$-symbols over integers. \begin{itemize} - \item Ground $\mathcal{T}_\mathbb{Z}$-satisfiability is \textbf{NP}-complete. - \item Extended with multiplication, $\mathcal{T}_\mathbb{Z}$-satisfiability becomes undecidable. + \item Ground $\calT_\mathbb{Z}$-satisfiability is \textbf{NP}-complete. + \item Extended with multiplication, $\calT_\mathbb{Z}$-satisfiability becomes undecidable. \end{itemize} \item[Real arithmetic] - Theory $\mathcal{T}_\mathbb{R}$ that interprets $\Sigma$-symbols over reals. + Theory $\calT_\mathbb{R}$ that interprets $\Sigma$-symbols over reals. \begin{itemize} - \item Ground $\mathcal{T}_\mathbb{R}$-satisfiability is in \textbf{P}. - \item Extended with multiplication, $\mathcal{T}_\mathbb{R}$-satisfiability becomes doubly-exponential. + \item Ground $\calT_\mathbb{R}$-satisfiability is in \textbf{P}. + \item Extended with multiplication, $\calT_\mathbb{R}$-satisfiability becomes doubly-exponential. \end{itemize} \end{description} @@ -221,7 +221,7 @@ \item[$\texttt{write}(a, i, v)$] Returns an array $a'$ where the value $v$ is at the index $i$ of $a$. \end{descriptionlist} - The theory $\mathcal{T}_\mathcal{A}$ is the set of all models respecting the following axioms: + The theory $\calT_\mathcal{A}$ is the set of all models respecting the following axioms: \begin{itemize} \item $\forall a\, \forall i\, \forall v: \texttt{read}(\texttt{write}(a, i, v), i) = v$. \item $\forall a\, \forall i\, \forall j\, \forall v: (i \neq j) \Rightarrow \Big( \texttt{read}\big( \texttt{write}(a,i,v), j \big) = \texttt{read}(a, j) \Big)$. @@ -229,12 +229,12 @@ \end{itemize} \begin{remark} - The full $\mathcal{T}_\mathcal{A}$ theory is undecidable but there are decidable fragments. + The full $\calT_\mathcal{A}$ theory is undecidable but there are decidable fragments. \end{remark} \item[Bit-vectors theory] \marginnote{Bit-vectors theory} - Theory $\mathcal{T}_\mathcal{BV}$ with vectors of bits of fixed length as constants and + Theory $\calT_\mathcal{BV}$ with vectors of bits of fixed length as constants and operations such as: \begin{itemize} \item String-like operations (e.g. slicing, concatenation, \dots). @@ -277,8 +277,8 @@ All the information on the formal theory is used from the beginning to encode an \begin{descriptionlist} \item[Equisatisfiability] \marginnote{Equisatisfiability} - Given a $\Sigma$-theory $\mathcal{T}$, two formulas $\varphi$ and $\varphi'$ are equisatisfiable iff: - \[ \varphi \text{ is $\mathcal{T}$-satisfiable } \iff \varphi' \text{ is $\mathcal{T}$-satisfiable } \] + Given a $\Sigma$-theory $\calT$, two formulas $\varphi$ and $\varphi'$ are equisatisfiable iff: + \[ \varphi \text{ is $\calT$-satisfiable } \iff \varphi' \text{ is $\calT$-satisfiable } \] \end{descriptionlist} Eager approaches have the following advantages: @@ -296,7 +296,7 @@ Eager approaches have the following disadvantages: \begin{description} \item[Algorithm] - Given an EUF formula $\varphi$, to determine if it is $\mathcal{T}_\text{EUF}$-satisfiable, + Given an EUF formula $\varphi$, to determine if it is $\calT_\text{EUF}$-satisfiable, the following steps are taken: \begin{enumerate} \item Replace functions and predicates with constant equalities. @@ -350,19 +350,19 @@ On the other hand, the search becomes SAT-driven and not theory-driven. \begin{description} \item[Algorithm] \phantom{} - Let $\mathcal{T}$ be a theory. - Given a conjunction of $\mathcal{T}$-literals $\varphi = \varphi_1 \land \dots \land \varphi_n$, - to determine its $\mathcal{T}$-satisfiability, the following steps are taken: + Let $\calT$ be a theory. + Given a conjunction of $\calT$-literals $\varphi = \varphi_1 \land \dots \land \varphi_n$, + to determine its $\calT$-satisfiability, a generic lazy solver does the following: \begin{enumerate} - \item Each SMT literal $\varphi_i$ is encoded into a SAT literal $l_i$ to form the abstraction $\Phi = \{ l_1, \dots, l_n \} $ of $\varphi$. - \item The $\mathcal{T}$-solver sends $\Phi$ to the SAT-solver. + \item Each SMT literal $\varphi_i$ is encoded (abstracted) into a SAT literal $l_i$ to form the abstraction $\Phi = \{ l_1, \dots, l_n \} $ of $\varphi$. + \item The $\calT$-solver sends $\Phi$ to the SAT-solver. \begin{itemize} - \item If the SAT-solver determines that $\Phi$ is unsatisfiable, then $\varphi$ is $\mathcal{T}$-unsatisfiable. - \item Otherwise, the SAT-solver returns a model (an assignment of the literals, possible partial) $\mathcal{M} = \{ a_1, \dots, a_n \}$. + \item If the SAT-solver determines that $\Phi$ is unsatisfiable, then $\varphi$ is $\calT$-unsatisfiable. + \item Otherwise, the SAT-solver returns a model $\mathcal{M} = \{ a_1, \dots, a_n \}$ (an assignment of the literals, possibly partial). \end{itemize} - \item The $\mathcal{T}$-solver determines if $\mathcal{M}$ is $\mathcal{T}$-consistent. + \item The $\calT$-solver determines if $\mathcal{M}$ is $\calT$-consistent. \begin{itemize} - \item If it is, then $\varphi$ is $\mathcal{T}$-satisfiable. + \item If it is, then $\varphi$ is $\calT$-satisfiable. \item Otherwise, update $\Phi = \Phi \cup \lnot \mathcal{M}$ and go to Point 2. \end{itemize} \end{enumerate} @@ -384,38 +384,194 @@ On the other hand, the search becomes SAT-driven and not theory-driven. \end{gather*} Therefore, $\Phi = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4 \}$ - \item The $\mathcal{T}$-solver sends $\Phi$ to the SAT-solver. + \item The $\calT$-solver sends $\Phi$ to the SAT-solver. Let's say that it return $\mathcal{M} = \{ l_1, \lnot l_2, \lnot l_4 \}$. - \item The $\mathcal{T}$-solver checks if $\mathcal{M}$ is consistent. Let's say it is not. + \item The $\calT$-solver checks if $\mathcal{M}$ is consistent. Let's say it is not. Let $\Phi' = \Phi \cup \lnot \mathcal{M} = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4, (\lnot l_1 \vee l_2 \vee l_4) \}$. - \item The $\mathcal{T}$-solver sends $\Phi'$ to the SAT-solver. + \item The $\calT$-solver sends $\Phi'$ to the SAT-solver. Let's say that it return $\mathcal{M}' = \{ l_1, l_2, l_3, \lnot l_4 \}$. - \item The $\mathcal{T}$-solver checks if $\mathcal{M}'$ is consistent. Let's say it is not. + \item The $\calT$-solver checks if $\mathcal{M}'$ is consistent. Let's say it is not. Let $\Phi'' = \Phi' \cup \lnot \mathcal{M}' = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4, (\lnot l_1 \vee l_2 \vee l_4), (\lnot l_1 \vee \lnot l_2 \vee \lnot l_3 \vee l_4) \}$. - \item The $\mathcal{T}$-solver sends $\Phi''$ to the SAT-solver and it detects the unsatisfiability. - Therefore, $\varphi$ is $\mathcal{T}$-unsatisfiable. + \item The $\calT$-solver sends $\Phi''$ to the SAT-solver and it detects the unsatisfiability. + Therefore, $\varphi$ is $\calT$-unsatisfiable. \end{itemize} \end{example} \item[Optimizations] \phantom{} \begin{itemize} - \item Check $\mathcal{T}$-consistency on partial assignments. - \item Given a $\mathcal{T}$-inconsistent assignment $\mu$, - find a smaller $\mathcal{T}$-inconsistent assignment $\eta \subseteq \mu$ and add $\lnot \eta$ to $\Phi$ instead of $\lnot \mu$. - \item When reaching $\mathcal{T}$-inconsistency, backjump to a $\mathcal{T}$-consistent point in the computation. - \end{itemize} - - \item[CDCL($\mathcal{T}$)] \marginnote{CDCL($\mathcal{T}$)} - CDCL for SAT extended with a $\mathcal{T}$-solver. - The $\mathcal{T}$-solver does the following: - \begin{itemize} - \item Checks the $\mathcal{T}$-consistency of a conjunction of literals. - \item Possibly performs deduction of unassigned literals. - \item Explains $\mathcal{T}$-inconsistent assigments. - \item Allows to backtrack. + \item Check $\calT$-consistency on partial assignments. + \item Given a $\calT$-inconsistent assignment $\mu$, + find a smaller $\calT$-inconsistent assignment $\eta \subseteq \mu$ and add $\lnot \eta$ to $\Phi$ instead of $\lnot \mu$. + \item When reaching $\calT$-inconsistency, backjump to a $\calT$-consistent point in the computation. \end{itemize} \end{description} + + + +\section{CDCL($\calT$)} +\marginnote{CDCL($\calT$)} + +Lazy solver based on CDCL for SAT extended with a $\calT$-solver. +The $\calT$-solver does the following: +\begin{itemize} + \item Checks the $\calT$-consistency of a conjunction of literals. + \item Performs deduction of unassigned literals. + \item Explains $\calT$-inconsistent assigments. + \item Allows to backtrack. +\end{itemize} + +\begin{description} + \item[State transition] \marginnote{State transition} + Transition system to describe the reasoning of SAT or SMT solvers. + A transition has form: + \[ (\mu \Vert \varphi) \rightarrow (\mu' \Vert \varphi') \] + where: + \begin{itemize} + \item $\varphi$ and $\varphi'$ are $\calT$-formulas. + \item $\mu$ and $\mu'$ are (partial) boolean assignments to atoms of $\varphi$ and $\varphi'$, respectively. + \item $(\mu \Vert \varphi)$ and $(\mu' \Vert \varphi')$ are states. + \end{itemize} + + \begin{description} + \item[Transition rule] Determine the possible transitions. + + \item[Derivation] Sequence of transitions. + + \item[Initial state] $(\varnothing \Vert \varphi)$. + + \item[$\calT$-consistency] + Given a $\calT$-formula $\varphi$ and a full assignment $\mu$ of $\varphi$, + $\varphi$ is $\calT$-consistent ($\mu \models_{\calT} \varphi$) + if there is a derivation from $(\varnothing \Vert \varphi)$ to $(\mu \Vert \varphi)$. + \end{description} + + \item[$\calT$-propagation] \marginnote{$\calT$-propagation} + Deduce the assignment of an unassigned literal $l$ using some knowledge of the theory. + + \begin{description} + \item[$\calT$-consequence] \marginnote{$\calT$-consequence} + If: + \begin{itemize} + \item $\mu \models_\calT l$, + \item $l$ or $\lnot l$ occur in $\varphi$, + \item $l$ and $\lnot l$ do not occur in $\mu$, + \end{itemize} + then: + \[ (\mu \Vert \varphi) \rightarrow (\mu \cup \{ l \} \Vert \varphi) \] + \end{description} + + \begin{example} + Given the formula $\varphi$: + \[ \big( g(a) = c \big) \land \Big( \big( f(g(a)) \neq f(c) \big) \vee \big( g(a) = d \big) \Big) \land \big( c \neq d \big) \] + A possible derivation for some theory $\calT$ (i.e. $\calT$-propagation are decided arbitrarily) is: + \begin{enumerate} + \item $\varnothing \Vert \varphi$ (initial state). + \item $\varnothing \Vert \varphi \rightarrow \{ l_1 \} \Vert \varphi$ (Unit propagation). + \item $\{ l_1 \} \Vert \varphi \rightarrow \{ l_1, l_2 \} \Vert \varphi$ ($\calT$-propagation). + \item $\{ l_1, l_2 \} \Vert \varphi \rightarrow \{ l_1, l_2, l_3 \} \Vert \varphi$ (Unit propagation). + \item $\{ l_1, l_2, l_3 \} \Vert \varphi \rightarrow \{ l_1, l_2, l_3, l_4 \} \Vert \varphi$ ($\calT$-propagation). + \item $\{ l_1, l_2, l_3, l_4 \} \Vert \varphi \rightarrow \texttt{fail}$ (Failure). + \end{enumerate} + As we are at decision level 0 (as no decision literal has been fixed), we can conclude that $\varphi$ is unsatisfiable. + + \begin{remark} + Unit and theory propagation are alternated (see algorithm description). + \end{remark} + \end{example} + + \item[Algorithm] + Given a $\calT$-formula $\varphi$ and a (partial) $\calT$-assignment $\mu$ (i.e. initial decisions), + CDCL($\calT$) does the following: + \begin{algorithm} + \caption{CDCL($\calT$)} + \begin{lstlisting}[mathescape=true] +def cdclT($\varphi$, $\mu$): + if preprocess($\varphi$, $\mu$) == CONFLICT: return UNSAT + $\varphi^p$, $\mu^p$ = SMT_to_SAT($\varphi$), SMT_to_SAT($\mu$) + level = 0 + $l$ = None + + while True: + status = propagate($\varphi^p$, $\mu^p$, $l$) + if status == SAT: + return SAT_to_SMT($\mu^p$) + elif status == UNSAT: + $\eta^p$, jump_level = analyzeConflict($\varphi^p$, $\mu^p$) + if jump_level < 0: return UNSAT + backjump(jump_level, $\varphi^p \land \lnot\eta^p$, $\mu^p$) + elif status == UNKNOWN: + $l$ = decideNextLiteral($\varphi^p$, $\mu^p$) + level += 1 + \end{lstlisting} + \end{algorithm} + + Where: + \begin{descriptionlist} + \item[\texttt{preprocess}] + Preprocesses $\varphi$ with $\mu$ through operations such as simplifications, $\calT$-specific rewritings, \dots + + \item[\texttt{SMT\_TO\_SAT}] + Provides the boolean abstraction of an SMT formula. + \item[\texttt{SAT\_TO\_SMT}] + Reverses the boolean abstraction of an SMT formula. + + \item[\texttt{propagate}] + Iteratively apply: + \begin{itemize} + \item Unit propagation, + \item $\calT$-consistency check, + \item $\calT$-propagation. + \end{itemize} + Returns \texttt{SAT}, \texttt{UNSAT} or \texttt{UNKNOWN} (when no deductions are possible and there are still free variables). + + \item[\texttt{analyzeConflict}] + Performs conflict analysis: + \begin{itemize} + \item If the conflict is detected by SAT boolean propagation ($\mu^p \land \varphi^p \models_p \bot$), + a boolean conflict set $\eta^p$ is outputted (as in standard CDCL). + \item If the conflict is detected by $\calT$-propatation ($\mu \land \phi \models_\calT \bot$), + a theory conflict $\eta$ is produced and its boolean abstraction $\eta^p$ is outputted. + \end{itemize} + Moreover, the earliest decision level at which a variable of $\eta^p$ is unassigned is returned. + + As in standard CDCL, $\lnot \eta^p$ is added to $\varphi^p$ and the algorithm backjumps to a previous decision level (if possible). + + \item[\texttt{decideNextLiteral}] + Decides the assignment of an unassigned variable (as in standard CDCL). + Theory information might be exploited. + \end{descriptionlist} + + \item[Implication graph] \marginnote{Implication graph} + As in the standard CDCL algorithm, an implication graph is used to explain conflicts. + \begin{descriptionlist} + \item[Nodes] Decisions, derived literals or conflicts. + \item[Edges] If $v$ allows to unit/theory propagate $w$, then there is an edge $v \rightarrow w$. + \end{descriptionlist} +\end{description} + +\begin{example} + Given the $\calT$-formula $\varphi$: + \[ \big( h(a) = h(c) \vee p \big) \land \big( a = b \vee \lnot p \vee a = d \big) \land \big( a \neq d \vee a = b \big) \] + and an initial decision $(c = b) \in \mu$, + CDCL($\calT$) does the following: + \begin{enumerate} + \item As no propagation is possible, the decision $h(a) \neq h(c)$ is added to $\mu$. + \item Unit propagate $p$ due to the clause $\big( h(a) = h(c) \vee p \big)$ and the decision at the previous step. + \item $\calT$-propagate $(a \neq b)$ due to the current assigments: $\{ c = b, h(a) \neq h(c) \} \models_\calT a \neq b$. + \item Unit propagate $(a = d)$ due to the clause $\big( a = b \vee \lnot p \vee a = d \big)$ and the current knowledge base ($p$ and $a \neq b$). + \item There is a conflict between $(a \neq d)$ and $(a = d)$. + \end{enumerate} + + By building the conflict graph, one can identify the 1UIP as the decision $h(a) \neq h(c)$. + \begin{center} + \includegraphics[width=0.35\linewidth]{./img/_conflict_graph_example.pdf} + \end{center} + A cut in front of the 1UIP that separates decision nodes and the conflict node (as in standard CDCL) is made + to obtain the conflict set $\eta = \{ h(a) \neq h(c), c = b \}$. + $\big( (h(a) = h(c)) \vee (c \neq b) \big)$ is added as a clause and the algorithm backjumps at the decision level 0. +\end{example} +