OKlibrary  0.2.1.6
0_23_13.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 15.2.2011 (Swansea)
00002 /* Copyright 2011, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 Statistics | tail -n 1 | awk " { print \$0 \" ${s}\"}";
00131 done) > MinisatStatistics
00132 > oklib --R
00133 R> E = read.table("MinisatStatistics", header=TRUE)
00134 > aggregate(E, by=list(sat=E$sat), FUN=mean)
00135   sat   rn    rc       t sat      cfs     dec    rts       r1   mem  ptime  stime      cfl    s
00136 1   1 5928 88596 135.153   1 316141.5 1531617 727.05 54225724 260.8 0.0325 0.0895 75805240 10.5
00137 R> summary(E)
00138        rn             rc              t               cfs              dec
00139  Min.   :5928   Min.   :88596   Min.   :  8.50   Min.   : 44778   Min.   : 475724
00140  1st Qu.:5928   1st Qu.:88596   1st Qu.: 49.25   1st Qu.:132036   1st Qu.: 841614
00141  Median :5928   Median :88596   Median :100.01   Median :253761   Median :1441747
00142  Mean   :5928   Mean   :88596   Mean   :135.15   Mean   :316141   Mean   :1531617
00143  3rd Qu.:5928   3rd Qu.:88596   3rd Qu.:209.46   3rd Qu.:414705   3rd Qu.:2078778
00144  Max.   :5928   Max.   :88596   Max.   :378.08   Max.   :850817   Max.   :3212359
00145       rts               r1                cfl
00146  Min.   : 127.0   Min.   :  7364895  Min.   : 11421272
00147  1st Qu.: 359.8   1st Qu.: 22478942  1st Qu.: 35039243
00148  Median : 589.5   Median : 42611416  Median : 61835458
00149  Mean   : 727.0   Mean   : 54225724  Mean   : 75805240
00150  3rd Qu.: 954.5   3rd Qu.: 70383331  3rd Qu.:104802310
00151  Max.   :1797.0   Max.   :155575015  Max.   :190427737
00152      \endverbatim
00153      </li>
00154      <li> oksolver_2002:
00155      \verbatim
00156 > mkdir oksolver
00157 > for s in $(seq 1 20); do OKsolver_2002-O3-DNDEBUG r1_k${k}.cnf > oksolver/r1_k${s}.result 2>&1; done
00158 > (ExtractOKsolver header-only | awk " { print \$0 \" s\"}"; for s in $(seq 1 20); do
00159   cat oksolver/r1_k${s}.result | ExtractOKsolver | tail -n 1 | awk " { print \$0 \" ${s}\"}";
00160 done) > OKsolverStatistics
00161 R> E = read.table("OKsolverStatistics", header=TRUE)
00162 R> aggregate(E, by=list(sat=E$sat), FUN=mean)
00163    n     c      l mcl       t    nds  r1       r2 pls ats     h
00164 5928 88892 261032 256 1092.69 2269.3 264 388286.1   0   0 15.25
00165  n2cr dmcl  dn  dc   dl snds qnds mnds        pa         ps        tp tel
00166 82432    0 264 808 2472 2.85    0  0.1 0.3913483 0.01715088 0.4084991   0
00167 oats n2cs m2cs
00168    0    0    0
00169      \endverbatim
00170      </li>
00171     </ul>
00172    </li>
00173    <li> Solving for key seed = 1:
00174     <ul>
00175      <li> Most solvers solve the problem in < 6m. </li>
00176      <li> Using the OKsolver:
00177      \verbatim
00178 shell> OKsolver_2002-O3-DNDEBUG -D15 -M r1_k1.cnf
00179 c running_time(sec)                     362.9
00180 c number_of_nodes                       646
00181 c number_of_single_nodes                1
00182 c number_of_2-reductions                120548
00183      \endverbatim
00184      </li>
00185      <li> Using precosat236:
00186      \verbatim
00187 shell> precosat236 r1_k1.cnf
00188      \endverbatim
00189      returns the correct result in 5.2 seconds.
00190      </li>
00191      <li> Glucose finishes in 131.55 seconds:
00192      \verbatim
00193 shell> precosat236 r1_k1.cnf
00194 c restarts              : 721
00195 c conflicts             : 402591         (3060 /sec)
00196 c decisions             : 1562100        (1.58 % random) (11875 /sec)
00197 c propagations          : 57405015       (436374 /sec)
00198 c CPU time              : 131.55 s
00199      \endverbatim
00200      </li>
00201      <li> MiniSAT-2.2.0 finishes in 60s:
00202      \verbatim
00203 shell> minisat-2.2.0 test_keyfind.cnf
00204 <snip>
00205 restarts              : 382
00206 conflicts             : 143515         (2413 /sec)
00207 decisions             : 801345         (0.00 % random) (13473 /sec)
00208 propagations          : 25615653       (430660 /sec)
00209 CPU time              : 59.48 s
00210 
00211 shell> minisat2 r1_k1.cnf
00212 restarts              : 13
00213 conflicts             : 33963          (346 /sec)
00214 decisions             : 214258         (1.39 % random) (2181 /sec)
00215 propagations          : 5270395        (53637 /sec)
00216 CPU time              : 98.26 s
00217     \endverbatim
00218     </li>
00219     <li> march_pl solves it in 19.92s:
00220     \verbatim
00221 shell> march_pl r1_k1.cnf
00222 c main():: nodeCount: 5
00223 c main():: dead ends in main: 0
00224 c main():: lookAheadCount: 133012
00225 c main():: unitResolveCount: 5664
00226 c main():: time=19.920000
00227      \endverbatim
00228      It apparently does this in only 5 nodes??!?
00229      </li>
00230      <li> Picosat solves it in 18 seconds:
00231      \verbatim
00232 shell> picosat913 r1_k1.cnf
00233 c 29 iterations
00234 c 439 restarts
00235 c 94325 conflicts
00236 c 783798 decisions
00237 c 35170202 propagations
00238 c 17.7 seconds total run time
00239      \endverbatim
00240      </li>
00241      <li> survey_propagation doesn't converge:
00242      \verbatim
00243 shell> survey_propagation r1_k1.cnf
00244 <snip>
00245 fixed 1 biased var (+49 ucp)
00246 .:-)
00247 <bias>:-nan
00248 fixed 1 biased var (+17 ucp)
00249 .:-)
00250 <bias>:-nan
00251 contradiction
00252      \endverbatim
00253      </li>
00254      <li> Grasp says "RESOURCES EXCEEDED":
00255      \verbatim
00256 shell> sat-grasp r1_k1.cnf
00257 Registering switches
00258   Done creating structures. Elapsed time: 0.12
00259   Done searching.... RESOURCES EXCEEDED. Elapsed time: 2256.6
00260      \endverbatim
00261      </li>
00262      <li> With "seed : 2$" and "seed : 3$", these runtimes and statistics
00263      seem stable. </li>
00264     </ul>
00265    </li>
00266    <li> DONE (merge_cnf.sh replaced with AppendDimacs)
00267    Finally we merge the assignment with the basic instance:
00268    \verbatim
00269 shell> $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/merge_cnf.sh ssaes_r1_c4_rw4_e8_f1.cnf ssaes_pcpair_r1_c4_rw4_e8_f1_s1.cnf > r1_k1.cnf
00270 
00271 > cat r1_k1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG
00272 terminate called after throwing an instance of 'OKlib::InputOutput::ClauseInputError'
00273   what():  OKlib::InputOutput::StandardDIMACSInput::read_clauses:
00274   literal 5929 has variable index larger than the specified upper bound 5928
00275 line 94566, column 2, total characters read 21231687
00276    \endverbatim
00277    </li>
00278   </ul>
00279 
00280 
00281   \todo Using the 1-base box translation
00282   <ul>
00283    <li> Translation of aes(0+2/3,4,4,8):
00284     <ul>
00285      <li> We treat S-boxes and additions as boxes. </li>
00286      <li> The S-box is considered as a 16x1-bit boolean function. </li>
00287      <li> Generating the smallest (so far) 1-base for the S-box (as of
00288      29/02/2012) from
00289      AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp:
00290      \verbatim
00291 maxima> output_rijnsbox_fullcnf_stdname();
00292 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_pi.cnf
00293 shell> RandomShuffleDimacs-O3-DNDEBUG 103 < AES_Sbox_pi.cnf | SortByClauseLength-O3-DNDEBUG > AES_Sbox_sortedpi.cnf
00294 shell> RUcpGen-O3-DNDEBUG AES_Sbox_sortedpi.cnf > AES_Sbox_gen.cnf
00295 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_Sbox_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_Sbox_base.cnf
00296 shell> cat AES_Sbox_base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00297      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00298      16    4398     16     16    4398    30108     NA     NA    4398    30108     0
00299  length   count
00300       5       1
00301       6    1187
00302       7    2703
00303       8     503
00304       9       4
00305      \endverbatim
00306      </li>
00307      <li> Additions (XORs) of arity k are considered bit-wise as (k+1)-bit
00308      boolean functions; translated using their 2^k prime implicates. </li>
00309     </ul>
00310    </li>
00311    <li> Generating instantiated key-discovery instances for key seeds 1 to 20:
00312     <ul>
00313     \verbatim
00314 set_hm(ss_sbox_rbase_cnfs, 8, read_fcl_f("AES_Sbox_base.cnf"));
00315 num_rounds : 1;
00316 num_rows : 4;
00317 num_columns : 4;
00318 exp : 8;
00319 final_round_b : true;
00320 box_tran : aes_rbase_box;
00321 mc_tran : aes_mc_bidirectional;
00322 output_ss_fcl_std(num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran);
00323 for seed : 1 thru 20 do
00324   output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
00325 
00326 shell> cat ssaes_r1_c4_rw4_e8_f1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00327      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00328     808   89536    808    808   89536   606936     NA     NA   89536   606936   809
00329  length   count
00330       1       8     # 8-bit round constant.
00331       3    1504     # 356 additions of arity 2 (376 * 4 = 1504).
00332       4      64     # 8 additions of arity 3 (8 * 8 = 64).
00333       5      20     # 20 S-boxes.
00334       6   23740     # 20 S-boxes (20 * 1187 = 23740).
00335       7   54060     # 20 S-boxes (20 * 2703 = 54060).
00336       8   10060     # 20 S-boxes (20 * 503  = 10060).
00337       9      80     # 20 S-boxes (20 * 4    = 80).
00338 
00339 # S-boxes make up 87960 of the clauses (98.2%).
00340 
00341 shell> for seed in $(seq 1 20); do AppendDimacs-O3-DNDEBUG ssaes_r1_c4_rw4_e8_f1.cnf ssaes_pcpair_r1_c4_rw4_e8_f1_s${seed}.cnf > r1_k${seed}.cnf; done
00342 
00343 # This holds for all k in 1 to 20.
00344 shell> k=1; cat r1_k${k}.cnf | UnitClausePropagation-O3-DNDEBUG | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00345      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00346     808   88984    544    808   88984   604720     NA     NA   88984   604720   816
00347  length   count
00348       2     512     # 256 equivalence clauses (256 *2 = 512).
00349       3     512     # 128 additions of arity 2 from Key Schedule (128 * 4 = 512).
00350       5      20     # 20 S-boxes.
00351       6   23740     # 20 S-boxes (20 * 1187 = 23740).
00352       7   54060     # 20 S-boxes (20 * 2703 = 54060).
00353       8   10060     # 20 S-boxes (20 * 503  = 10060).
00354       9      80     # 20 S-boxes (20 * 4    = 80).
00355 
00356 # Due to containing an assigned variable:
00357 #  - 256 additions of arity 2 became 256 equivalence clauses.
00358 #    So 256 * 4 = 1024 clauses of size 3 became 256 * 2 = 512 clauses of size 2.
00359 #  - 8 additions of arity 3 became 8 additions of size 2.
00360 #    So 8 * 8 = 64 clauses of size 4 became 8 * 4 = 32 clauses of size 3.
00361      \endverbatim
00362      </li>
00363     </ul>
00364    </li>
00365    <li> Solving for key seeds 1 to 20:
00366     <ul>
00367      <li> minisat-2.2.0 (all solve in < 1m, with < 200,000 conflicts):
00368      \verbatim
00369 > mkdir minisat22
00370 > for s in $(seq 1 20); do RunMinisat r${r}_k${s}.cnf; done
00371 > (ExtractMinisat header-only |  awk " { print \$0 \" s\"}"; for s in $(seq 1 20); do
00372     cat ExperimentMinisat_r1_k${s}cnf_*/Statistics | tail -n 1 | awk " { print \$0 \" ${s}\"}";
00373 done) > MinisatStatistics
00374 > oklib --R
00375 R> E = read.table("MinisatStatistics", header=TRUE)
00376 > aggregate(E, by=list(sat=E$sat), FUN=mean)
00377  rn    rc       t sat      cfs      dec   rts      r1   mem  ptime stime     cfl
00378 808 89496 18.5295   1 100209.8 109272.1 279.1 3570575 37.85 0.0345 2.757 1440958
00379 R> summary(E)
00380       t               cfs              dec              rts              r1
00381 Min.   : 3.260   Min.   :  5703   Min.   :  6613   Min.   : 30.0   Min.   : 180100
00382 1st Qu.: 8.595   1st Qu.: 51497   1st Qu.: 56678   1st Qu.:166.2   1st Qu.:1667288
00383 Median :19.450   Median :110232   Median :119672   Median :290.5   Median :3808369
00384 Mean   :18.529   Mean   :100210   Mean   :109272   Mean   :279.1   Mean   :3570575
00385 3rd Qu.:27.655   3rd Qu.:141995   3rd Qu.:155228   3rd Qu.:388.2   3rd Qu.:5182173
00386 Max.   :36.350   Max.   :194696   Max.   :210509   Max.   :510.0   Max.   :7114841
00387     ptime            stime            cfl                s
00388 Min.   :0.0200   Min.   :2.740   Min.   :  84767   Min.   : 1.00
00389 1st Qu.:0.0300   1st Qu.:2.750   1st Qu.: 744394   1st Qu.: 5.75
00390 Median :0.0400   Median :2.750   Median :1577062   Median :10.50
00391 Mean   :0.0345   Mean   :2.757   Mean   :1440958   Mean   :10.50
00392 3rd Qu.:0.0400   3rd Qu.:2.760   3rd Qu.:2044834   3rd Qu.:15.25
00393 Max.   :0.0400   Max.   :2.800   Max.   :2792138   Max.   :20.00
00394      \endverbatim
00395      </li>
00396     </ul>
00397    </li>
00398 
00399 
00400   \todo Using the "minimum" box translation
00401   <ul>
00402    <li> Translation of aes(0+2/3,4,4,8):
00403     <ul>
00404      <li> We treat S-boxes and additions as boxes. </li>
00405      <li> The S-box is considered as a 16x1-bit boolean function. </li>
00406      <li> Generating the smallest S-box CNF (as of 29/02/2012) from
00407      AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp:
00408      \verbatim
00409 maxima> output_rijnsbox_fullcnf_stdname();
00410 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00411 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00412 shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 40000000 -wtarget 294 -solve 1 -seed 3213901809 -i AES_Sbox_shg.wcnf -r model AES_Sbox_s294.ass;
00413 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00414 shell> cat AES_Sbox_s294.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00415      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00416      16     294     16     16     294     1939     NA     NA     294     1939     1
00417  length   count
00418       6     143
00419       7     127
00420       8      24
00421      \endverbatim
00422      </li>
00423      <li> Additions (XORs) of arity k are considered bit-wise as (k+1)-bit
00424      boolean functions; translated using their 2^k prime implicates. </li>
00425     </ul>
00426    </li>
00427    <li> Generating instantiated key-discovery instances for key seeds 1 to 20:
00428     <ul>
00429     \verbatim
00430 set_hm(ss_sbox_cnfs, 8, read_fcl_f("AES_Sbox_s294.cnf"));
00431 num_rounds : 1;
00432 num_rows : 4;
00433 num_columns : 4;
00434 exp : 8;
00435 final_round_b : true;
00436 box_tran : aes_small_box;
00437 mc_tran : aes_mc_bidirectional;
00438 output_ss_fcl_std(num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran);
00439 for seed : 1 thru 20 do
00440   output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
00441 
00442 shell> cat ssaes_r1_c4_rw4_e8_f1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00443      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00444     808    7456    808    808    7456    43556     NA     NA    7456    43556   809
00445  length   count
00446       1       8     # 8-bit round constant.
00447       3    1504     # 356 additions of arity 2 (376 * 4 = 1504).
00448       4      64     # 8 additions of arity 3 (8 * 8 = 64).
00449       6    2860     # 20 S-boxes (20 * 143 = 2860).
00450       7    2540     # 20 S-boxes (20 * 127 = 2540).
00451       8     480     # 20 S-boxes (20 * 24  = 480).
00452 
00453 # S-boxes make up 5880 of the clauses (78.9%).
00454 
00455 shell> for seed in $(seq 1 20); do AppendDimacs-O3-DNDEBUG ssaes_r1_c4_rw4_e8_f1.cnf ssaes_pcpair_r1_c4_rw4_e8_f1_s${seed}.cnf > r1_k${seed}.cnf; done
00456 
00457 # This holds for all k in 1 to 20.
00458 shell> k=1; cat r1_k${k}.cnf | UnitClausePropagation-O3-DNDEBUG | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
00459      pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
00460     808    6904    544    808    6904    41340     NA     NA    6904    41340   816
00461  length   count
00462       2     512     # 256 equivalence clauses (256 *2 = 512).
00463       3     512     # 128 additions of arity 2 from Key Schedule (128 * 4 = 512).
00464       6    2860     # 20 S-boxes (20 * 143 = 2860).
00465       7    2540     # 20 S-boxes (20 * 127 = 2540).
00466       8     480     # 20 S-boxes (20 * 24  = 480).
00467 
00468 # Due to containing an assigned variable:
00469 #  - 256 additions of arity 2 became 256 equivalence clauses.
00470 #    So 256 * 4 = 1024 clauses of size 3 became 256 * 2 = 512 clauses of size 2.
00471 #  - 8 additions of arity 3 became 8 additions of size 2.
00472 #    So 8 * 8 = 64 clauses of size 4 became 8 * 4 = 32 clauses of size 3.
00473      \endverbatim
00474      </li>
00475     </ul>
00476    </li>
00477    <li> Solving for key seeds 1 to 20:
00478     <ul>
00479      <li> minisat-2.2.0 (all solve in < 2m, with < 5 million conflicts):
00480      \verbatim
00481 > mkdir minisat22
00482 > for s in $(seq 1 20); do RunMinisat r${r}_k${s}.cnf; done
00483 > (ExtractMinisat header-only |  awk " { print \$0 \" s\"}"; for s in $(seq 1 20); do
00484     cat ExperimentMinisat_r1_k${s}cnf_*/Statistics | tail -n 1 | awk " { print \$0 \" ${s}\"}";
00485 done) > MinisatStatistics
00486 > oklib --R
00487 R> E = read.table("MinisatStatistics", header=TRUE)
00488 > aggregate(E, by=list(sat=E$sat), FUN=mean)
00489  rn   rc      t     cfs     dec     rts       r1  mem ptime  stime        cfl
00490 808 7416 16.425 1180878 1362256 2262.45 20572165 22.5     0 0.0185 1 15619589
00491 R> summary(E)
00492       t               sat         cfs             dec               rts               r1
00493 Min.   : 0.030   Min.   :1   Min.   :   1171 Min.   :   2035   Min.   :   7.0   Min.   :   17687
00494 1st Qu.: 4.043   1st Qu.:1   1st Qu.: 367447 1st Qu.: 430745   1st Qu.: 866.5   1st Qu.: 5790918
00495 Median :10.450   Median :1   Median : 865446 Median :1009142   Median :1859.5   Median :13935462
00496 Mean   :16.425   Mean   :1   Mean   :1180878 Mean   :1362256   Mean   :2262.4   Mean   :20572165
00497 3rd Qu.:20.517   3rd Qu.:1   3rd Qu.:1543638 3rd Qu.:1777449   3rd Qu.:3005.8   3rd Qu.:26393793
00498 Max.   :84.270   Max.   :1   Max.   :5113383 Max.   :5820085   Max.   :8191.0   Max.   :97606508
00499     ptime       stime             cfl
00500 Min.   :0   Min.   :0.0100   Min.   :   13866
00501 1st Qu.:0   1st Qu.:0.0200   1st Qu.: 4841715
00502 Median :0   Median :0.0200   Median :11288819
00503 Mean   :0   Mean   :0.0185   Mean   :15619589
00504 3rd Qu.:0   3rd Qu.:0.0200   3rd Qu.:20415258
00505 Max.   :0   Max.   :0.0200   Max.   :68075622
00506      \endverbatim
00507      </li>
00508     </ul>
00509    </li>
00510 
00511 */