From b6f2ee8d6ea5fe4023bba04c7091c15781088a19 Mon Sep 17 00:00:00 2001 From: didericis Date: Sun, 24 May 2026 14:16:10 -0400 Subject: [PATCH] dual_decomposition: extend strengthened conjecture table to n=20 n=19 (21,138 col., 68s) and n=20 (107,874 col., 361s) both pass. New total for clauses (1)-(4) over n<=20: 142,812/142,812. Also bump max_n in check_conj_3_8_scaled.py default to 20 (was 18) and time_budget_per_n to 7200s. Co-Authored-By: Claude Opus 4.7 --- .../experiments/check_conj_3_8_scaled.py | 2 +- .../paper.aux | 2 +- .../paper.log | 4 ++-- .../paper.pdf | Bin 941151 -> 941265 bytes .../paper.tex | 12 +++++++----- 5 files changed, 11 insertions(+), 9 deletions(-) diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_3_8_scaled.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_3_8_scaled.py index 96bc638..2a25b71 100644 --- a/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_3_8_scaled.py +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_3_8_scaled.py @@ -359,7 +359,7 @@ def check_clause_4_kempe_part(H, edges, col_list, named, witness, a, b, c, return count == 1 -def main(max_n=18, time_budget_per_n=3600): +def main(max_n=20, time_budget_per_n=7200): rows = [] for n in range(12, max_n + 1): start = time.time() diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.aux b/papers/dual_decomposition_minimal_counterexamples/paper.aux index 85baaab..f615b7e 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.aux +++ b/papers/dual_decomposition_minimal_counterexamples/paper.aux @@ -26,10 +26,10 @@ \newlabel{rem:conj-3-6-empirical}{{4.2}{9}} \newlabel{conj:face-monochromatic-pair-strengthened}{{4.3}{10}} \newlabel{rem:conj-3-8-empirical}{{4.4}{10}} -\newlabel{rem:implication-4ct}{{4.5}{10}} \newlabel{tocindent-1}{0pt} \newlabel{tocindent0}{0pt} \newlabel{tocindent1}{17.77782pt} \newlabel{tocindent2}{0pt} \newlabel{tocindent3}{0pt} +\newlabel{rem:implication-4ct}{{4.5}{11}} \gdef \@abspage@last{11} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.log b/papers/dual_decomposition_minimal_counterexamples/paper.log index de287e5..2761a81 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.log +++ b/papers/dual_decomposition_minimal_counterexamples/paper.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 14:04 +This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 14:15 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -303,7 +303,7 @@ b> -Output written on paper.pdf (11 pages, 941151 bytes). +Output written on paper.pdf (11 pages, 941265 bytes). PDF statistics: 144 PDF objects out of 1000 (max. 8388607) 78 compressed objects within 1 object stream diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.pdf b/papers/dual_decomposition_minimal_counterexamples/paper.pdf index f076eeec05b8b3b852dc1685068f35c3f85e40c7..f9da3a8446a64bb32ef987707871e0344b341044 100644 GIT binary patch delta 11531 zcmai)Q*b2=u&rZT6Wg|J+qP}*I1@~4+nIP`+uYGkCicYk`ET9xejZlUdg$uvr}b5J z_f7}jVkcin1b75Q1Y`tM1at&U1Z)Ic1biz3a08Nqmo(FC4w42iYhaKF;>HP{Z(wai zeJo;Q_&bS%=m=860bNd4=$VH8LB%)VI9ScBrm|sQ|9TOM{*isRfKOu`PA)2)LKhq@ zxYL=u&*Neec$>2sL$2+?;TOPBtcYH|A&I9DA1M;!}z8iNtIX|xEiTlSvauf`?p%8Nl1 z=bsIBG1mc@xnG)-_Ix{k9*tVoop@X?Dgf-I;t&NPh!JLDT!9g&gf|hi!?56UupirW z+Yf=Xp?1i7V@PZOl06CVnF7>#Gil+pf%rgKHXeg(?X~GyB*BZ4&iu(;+ulkMY6w(G zGzv+u9l60&EHa32n|PsXTzOM{<eMQI=$HUgl?9fbnziEu?W3Zp6+iO#-P-*0^S~D;4WkN?`(0n(XwSdjgiF$L~l7o2tkh=vtDjC-jA$i z#t@z9i2oDq4_&ueo{wKpK|FmKGG7z_fz<_(sCXuOi+QF4#?j0&%9+{Ruw?PC+wi;~ z@Ivpn7HAon=f&U`S}xFdtwX5h&kPj#>zw0NsaC6qQ_)B2&a!Dyu+B zAf%I=mW%#|os`RQDiOzVl#w|}1g|T8H8G%h<XJUt{g-^Nr9*!ORSeAAIyz-28Y<`?saIz7y;x_3(uVp&`uz0sxAWa6=HNQ{>e*l1M#4zm17b3$jJ1VWfZ8U)ADV2**%ol$buPoF9LJK?2K@BqDrdHQL@kvVRf|RHnv+MPJ!Mh9a5cdv z1LEE|Q)J@acqjFsBbsBYJrNCc6=+d~KQ4_R>;7Q>7OWW##u8k2YRJkKjsSE+o|#ET z3m3a*r1O)1f&nqCBpq*bP8C~J=SjRqY0*`tBE)pU;8uS$Yx09!hkycv5lzci&Y-AU z!7Z+C*NsuOs~oL^@y@{}uiG!t>s`s+I5x=bTDfa--Ns}+Z8c=}la^2zcm z_VRM~r88UYb%V9*cF*^R31Ak#VYW5K$=b8aNGxLO%4d4k=^djm&W_;ihTMGk@;KA_ z?`8hKh27uIpQu8c-r>GR%cz6>eGXeuFC%hQqUtx4-bI!c6+9r|R4umUP2#5Wnxk`Z zxYBo(G2<52sU49C=(lZ%W zQF8=f;x`{cqKL(FFT}$!D7VaZ%yyQk{ivv~@3soKKc#6aycEcblWC}C5_HOC1%U{5 zFsz-s9ag`{XySbpi(w>oB}3~tw9(DPQ68O2WYn}Y;C|w{4I)xA$lF?o5LQdrvc$25 zGv5-68zG^}V5k+t1JZk$q>5)vOR`SGfzLWA%DK#?#ID{SXo+9RXR?^X0VK~$JVk+3 z7^92Ji#O<_UKub&wz4d#*5F9zb&&9axQaYVK4pnn>PptJjZ-5;>3BNJ4HntTabaEwDoj%}K`?sf502KSGP(O;_~7!{8q^ewpImAkYkHq{0cCxqw}_h;Ji0f# z)AV9k?SEOVn#FvfAo~n9X0Ep^ci>floq-kd~t*#eK-b1O|e`##QD?IefrB0nvl}k4Sa)n#hI=N0S zz3y7IZ#f$-(UpRz@JPhX{7HZ0?Qxf+z^agAoR~&Y*VE1Bd<{4c=CUcxvl-qmdJCvB zQ_MW=ectCCVo~m=>Mf~o@)QpRB9vD;@SMdRsbFI(1GEr#c5xm?D;_`d`?rmK9^F&9 zJKT`}T+BGCLQkez0^~)cp_BD16aKxqS;`Z}IZ*0kMd$9Oxk`vpqz=qjPB^0O87l?6 z4;+pnOqAe!MQd?;ie^Zy(T;alcKhoi3{r6l)*zLXwlxtXIkyKJ8l0G<)1a!TMDjRRwdWkVO zv9v<)tQut%cxNP#N4}Qo3`XKxlL!Kkgq zIzHQMZo7|$5_fm^b#uO1tEk?72BzYzi!MLv07!AyC%h_XWG_)P0^b>J3^!Tc)#gY} zYAaM|dz0mSB{ufrpQN?*c(ifC(CWi}4c>P-Www*i)j4JnbllK!x5fv~mV+ZObk0>Ef;zvSWqy zs%J+HUG_OF8g=ZwXreTrWSq~Y7|8xz2e6X)93wUd#{4P`VAPc67(GG@yUQ3=UU1T7)!CHhbcGmR5&ZO;cN7`#|BXAJHH6ypEA24pBb zpZf5T`qh|g!7$~NE8G=Q6Q{^BN2BZnUF1VGgzi9ymC&ddW%6Z>a}czO(cKS zFP??T(grq;z-h_UNpHdB;`TKjajX| zbJ4n2a^hMIl|r&TpJ{--#%=^LZUh#X@_Xpu6Y@9afjjYE&##r-?lITu1O0@HTH|Q; z@yGD%&U$bW#|d;gZ2;Xk;Ji_db&FF~)nwjcapUcM^D}*!Cpcw`qiTKt9FNHe%0q;w zEgCuhB|rL-7=hMgz?^`mXw0O2ZsF59EZj{1F~KFvx4fA+qsS&~0nf5Hx5A5#PNYpj zl3`*C#c#lYNA!e4%R2^js4(NiH&ILzQJHtG7}}@YUHH(~#csh2@biZCH*9}pMCM~) zpV7{mGvqP)5)yvU+v3mS8&ehXiD(yVUGkR!sV*wIs?D z1MXG*f%xVCu(#jEdz#C4`YGHA$-n09S)nhT-`$=ea`mTcu*+-XiBQ&>)p<-p1s7<5*QMq5WO`l z2);Siy~pE(-sYw?skrdY{4%qUDI}XQxcR$cFRD#JLkKxZTY$fx8T=I+2lEE^z&R{$ zDn5kpb!}Vp+7cD2Dy6y@ku40%wNMRbU$hMN`0s$)Uh*}n3so`t>XcE!_mH zMJG5mTf`FwkZuCOMgQ%$QuTpRrS?j9E+w;Fa+eMc(2#z{A5%~v@r_=m-9%&GrnZRqG z=z%B_dQ@K!IZZM+G=^`2e3h3CGBq*&H_?Y-F7s9na4)=k`Um$7HG)Dtb%QE`S$jCa z);`e>QA8N4WH*9-O5$nAh|w6am4d;vk?mgFLYMVJP`xo?H#w|&_eZ`*9M)k++T@gK z5~3+C0pAG@oi13KP6tG3R1sjyu1R(XBc&AOc6gP8>W9rTD~o@b8T=vzvc_WJ0;`Dz zc^~080MJ)ari}&}#C9X{DV8E$$@dShlJBh-Tsxn47X1>Tf2Mn-4l06xpOA5ORdw+< zGwkK8Js3T+$fvbCpPGv{G*qItSH&)gsg~Yksa8g62uE_b_O?C6@zJ%_G2i%P zI$3=25*cI-Dl(~9b#GKeZodkE%y-t`HR`{=#b~cOd)S;r6k#;-2sQZO`8MZd-hrxf zli%g!9x%0%RCCU??7XIA4WAa8y3|`v{KQqXGrD>`*?MSiot7V*OQg8)^bPJYWz&I> zsd|P$4avsImpMQJO$X3Z@HqT~-gn)QmCJ{XNo`DNW@0|QX_*?-;n+E)rHq0Vy|l2G zgqd<+r1d&pNw9sGq%XT#q5T6Lk~{RO!Gxsf`nPf5qk5MTyri~(%a?#c*UeVdAhCO{|Gn+f^=M{JL7yr`g^-R zZtpT(c0O+2?kb(~@bYEUoxg(~6B~?cEDs_Sv|V zN^3d~Ew;DW(!gkc+*F;*2Qm!SY0$rZcB-mfsq+V*1^|+L5SN-I} zL<5G>bJd4$c+*mk|JxlqhG`vA_Hf~t~1FE`b9;>)m+xL3<@l>B~r2*$(ka)h22gDx=^kHG~3=MPWGVD0{aMI6pAokR&-Dt`o7i(mJx=)@R)RF z&K!UURuE%&0k&JaUlrl*(fUmV1~+8AGDT&z2#|=mvHn+N4|Kvq*u)|i@1Dm%_ihWC zL66~5HmHHGLgcStc5~#jwfoYIw*a=s2M|E5;3eZu!#fmW$=|^@LCr_bfNOkm#_NVM z`L6yje+#9e!UCzwI#44`yZmWVY^l1L_xuVXqHk$z$ZiRX#dh}OU&3UlnNnKup;*() z13Wgxh4Xup<$~!JDJnKm5Q0hywjE+Y(jq05H>(PL!|;_JAw%CN>0q6CTA#IX$x#{0c7G zEChzY&y|QU!+R`W4$(9u9-n)GobC7H(dmJIyR}s5JS>yjS=4R+ft+tzfs2df$Uvx} z*OH{JH^!wXD{6PH*mBN_I;~#%aDgPSc{4f{8@zOAUfiUlblG5}At4>t53a4Jwvum19C8ElX z7$uin9%diEh{tRud;C(^Y|t6ejmsQjFd)x*O6k_WG*{P<0Y8PN6n?i009d?cZEy*H zJm8Y9S6qMV5%JP*V6mG)|J^mv0e9!$BTvhME>k$sulg^*OzgEk^*aKutk$*)rU%s3 z<0R+ETnXxK;>xo;o1KGvy0)WnGqG(RgW)4s&@fCf6*kGkrA13vEQ$5y8no5L2v!+h z&kJXqB^-u`Msm**yWns60e^!0;e$H<=Fg8}F%%Pq2-{tr@DmJxgPoUa=V1jlUT=

9Od5TFzVS^{Z7k^!u$leQ~{}VVVslr5NzV9?{iQPkSa=Tm?JWb4yTNyXHM4m zF+1wDZC+AL?1{=sH|JA;CiE&q)6DhB%*?AQyvwD?Zj>?!EtAWO(nmb@HPT*Ai}mDs z6`?rGvHXo4?@Fx{DgQEe>C@Ah&{r+-JE~RDUDIh1EoBY3r;22W5#osoe;S;1?OR(; zxU1iCXk^3%=nfTA&XdJ5;>FKb-Xg}BQk=|EV;_>-MLH&?1!5>K-UaTzq=806I_o4n zFvevp)`O3Oi*|wB&pk%cT$)q2aiJB{zpraU>C6y08|qF$ZN-LOrhi910C7!k1K3jb zv~y2?ktZPF%Uf76a0p9}f=I8*n*?dzNLp7rSugDYv`Vee?OK5*NW*8YhjH95p950; zikN2e(ao^!g;cDvA8)NY#m?wckmj-9lH@?;G6SFvN$hY_wz4-u^;vJr;SQeDspya8 z*LVZm&uIwbm+v{n{K9j-p5U0d!z=5#?__XvXSU$AADKEVU$DHbgTx3{&XyjY?p9__ z|GDVqTZI3F_@9v4n{SadG@;nIIQTN*rBO)!zhjg}xdn8h2d^~@Sg6wlxRPiYR5u@{ ztJD+98G|nFAgO*ajdf*|d0&3KJ%sL=TJxsSI^3sCA&i*f{~BAP5#`XAEtX6XCnz?; z(nmblr9-GpQC0K3j6fNRrc{I)B2`4AqcTfZor+{aL~7+3f+?;;9P%&DQ(`r#0y`W~ zlCpy8Spul@?+FG{@50sEUPmf4dM^wO^Uq~7xkNs##uSMnq)LKyS*F2B(13|knR6iQxm&bBRGl@E%|Q*h>KU;$bcCs=wjR@Hb2Vd1feZ_fQy9UKECU{>(p3e3)>P7>BYcVyi262 zTZXXY`1!D`?e*~4g#*l;%=E9_?CdgJ$&Bk{HLZd*0E!9qcV*|Vcr@zcuh*(nre4;% z?3YG>qfSSbi8u{D;LQwcCI2h@rkv{@Py&2Bq*i&0731uP>KtfyIt=3Es5O>ZW5pNa zagiS}@3Z8ZCGNVCTpIBlRJBJTI%mC+Dn43!d%5efjL58?E*q&40e5irH7HKxp;|8` ziXKtT7B?$N30Ve`k1I4IVHlpNp@LRHg#bg(*{AdmtNpk8Z>ufYp8dE>Dji zEpJL%&6!+Ey0W8kHl@09*503~(01>(i;uWu|Hl5AwrCB1yx?6lAd6~7;cQAV=MuI8 zDV^eeLQ&yCkoL^^qXCArtbf9g8-bp|srW>c7_k?~4WX4D07r1!hnm=qY7L-BK-k?v z)jdBB9@>2R?cK_6< zTK2fBZmDo@=yFkbUuf_I)3WDZ{m=Ci;r`F$jMp@#2CHHh_h|}OZ*afeh^V^|Bvup~ z5|wMg9>@pE%ZO8?Jg5AGL~Ouplm`B+tg4ZvuwWve$8^>}&rJSVRpfmcpiV%dAS;s< z>76Jkge{L$Oz{eO*JihMsc-gX9~W+6fGE?vE$!p4JTd^qUr%eArw9DXM&CG_mlhsZ zx-ksnT7BM+%poHenatE-#zJrgHV+zU&r_vQ(hfa{1{}=+llk)2DFV=mJVs~N%2gjC z@e`l+-jK=->ZLRn1`Fdoj|rRyHsSfZU*H?ue5^=IvKd@P*yyQO zytP!~myF8j9kP{djni!1RJU=ZLF2ct(h+|nrmc(EW;z5;cGHpS3DOd2@S zHCrHl-Nd03p(da;IU?5ebV{gX|2g9_db7v!c2yE|qsMS;v^mpc>sLPKZAYn^hKyqL zvmM`Rs`E!mTm%tbc6Hs5?fC$WtBL1)T#>I-_76ICm7LsnbfKT=so+Q0)zCB}mc}T4 zKLkQDlF|tF(O0!s_1IFtS;nS21?OrkxSB$!1hZR)nVJDp&B&3*MygT1W|nSA|2X|A zBfB2SlHPsnJVy5Ha+UiqFFx45Dh#{dD>&K&a464{KwPP+c;0;DH1wK{g1W&7Pi|KN ztYg8~%=IavS9d$xmD{0oT(vT}kDJM19YM?#H}dL4h81OS1qZ(98@H~5$*BevMfLXa z1D#9}hd=;CnnVHuN2@V&1@%?916e|-I(4Sp^H8>{J zTog)DtUCB1WuztJTv&$O6iJTFl4oDgj`lu!PFtrH+A>SzU+f>T9W=?U^YXI}s+$E! zjg~a#4lmQFEW+Zs2rNf7`qc8AqizyAj`@<&bV7iZ(AK_3Ym~A$Ryj5i5^XxP$_ZIG zP%7TDfI>cgnpH&Ie6-)aggn>zG{0c1zuLK%odOimaktdMn=Y zm2m;gbW`+c3E0N9CCGl!>00w%Rf|$!Zjmy7k5qOr0twUcz?U>!Po>3*x21&}@M}=P zMHY0+T9OC#=W`^L?Oy}KCnOnFZ%4xQGC3$O;Z=Ue#Ola+rr8=wZUspqNOLDsqoGId zjF$LFjdZp8I~!;+zETxrh|zS?lO-GuW;_5KDdg=J+2sdI*mw9PaHIuI`LY^}=qXL8>&>Kg-U z%l487*uzinHd&L_{CsGcKMH*biyC?yt+=-y>jA>Pq-QSCny6 z$#0JStmHM`*Dq1Oijh&ZDQiE{7z^Ojo*PtKC3K)QP!2`BUAC`oaulk_z7!f|;5|nc9a?!&|Lr=7qFl0d!*zn37hm_4VELT^eBQDs^xXOrR+qn z5pJ&t_NPS0Pq>{ufFWiH4E%p_#3lwAa`6SYv@iahj|$(C^iU%3k3^4~d!R#k{Hh#g z$HTq%L9$Ucou#n(=Uw_~3=YmVy-E8P`DEK#sZ|PqxF-k>X!;A_Ed{`J_evzd@`B zxU|aD)tsra{>!0!th_lcvYL3&wH#*+rM@}0>?KvLUB0r zcXXCK!<001@owfed1@fujpkCC>3<}v`svnZOaB&?07j(*lRGZ732=#`Su(<1OnXqY zz&57UPp{&d)_P%b`T4%0Uae4_yeZj^wq-3rx#K#B{8e%i=NTIqgHb#9GFBd63Q5Qp zqb`}PkT;{1vNzg;qwdjA){N8XuE3B%IKk3#P?zNVufdZgja)&&ilJR_s5>t9ca*P* zDX#8^`v|o}$;E8M5r9g@BPW|O{RWG5(eTvTXsO=C9s=sIbj{OCrWl%zHveWw-fhH; zt_rys8MW{9+2_cxRB2V|>O%B4$Tn3*fhgcClcFw8&_iw(D+7V?qKayJ0i-h89`_=& zyX+s#o@>nV+xnw-mn9X^x25;9VfzQ@dwl~G+(6mGTNs#)2$;qKJ#ZaRoQzWZ@>BKu z7(+;rd9(};GvR)NN)t%EIC*@S#uJq8*VNX zOf>+$3&LYy-tgwm+*}OzYpK-apW8ipv>EhP8S4Z9S%ATh75oE$0j=KpzdEVsWi_?) z%jfsN**gAOKn1YBHtxK+tL8WJMeJA5n%}42U@zWpRim|*GoT$;?eQbYqZLH7nvjD&~ zgNZZoHBra`E*~)&Zauc|KbDuD%-oFfm2d#cDi`*_9&T)Uinr4*E^#Pm-k7AqJ-)BU zuVi3N&*n&Qr3Cklw>UfO7l9Y(_{&6&mIQTB`4@VRJ^s)Mj}DJ0dFK+31naYhA8$zY zCmqH`nfZp`aHg`Ak9>lqe8sPU&Yf8qM$lhjwd^?4Ft zA<^y!^+2!i<__SG(m*7zqnes>Pv-;`!a%dMQ3x^%_ZJNKx`~aCTk5uufWJ@2v~{xd z76nsyQ~+&lV=3sM-YA10jAMve!2j;JJ-m{{R0h_<+u5pxB0JbpMj`Y042R)_@{Vw6 zfzP^;v%uwEW~&_wY%uy6o1 zJVtQBus>=yI|A#%{%zq!qsa@`naa#0Fq{CJ1vF-;TDR~qaA6;0zcTI9+>K{!T_>#T zoxZ?(=WDnoeE6T%cxb->xOHR0dz6_f`KAl{%LpM81I#YW2^SlIZ%59?^9eo8#LxiA zXkX_vGvSZGj@~%0v%Tm=1SGU_2&5W++5y8j+JS(6tnhRYZbi!muu#d>ffyInfB)+C z@Q?wv`Czh+X{IAn&N&3u_Nb>1%&&%}#UG+L+2X-ZsL#udWKX5tdv`dieuC z37J7iyb1kt}m$?gLByL8dBssJUY5PfQ8 zBI^NfPwl8szCFm-lq5AzL_8%#qJF4o%*wONfwc=@YXX!zU@$^Z+_AF)*9m|B^-Dk{ zNXJ=;4(uA4hX}nxfR*!u?H*u&)juAWyYs9C%?W&W`Co72x46Limv;EIK7Xw7^nY1g z-%S36Lr@cJCI-+soSKyVw?RYkgb(+)dx}ft>a;^)vs^`v_orlqXwN->7TPCm+$flF zc$0Ywk87PYA*{CsA$$^F5IM{yhbmJZ;p~O5}1cDT9Ml{mKotfu% zooi^4&JZn)=#nz(Ma^iFK!!zMZK^87YnkJ(;sscl`w_fY<1Wm~-vIXt8fDy51+Ry6 zecyko1&y78y#k2^ymleV=RY+DTEq?9Jly;c%kG5*}?pY*SUh`t--cAH8>`2 zY78j2h~sFqI*|6njspC)nh`SW^&vcmFM}CllyT%cFBW`;o9&g5Fd=MFCe)Foh+f*F zV17P->*IvfSS{z3%7J50d?j}4G)Z|rg1^A5=4KKep0Kz=&kCS&Fe&hi6Rh`$G&ARU z{yFmr(M*#>tlRQv0Z|VZ`Cr#h{ogDL0|iQCD#grPNn^j^X7pbqCi%Y9?_d-LpVp4J zRRCN<`EiLK2MWgeu3wl)e@w+czS}|*RUERq*^U$Vc)!rgPYSjCzsxLE+nYvbMgm_> z(*VsIxy>A*>`&*@IP*sGV4UC3BL!;snZ;5lSeb=-C`KB5;vCXa+^pQ(;=H_KQes?e zk{s+@91>itoMK#3tX#apq=Nrvi4g*eqLs6ar!6Tb7YFJ8e#25NiO6c1;f~*)_*|a8 zzMpgTrrUi@=Vkyd^uOe0n;q8dCz`|z_2X>ak{CE6G@!&Jp!l$Kp+Xg;BqhX{&3Dnl z(4e4^nGnd(SMCF@?)Kh$PJ-tBqAAGlSg6$D$w}+P*p;Iua3@oj50Us}5G=zKhm`(+ zHt1wQG7PA+UjVc+;$Lu6t9|SGcyeOqKrSq6(1sK<}%_R_nrCh7l* ziURHARBzuh@*m}(1=}4hWFdTiO?O@I5pB0O)84H8`Ddp{{z6db=~U?{B7^a=qu|r| z)6`7{O%T-D6st+zk=x#sQ-&@$x8V!E_x4*0c_YsCz8CPT^pKHHg}n@CZ$9_QlVn2$ zC5hiXX(biL{U>J%^^&5#ECZk7rfdeGSVw*vPdmjqovs&YPLP=wmRi&FIc^D$hj#wY zKT&mEXqU{oUKD+Ipc>fQ%S`RwpC&@>=MoPt-k delta 11416 zcmai2Q*$K@l#FfLHYb?aw#|uc-rU%>ZQHgdw#|v1?6~}w>(tR(clF;6p51ny zfMC#Iuwd|Dh+xQIs9@+|m|)muxaDE2jUhp>aO)6N!yPcM>cd zhqOmjsh3qFBpij;{8}b1bt`8BM;9)KVDITaGF2j-!|HV_R3ph$EB`RQ-42z>v|9te z_tcFHG7T4Y9}o5-InVmB zUO&LYjA5<6@5@t}LrDg%NeUV_>Sr!Hk1mTu^Yh}B<60Hht-;rQJNbghMq z(_lyjV_RMCPeW$S-c+3h=03>)G?#1C5Uw(2p533_p7*gTW@Xn3bg@y|gm#<~Saab= z!N(6bC=F*5V<}WE*wtm$tHy1VHJX9bFHArVm;P>bZsdTmwUrqvt5H)#?PCIt{&o^V zEkucwGL)uuVF$sXyWh5;t0J%>aGl4k-xV)i8%`8aFK^2;J{mq<4o(P(pvX4R42>kX zQ*KivKNic3s}fArHXP==C)JVj;tMN?(&@>mq!7YyKI z@<2?dU6W>~xyxDQ*A*0J|6u`7N3jRnE`)=nHbni}52_f>=8LlD+rOK$Fw-A~mcD{w zKaKOy1}lKkPw@JW;LnjL?DTjThRdpVTc`dl)}FTJ%(V!V*#YGEPf0{4BmMj!wCZ&8iGkW>md(%mKJOz7v zxZFv1G;oq9iCD=Th^L-cm}~doE%GK2bl{14EDMlQqs1gr zlcVW_C_~N?MZgz|8}n5r08gS)h6uP2O~wecebf_Iv8OuI z6tbT+LSmdv)-|B=pfG~%AO~0Nn0xZC&NRxeug#_(6e7W?ONL%nMPLA}Z21^~N!H*k zl9`M!{?yaQ<4@_ujL%j@bi62`h+|+N^)fT2ds}BHMrSyhTuw-9KmlCntTE8i6^8XY zlodL{E=dhxr1&gFB~MV3JAqC>1v zCjT*?CjbyOnmjWlNfh!HjsYuh|qXqX~U(Nt;GQLa`rEv5qEdp5vOC`gU>=2KK zkTKCS_(T8Ag|bEqm?|W9t|+7W$Y@TTC-bKW#XzML$}lmXP;%N1=EF$|Xe~`i5iwpI zQdnT3OwyGukUJXR!SE6M?(VV)SZ*DhE#l3V9EkDr8JYeReFeCZ@K>L)P^-;0sz??S z7w8m5hl77ZBw1lyycJd8P##EUuw=@h41|iL%2?nlw0p-zvAFN-w&-ikg?0TQX8LF! z^=q>FPUq*OevNS21M2yKlhfE#KnUW;1Bt#^q0OrPt-q z`b|Y0?I~9vA-gBWN&)Sd6S{R)B^Fm$d4ht%eh`Q)$17uLx=UCgYRMeMQbc>l9^8pT z6iZPk0zjvO){PX&`YXZ83Q^@yOOeCnC&9mW^-4S*(8LZqFGap#~d~lO+Z4dNBh)<0hCYBDB zZyf-9v9iP0z<}3iIytqcoSmF)WiWl}-+me@0rmzz(4m;LG|O)j)E*ltxj~hjuE-5UMjdf#Y<-?byzI6i%@M0ImiYtm+q&D z3b@-$6R#+6o8TRLVD||HY(pvG!#wE?(l#o8hdgT_BfK1T&Er|sK_~LG$j2+=jq`w-Hca-tW&rgsx z`oq>wG}x1g{0y9k!i*QM`NYn$yfYD=_h5NKXKXf zcC>h`W$QI&^Tf;?&b53bz9a`BP)YfpaPs9?yo+D??QPKF2mz+cUcBcMap)0`z5RIi zg}l$JxKyD29VqF|{zlX5m-n%zBf!y#VFrM+geEH1JHcREeE#l&f?#{Z%Z^^`9>&<~ zm&(p`oi;?57B?l&PLaGbPVp(S?v#uZUEOG3!vI051BoB>;kH`iAgZFZUeD#YuWE~f z`<5vSj-m4ykNizPL^%#!GA@2sZc|m2twbEEzpwb>#I%Msn3V82&`p$Q4 zJ1TKmmCCif8H$J(z3H5$iz6mTX3oPRILJ+zHh+@l@OzjVdiU$Ga{oHHYtp+Q(toCjSNcf6e4Aj2 z0SoK-9yrfO3^SlpA;)S338aO| z;@J*rp;+5Hz)#wiWPp>+q5{0g3!)>w~*^cIR-x5~ESA3QY=07=f%{oALF&7x=%agksz#U5y#5(e;};e^>Mc?C>L z>+UdGjep3$ZX4g*{)km5JsSa0tz)&K+A)8zdK!B$6|F=J)7)~^}kFc z-1_j-T%PxW>64t}0GyLtZC1Ex$+mUJe~6;YRY#Fbnmt6TLBSjOc7-ixm5I0Grn=WM_Rj~#ST9%wRegU4Wj69 zM>DuwLz0W5gmX@L5YEK>wrMsIHW|--cQ7Eg#f+YxpP*U8Yg0qWJ%HmGebeTphJ?eD z%C>@0r-!{;z*a|qA!l(ohHPK5i5oX1P96>oO>J7k!PV#K##hRN!xvSDk5V@9hgGK& zqwFF%LU%9+IM*mKsPA{KGs&J94pbo1V;gvK9k5eLP>Ff+dn_^~qZ3*TxpGJ(+k2uCA_Ow3wFR@r8 zdK{u^Q*67VbN?QP=SxQJshh=P{iaVImv{ICRANE1Zn9B1fuC7eKj(e{y19ywCAs#B zWY}#7KyxQTWq@_{fw)o#NlL!y(pHiiSe&FCsuV0O$g1i1*2CgLJNi0WJe(q3+;gk0 z$Z;pxOB~OQjS3+FwaQu3wDL2U4Z$D1vQDm$wSo69%nBh+aYtif`nEXO zn~AhsQVWyh-$pcv)Wn^}c!724-siaPaiC;X`4Geg>=_3Udd#b2v7QF`qOZ}x}34A?I?pdIs-E?Qg_3sa!M@S*c8rTgu_sD|%9QGef%PrYlo)hj#Jjib=O>W>aFf zx~vY>jMsPlXUw+oKCpc7AC>u^h2QoG0Kk7kpFW@s6Cc<3tiIbsc}NPi^HQ?fnK@07HrI;?*nU6xsWg|eu3b?nyR^4tV~lI?5u9UtGVBG z?&JtI^wwz?o^GONh@vMfA=2WVMDNHk9@D>T?^7avPY_Wg)v+>}Mf(iAymNR)$!*-% zGlg~6jjAC<(V<&TqUrg!mL%+6t*(8r-|nv8J5M)TPK@8BHrPgv&h^ zp?%jxmqQBYK37Nk8h^ZVKrLz7e!#PklI`Kl?af?Voz0Ey{+BtJSf@Fj!(oB5aB`$6 zGa=FdTC`5P?A00L zl`gECn`1KkaeP~xs!B_9aEz2p!~R~rOmi>*^b#GuSaArq#yOwVDm_)6RYSaW*qW&S@TicVscP4Y6fEh6VRyq!suIdI$?Z z;FOaOmJ-V2RHO1<^(->~bp#!q9yWB!X8%kZR}q$c^d%^k)o3wRRl3U`w~Ms*B8E`W zFq?CTt5ohi<-EF(h#PM~e%lA2S|WQ&wNYeQk%D1B(!yEj(eTz6?3ANsY4v@h{Jao6 z%ye+S$cA8@P2EcUwTw!O<6dHa!Fn=4Uq}?`MpIHxkPMYymB~EQf__3pA%FsO8)C|~ zGtxrEmXN-xsBUu5>)?AuW(ezKy}v@jl8=Rs=_a!C(Lc4mlp~)Rn?XI}hs5DmKAWa; z?;APuCs0;q_;qy_~rjg@{LXZ`H@S4;6{}*k_=Dkz7;qYeVL#GaG&g1y`Z=8qW|=Jm+RFt(JF|$Y z4*ZfrQsfjyc#%g#at(rRNSAOxSSIzLh0!wv+#9rLL38S^#|9}lR83$P(J}5{cf(^=4n&d{C z2zVM~`0VP!;SU`Ek1PW42Qx*{ypcu`j%0R+w5;*7zXc&Ti6bvMOOYESc_xnC$4YAT z-|h~#1ifKe?>=s)2*oKg4uo~n7rItbg0khxVJNMk&bK=7=%mRMWoHTv*=HUyWnVGC+6LeRbt9#y&sSQ)HtoWltlZUZ(}Z5ZNI`!ASj!msEFmb~jLqtHYOG5dnTq3*u3IGRLlBK1gJ!{_l z)zSo6NTaq|Vx|*`e2}svFv562Yp=}|@)b2z?$ATn%Qs|{O8}J^cWF&r$VUb2SDl;h zB+4H_+=f&YT#4`l4WW=C#>!1h#DeZ>9_v6ZzA_zBnDD6jg!ym~KHZ9xOk@P5|5+j;F)} zo7&dX(?q1gyV$=4l^8jnMK2u7=1! z7Gut*J}38s%`%w5VNO=?yRGl;g!jE0t^*ISz{Xm>QB6uwH@VGp+anFK0E;&N#j<;+ zA*No3a{->Py`Cj7ZefoGZ>d+_ZS8*HLO1*%h z$U#aB3qNOYHc^prhUj3ZF)4qzVQIVv)54#_RbH%8dB~Cp2VpzR-BUln+Vy!MqQ9Wy z-?_!$^TUFxfop151hlr^T?b80m}4Z?nM>uCpw*hINsl*s!#L{Sz@;T7()ZN)P$bu1 zxpU-U4ti;+HcUZ7GK#y#ABfd3B& zZ5a26Mrsf&9Bk}qo)SpJ|HrZYng#P)( zjUx@UR2BAK{$D3RlY&aEWEz`iD^nd3xD+XhUOv#wq7V!j3fgAW4e^2&7Np!lM><%{ zkX3~<5?`r7F%pD9hy)ch4cHRBwZ?uSA97oi$xf1L?8$YAhmil$?=3YoiGBb*V+s1~ zkOf$5edM!2JA@51BVYAl_WHesr9%!3TrrC@M82#kP2 z>WWMx3S_u31dMHwx~?*ug(-?MEVenC@=#fz1$j58ff#(&qKcT-f~99DB^t{BEfX%P z(`tQ1x|s8%9pzeD@DHqKSup@IJTWL%(V)LJS&qm6)Kw-ZUaBlP#6t#*2PBX`f0gcl zAwAztgg3oFv{6@P0HFvWA1a^L)Ho`D{SmAjlv{`y_XruVG9KQI;uRnPL`#Xu=i56g z236Wu1r^B`JC4@Sg-sDf5gi+{MMlsEG2gc+u7NqGtOn6X&O|3l{RfZ$m(?26%?6qB zM2;g`djpXXO$_g9E_Y=?L{@>`Aa_Twhu(pLk924G&8^fXf)2L>8X{gvGPAZCGOXe4i6scU9V2K^iY+xF3k^JRRZjJcjaC0?ZnKZMDWyNqWCh0 zFP$?Ys*N=J`J{H*fdtqeq#25}z{9n?LUrP`P3pt9&PNAQauyjO%#@?jdY}T<5qu!R zJ}hrLaV2{=^&E$mpp7d%nyQk9yh#OyB=T+}FUouM!EiqI1AA>%?)xpfjz_b1ti6wFvjR8mDo*HSvCl^{{{J$1$+jC8j?*D$DerA zIiD!Yv&K)|-!|SV#NBIH%k&ND+ex2E49T6d?A zqDiAB_MU9TIk@WjK{P`cFPM`uAd}7Kl2Y`PhKYJa6j;*qX?v&}CC+ zp9?);;hktK79b;~v9UC7LgKeE%0?3MpIX802!^JtaraOD80t)D>EXd!)nqUro&z-w zpfnC{EGTDfttmaSMy1x69t?p}xOS;VNOsV0(T_O44xoM=d{RmAn^4et2$=AC2)_xr z+*yN&yd!5!NeG*lFg_BDn-;WfNaR;K#~G9FyzJjS1OD0$D}!c#fXZ%fDQa!*tj21T zT`DZ$!mj9p5F7Csqu2!ca=6OCdjc;!5Pa&Ga{!c@3z$#YXrE`@VxwYVcCp~K-sd~dyO@oqKA}Vy@`t7{LZFsHN%8@G z#pSMPc3|)3h63Yo94pacr0i=`8OjSX&{)1lbO`v!NY$i5k^u`vtTM&piGk z3bTgyfPwq~Y5^+By^YSGtRuE74KlnDEbHTo4=}b5a+1Nblc(Q9DTJEj)08Fv{XQ!N z4T11hY{GalX8H$8@^6rw6epKMM~AkpyWwQWT6VLIWk@G^ScKRUCx#qosZy-5po7=J z`-I`ZV>!%iiKwNHB2A`YAlp9!JpB6E?fC&=HJzs;TMr=5WBM>4-S}HDTEu0BS?poz z1Q-^(_gONH=DX<^$)~1!`U_*I3(U z^EBadk~UzF;&e-(lQCX^Yp0~gucq5c#jp|E@mega4I0{H>X`)1U0a!P9O;l+o>oe8 z0a{>Sag|S&))J~9K#-%m17~@B@`)UT5xaT!X?H;9s*m z^=_2gHx59xcH3_;V}lSL&29WTQ@R|XEBg=~lTM3>K@jqT`-Kq4w9g|?Lz=|n?e=@| zW*|9pxoF1wT1t3JAPv=%vI2=oRRvCu|gHvK}3rpl4U=2D+Dj9;S z!;HNM=K_zZCTvVLnhbTR)P8(0$xh5|_9kVXo|Cg?4Fpe^f` zM~=!8T8z_(@081t{3dEqMZW>YHcjjKP?@>ko@>sq_eT;+ zb`MQfp7Ji8kp;95lHWd*-NFdOPDX>A({j5O<A?hXoK@GA#U;Ue{R2lTo+$ z_6nPkVU>Fx3{+3yCO!vKuZoRSk@L!MFp=E|kU^4XNuh^_58ayl?IJVL*Wqttq)Yuo zQ=H0A(n~>+yf=~sc(ksV4k%@+_;1D`Rv{w0b#_&hhOpDS8yMys#Jnb?OWMr1o$~&nf17+;MWr zbCx*Q8Hq^KXT=6ZT@X{x9uYZ>>A0P2OWwR7;n1oJy1`Ucvd}26O@>ton4K7vX~mb6-l7N?(c53mRu8TOUWFzgb1E9FX#l|xK{ z`*N*hCPoYZOBclq*E=3*d8<5TgUG#wP-=tH>lC#T`mREbe2)-MWJD+P{6iP~whrrl zmN861hbWSxy%hPF9K0$w_a~FQS7ZY;NWz05(}oV1z>d*H;|zr8x8I@c)b%F`?CxEE z{p$h((#`EKzC?UDHvazS<;>LEnK)I`i_efEUmHXKk!{_eH!hnS5TSh zf{Sd#_T*(jg~z(Ve2H!%r#0c}l5jr*bZ}XjH^j?{3v3K}4mxrgN6&g*_vUPO$8TOS z=Ef`ST^!KR2lsX8k;RfTR2Ura6&in&%^+} zqC-kF6Y|6 zRF_mQZX~OA%@ai>u|1Dds4L>R9mRj(WFb@CmJ;pHuG0=S#XpJudGQNo$k$08MKH2&Q8vc5R zNdBF4nfCO!iOVO^r@qhjdJ{32R)>}Ja6ZvA<#5^p@*EcRe&F$$mZZBp#s`ar{*OCr z`rqZyPi3z9@8yS!RqHly^`4sN%H7JZ3w^hMpMWZFL%(XOWodOy!?NYosw{0cfQEb( zKplJ8+)Z6ye+BdFqxRwbGSG)zub{KmVzFw`T4Uz2?_$bYpr;0F`M_3Vb@|}7>f)r& ztF22lo^|5>a}<1u1DFUbU!qgShO*4zB7ijgofT6c%>~oZP8u`=|qetN9bAg{vWv0d&8` zrnn87zoO2qKI+?RXQ`t4%F5h0`#Rdw8A@NxKd%eHgSR2V73&Q8e7swnwyC25x@&=s( zeHoen4Zw~ba+k8u z&%ezvi`!?V9`c=X(Zg6BfMBHi&{uO;rmsh-FggUVU;gJu_fA3&FHng4BK3G&mIQk?tMQW7A-x%2TEJzAyYH_{58~%ol&XXP z%T&<6uVVw&d;|*4Z%eRHHJmjd;RsjvCkO4hGiAFsr%zYo^q0y)0N3zS3EY##y0FbI ztu!KkyqbOxWxD?S$}q6$mT<6cWLZ|Nju>O!Ed8%-h_(~pT|V^5ai? zpNu0Y&j5|tOZfP*_g_`iD0n;)d8-dRFHEIrdrN6gTyzKNl!vihAm06b-`)nhvktMR zZe@e2))aFF5UBPY(l;oUGtzox+nqPZNBbXeGDi*_25>N_TQu;i zb!-rtWl#{}G!V-gF6NZ3jvJeux0hv~+m&>`-}Cq*GetdVeSIHa#6Dqj&k{=E2N6%N zvf83QWFyJ$fP7h;>?9Av?CJ@5mvGW1d!r?CAZq(I0rMFuG;rqG%wSQlkyx+Tt(8gT zn|1ug^_St^M*X=w)h!L0hTR9x9G`D{ zJq}BQyQ)ZLgXLmwL}o=Tb`_sR1_=TTnH6pL2M~{?v!)iiOwOiESE^(;HT3;S;u8L= z@T0$s;Nq~4=9O?aENgIxS}lS5R=KQQ$+Fj*cRMrpE7x#~?y@0=hipIS8D;|+@wp1C zSX=>&rbK%eJ%>t)B%CaNcuc00k&nHEEN=+$-Vf5<4%$WVc#=;*ojNpEUrKP(8<|FE z7sRxTCy~Raz7o5c6}9rDTCDDHC5RpZ`nTw{KkkcvA6ezlBcOMA37Oqs$MXXp`!j2Z z(JjSkeE-|J>g)%EdbWl0f^(|?a=42djcOCi%-*FXa%sV}_A#}2y=R@D>-nA#8{RJj zKI9qIL!ux2)FJx%Y7cG2uzE}n+%Z%0|5PtLAd?4mMlt@OIvJ8I`%IeINzQ>yZqVFq z^}JC5%YQQ*!B)mg8xTgqNJG*=(pQpT5f&2_Wo2O(=HzDQ5fx=;|0Th}!pbHgBE~Jj z!y_g@!uS8S=)*C~ncG{qT9R;ZrWuhV(E%tI=4923F-GqmqGNY8iL!!`%e+9xfBx4!t>ZWIb!NQ5a=>%gn#|H|*pbqBboKBw% zy>#FD-TGl`ikS&gsX&sER2#5KF~$3C})a!jq&G%wSu(E2d2^PitevBsZUGY(0UIBjUoxSx&z%<7I}6 zDDn9Z$Z`!9PEUx=U8YpQEWX07p@zdAo`PzxQ*W>nP-g2E^lOK5HZa@ke%Z>!)3qx` z{URb+cEoP{Wf1b>HCGu*5Zrb*I|>kRjzCDFs0evEt-W4J@Lmu?N*JOLkBu*)kdIA} zSP+X%LNCrR8<+O{P5*qN`frn~MrUuARx2m;XRl@%_qD24o&NJSuXiKpi?TrCXgk@VZaq6osm^rW2*Lr+$)*V7+aUG#j_+LZZFZd^yO`Vn+0WuTTm? z*{w~*MO9ir8ShWZk_+XRiq(c1+dH)cqo~Yf@B(Y48GcGGKt`bKF@`>C4~ZC#gM$-}l2Tkz0`7kRm9Ye1 diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.tex b/papers/dual_decomposition_minimal_counterexamples/paper.tex index 9a30bc3..9806a5f 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.tex +++ b/papers/dual_decomposition_minimal_counterexamples/paper.tex @@ -647,12 +647,14 @@ $(F, e_1, e_2)$ whose accompanying $f_n$ satisfies clause~(4) (see \begin{tabular}{r|r|r|r|l} $n$ & \#tri & \#col.\ tested & \#sat. & status \\ \hline -$14$ & $1$ & $216$ & $216$ & all pass \\ -$16$ & $3$ & $864$ & $864$ & all pass \\ -$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ -$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ +$14$ & $1$ & $216$ & $216$ & all pass \\ +$16$ & $3$ & $864$ & $864$ & all pass \\ +$17$ & $4$ & $4{,}650$ & $4{,}650$ & all pass \\ +$18$ & $12$ & $8{,}070$ & $8{,}070$ & all pass \\ +$19$ & $23$ & $21{,}138$ & $21{,}138$ & all pass \\ +$20$ & $73$ & $107{,}874$ & $107{,}874$ & all pass \\ \hline -total ($n \le 18$) & $20$ & $13{,}800$ & $13{,}800$ & \\ +total ($n \le 20$) & $116$ & $142{,}812$ & $142{,}812$ & \\ \end{tabular} \end{center} \noindent A subtlety: only about half of the