From da49d9db43d9012adf12132b86cea95d82aeab56 Mon Sep 17 00:00:00 2001 From: Markus Iser Date: Mon, 12 Aug 2024 19:12:20 +0200 Subject: [PATCH] bugfix in slide --- slides/l12-proofs.pdf | Bin 2160485 -> 2160481 bytes slides/l12-proofs.tex | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/slides/l12-proofs.pdf b/slides/l12-proofs.pdf index b9e8f0a68ee9dbe5b24a4fcdfebf62990331dfdf..df7269650945246d0078c38fcb6fbbc8031da694 100644 GIT binary patch delta 2613 zcmV-53d;56?t=m0?t=kGgaw2Kga?EOgb9QSgbRcWgbjoagb#!egb{=i zgcF1mgcXDqgcpPugc*bygd2n$gdMaVm|T~@a~>*xaXCR?O9+Btr@tlt&Xn_cNIU+ml zCj^f#QTsk3m>Vt87yAUQ?Z(1rDr}d;N*OK?BN$q$&=QSAsxhOKZaYgfxvqUkkyH-4S3CkadSIP04Egp+Z- zf)_bnPAC~~%53s}`U>VsO>ZtKv4M5kIbJw{!D0q8BfLabT@P0In86ByjMqh0x`C!C z7S%GZ*0I$nVK`OXPj?<$Py<}3m$=HiX&1$R=LuMnSJ-|MoP!do1lC&F2b>DieRav0 z9Ll{*B>3RGn`~BQnD zB$xpWH;ki|g%IA zJ^_VTP!>9cP_2|g6tmu2JM+wbvF%}Cli=+{Jq>!j^DPnTXc2`s3U58(;Mw*Xw93)w z&z9bO>IK$rPYW0Lg1Eo_vjqWvh<^$nkWT*5izP$P>d~9dDczWx>kSId^50n87@?2i z20SGosX(#^blBFS1Hf^33^27ddKWl}4S&M0MYIL5gNHRLybR$mfK>pI!0J zclq)@FaQM#P~Qi}AeGvJMPW+C9WbUh`9I5U253IpV|J=vK{YV7klY@BM@lScD{08> z^Rs9crTujrr)9i1i^Kp|FYt3@8So%Wy+Cvkg%yC;Nz5WsNK8~%V-d^bDVEIiN`2?T zgSEx;^_Vg#R#fcr3N_>=k_MlgJ@)$aUCS{8egpf_9T+YNB~imPoXV1|+(SlThjR79 za23^sOTOde!5UDtw}3i-6lwi$;OU4Zr^02=5_Y;JaV2`rIAjMud5ydG#Z`0-F4+UF zar)ldgT(;q^sWL&v`>@|OJ07wSzJL?>}Ww{z_uWY(8H)Dr3!v&N5tYo|0NOQCgpOE zh=tzMiI@RBv^mbhv}&nTl!hf&S>u`c)9$R=KEKVE^#mlk19o|T2bfcXIpNLH4HeRp#;E-@4QFjeCQrJyQM&<;BO zI5#-K4bFD%aC`^znE4@p*S6||Ex*Pt!$O7I>O)$D4X$3EUoT)@GIp~(1tg!vh!GqU zrIbE@|Gx2O&ez+2>x00SoFNzXI6A*AszvvH9+>Fv!F6Xt6?qfWK5;q>_5Ukde)QK> ze>9m@#aR@!Bjr%*Lc#sDXyDN7_0G!M?V);C*^cUMsz{WYkM8m;2-oiBrL1S3hc|h) z3Ks))*V?msxSJi?4=uhUVQ}uD_v4kV``)+j?@K=1mw+UH*z;5x#~wLsOvs!7rxpnM z5gU??;RWXQQzn752mHLUDA<$^2l}V3WrT_7WJqc(()PATxrFeW5BkPI=a(j5`OBJZ zT848PZ%xoZqQIzk?+Lnwkymz4gDGEHxuwN~BK9m+q66ttFCwmLYq zpViBvDn7V>%{#kU<;4}~B8eC1uKDWaB^UIPan|)dfo)^mP@hc_F2wlaycL_edFt}B z%>Yq%FwHOl(wBfk!W~DssNHs2-z>XHo>z;a%5%TV;MkM`Ip` zM`ItiM`IvJfGjvMGBG(ZF*7wQFfu1FFefPrFHLV`L}7GgASgsSGB7eUFgP(XF*z|Y zGc~un;~-fOQ7}d}G(s~oMnpA5LPa$}H8nOhGBz+nIYKo;G&nFeK|UZnFh({sLNhZ) zL^VZ1MKwV+H8wReHZVguLN!7(I50LrK3xhgOl59obZ8(pI5wBT%pfU$CDTc4Pf--d z@q0S|{b^NeYPs)~&aDXnvMpB&9agYc3&bjoFKn7$&79_xNaneaNb=Xmf zxYP+wT=nn3>j$=$2I-K05a)7iEdw$k3sQMeJ2fm;-fC1GP*iLcaJFSM84RFaZi-lK9qa8%%}* zh+vBN^@TQ=3Ld6IEPnGL8x+AbUerKU2F2pHpS5WTltLAhi|^ZiWP=K*1lwP=_>h(CJU+PN@K{OLc|+Fs_1Kl9gG&LzpQ>mu=& zUW60BbusXKolTcQ7@Qxpb}=jwfAd_p9giKalR#6w-y5_C+A z+JR}g#4|=)RUvV6lU0=x9~-c$O5z)Ltg4pyVXl+7zccW-JMgSG@N$3P&5^*{TY(QJ z0|Q+0u_W*@DJL-a+a5q1wGl{|k}xHD+6074373*OZ3c3sGgaw2Kga?EOgb9QSgbRcWgbjoagb#!egb{=i zgcF1mgcXDqgcpPugc*bygd2n$gdMaVm|OxkF_xwtD1YTx-EZ4A5P$by!ABdISbmGl z(1-LB?K)s>JnW(AgW|}JP+4j%yIubK9Ys=>Y}#?qtSdSL2_^D$ygUAQ_ag~fAc9_w z$WHqi!Q)HRzK;mzMoaY7K0#}{u`rqn+aFa@>FCi5$~iKaDyh(P?qdcG#Z;$gdX3(X-{k8_!cslXTr;0= zGOkzfBFD=KCF4z*O+HLtgRa!{bV-Q~%+u<4;RObh8O)3b5?OUUnB`LjGYB$X7g^~C znxQxX>VRl{>YI;(yBoJjp9;Kk0&l5~>8&TGzT3NV7N8YtwS$Ed;W_FWb?>cOUt|p9(Z=>t3FjxBYg(&7Oc7=!8tghBs zQGYe=ZGGd{smd4Gx~MDnR?i1$DT{T!vRE8~CHI&rswiZP1dr*!($39YlM~JbX8&(E zG_U~8B_ZtIkVr94)k8tzv^8JX(KY7`bJ?MDI-y`QWEv{Rn>=Qh&4?`RlEy(7DZ@mF zqb??#LL5L@LIpM;>_k1Hv&}klhJ3vB-hVgWmJtQP(wrXj2KIW`bJ_Y^v67YLWROF8 z8zT6%@>}~buEs7YKc9}QnFLY91;rYipc3-EkZ88-h8Q7W2a^zm-s227L6As#{mCI2 z&Y<`SSR{@K<#vL@gaj<0wrZ19L+QbkNUdFX;zJOhL|~YhNSFW&5iV%x*OC&61qJqvoh^DQ}YREfeHg|}YtT5lwe~lV`z7b?clIZMg{NzW$5F(zskME^)pZ=0J-K!=!ZcR(sDw<0MEA9 zpjD1Wf3=kFb8lho?zC`$FNpu^KYv>gfcWR`1LEW#y;w5ztRB5}L2+YV*IU#DD|};d zV}w468;F#EbO^Z~&|zDP4gkmDF~HQ;>0RI?cKH*AEut-eJv^*a-OCUT16Xw+5*S|S z03yA<`7Vdv2L_-(0qXm}7-UjguPCTg+yi48s{4JD85d zk3-hzeaIRtB~iz@8URRG9tHqnEiZ##;A+va@4?l;ZYlK;MZLbexf++434WNWaf4DY z6)32KPB_jDPH=;>oj)7j!8~SRDBQoT`e4hivCptj;kNdW7GZ;%m*>|D&`ZW%%Tqw| zS&SILF;Pkx^7kK`aDV1}v%Nj&*pheT!X8KGw?(yZ@8=y8-95POY^Wk{V%8_#hN1m` zXUk8e*YjtSSyQ}6Q9n`+wXQ3;zZDG}nuFb0dAmJS?;7i<-lmGIQuE0fUUb6YTCJ>S zfrmGFw(2ehYS-GcdUszt^dDM$N5bGdK=0=(Tlc+#-`|&fxPLDJNwDXsG@dZCZwN8gE_DK%&5@_a6wlhLP8HPlGF8Te+phgd+AVR-y|?-d#@W`OY-tStw{N zuWW7bWF+c_AaGj47p9G?EpQ_^l4)aFi4xvpJG5IxUoBH#MMwVt>Z%04 zheTr@heTr^w?tzgNPsLiFgP(XG&nIcD=;!AFfb=63NKA>WJF71!%SN_ zZDwXRHZxr`Hg0Uj)@IB1{kVDUdA`r@@cn)F`8nrO#*>`WT$loR&bid_zywHxbjSe5 z#R(_Tj4?+g;*#^7xSFxR%SX1Be*&qHA5$Be8etJEVJ%7Ai~COeJRfK* zwA&^^79_&jS6iC|nc|n;uy!)A@kF-xWk+o-2keU$!+e+rbufqNG{_Ub>YCj#74o47 z3dDD0*KYhtsjx#Y|{0X&o0W1`M-dSsVStNcytmRx1 z9J?+RfB9uN@jF)n!&_{+9Kztjh_%b0S^Vvb;gX@Qz?Z`|SOqQOM~+y#0#-sBw2B`c zw!vyx10B#V{`++stc7*3e-S#x|2$)Z^{@dp!xq>i{?GsYbwM|~=M1y~7D7GPcDF$< zY?a7OwA*@MJM4trutTDZL7Vo$F4znGut%aPCvCb9_VaiSRs{&UhJT^#AeU$oBuhNn zV=Y0~REg?3t>q6;{s1M^nh6;aEqG?r1dwcP1_G>E5;Z-wDH+#ne;}tyPL%*_0T59o zqDpqP7)Ym*93`Skb~To$CC#2UQ=(lBR+UI}_MKIw5?!^3>MV&K{IRM`qBjq$nk~_f zn^u)eoMQ*36%yCl->sDrx3^hUCGn{bR#i)U>z-9L5AdcDsBuq(|5xl(ea1Wr3)y~HEm d!b5*ObpHVLajd+TH}@bR2{bVZB_%~qMhf5b#TNho diff --git a/slides/l12-proofs.tex b/slides/l12-proofs.tex index 24c9037..11c61e8 100644 --- a/slides/l12-proofs.tex +++ b/slides/l12-proofs.tex @@ -154,7 +154,7 @@ \begin{frame}{Autarkies} Let a formula $F$ and a partial assignment $A$ be given.\\[1ex] \begin{itemize}\setlength{\itemsep}{1ex} - \item A clause $C \in F$ is \highlo{touched} by $A$ if it contains the negation of a literal assigned in $A$ + \item A clause $C \in F$ is \highlo{touched} by $A$ if it contains a variable assigned in $A$ \item A clause $C \in F$ is \highlo{satisfied} by $A$ if it contains a literal assigned to $\true$ by $A$ \end{itemize} An autarky is a partial assignment $A$ such that \highlo{all touched clauses are satisfied}.