OKlibrary  0.2.1.6
GreenTao_te_m-4-4.hpp File Reference

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,4,4]) More...

Go to the source code of this file.


Detailed Description

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,4,4])

Boolean problems using the aloamo-translation are generated by output_greentao_stdname(append(create_list(2,i,1,m),[4,4]),n) and output_greentao_sb_stdname(append(create_list(2,i,1,m),[4,4]),n) at Maxima-level, and by "GTSat 2 ... 2 4 4 n" at C++ level.

Boolean problems using the standard nested translation are generated by output_greentao_standnest_stdname(append(create_list(2,i,1,m),[4,4]),n) resp. output_greentao_standnest_strong_stdname(append(create_list(2,i,1,m),[4,4]),n) at Maxima-level.

The logarithmic translation is generated by output_greentao_logarithmic_stdname(append(create_list(2,i,1,m),[4,4]),n).

Todo:
greentao_3(2,4,4) >= 553
  • The conjecture is greentao_3(2,4,4) = 553.
  • Best local search algorithm from Ubcsat-suite:
    > E = run_ubcsat("GreenTao_3-2-4-4_530.cnf")
       
    evaluated by plot(E$alg,E$best): Again novelty+ seems best (the only solver who found a solution):
    > table(E$best[E$alg=="noveltyp"])
     0  1  2  3  4  5  6  8
     3 16 32 19 14  8  7  1
       
  • n=550: cutoff=10^5 with novelty+ not enough, cutoff=2*10^5 still not enough, cutoff=4*10^5 found one solution (seed=1478958963,osteps=358472):
     1  2  3  4  5  6  7  8  9 10 11 12 13 15
     1  3  5 13 10 13 14 11  7  8  4  6  4  1
    100
     1  2  3  4  5  6  7  8  9 10 11 12
     5 14  9 13 13 12 17  9  3  3  1  1
    100
     0  1  2  3  4  5  6  7  8  9 10
     1 12 29 18 19 11  4  3  1  1  1
    100
       
  • n=551, novelty+, cutoff=10^6: 8 solutions found
     0  1  2  3  4
     8 40 35 15  2
    100
       
    (seed=3514873770, osteps=223114).
  • n=552:
    1. novelty+ (aloamo), cutoff=10^6: 5 solutions found
       0  1  2  3  4  5  6  7
       5 38 34 15  3  3  1  1
      100
           
      (seed=783660701, osteps=463980).
    2. rnovelty (weak standard nested), cutoff=10^6:
      > EN = read_ubcsat("GreenTao_N_3-2-4-4_552.cnf_OUT")
       0  1  2  3
      10 65 24  1
      100
           
    3. rnovelty+ (strong standard nested), cutoff=10^6:
       0  1  2
      28 53 19
      100
           
      So rather clearly the strong standard nested translation is superior here.
  • n=553:
    1. novelty+ (aloamo) with cutoff=10^6, 2*10^6, 4*10^6
       1  2  3  4  5  6
      33 38 16  6  6  1
      100
      
       1  2  3
      63 30  7
      100
      
       1  2  3
      95  4  1
      100
         1    2    3
      1879  109   12
      2000
           
    2. Finding a best algorithm for the strong standard nested translation:
      > E = run_ubcsat("GreenTao_SN_3-2-4-4_553.cnf")
           
      using plot(E$alg,E$best):
      > table(E$best[E$alg=="rnoveltyp"])
       1  2  3  4
      19 48 30  3
      > table(E$best[E$alg=="rnovelty"])
       1  2  3  4
      15 48 35  2
      > table(E$best[E$alg=="walksat_tabu_nonull"])
       1  2  3  4  5  6
       9 20 41 22  7  1
           
      Clearly rnoveltyp and rnovelty seem best.
    3. Finding a best algorithm for the weak standard nested translation:
      > E = run_ubcsat("GreenTao_N_3-2-4-4_553.cnf")
           
      using plot(E$alg,E$best):
      > table(E$best[E$alg=="rnovelty"])
       1  2  3  4
      12 57 27  4
      > table(E$best[E$alg=="walksat_tabu_nonull"])
       1  2  3  4  5  6
      12 29 35 18  5  1
      > table(E$best[E$alg=="walksat_tabu"])
       1  2  3  4  5  7
      12 22 35 21  9  1
      > table(E$best[E$alg=="rnoveltyp"])
       1  2  3  4
      11 52 34  3
           
    4. So it seems that the strong standard nested translation is better than the weak one here.
    5. rnovelty+ (strong standard nested) with cutoff=2*10^5, 4*10^5, 8*10^5, 2*10^6, 4*10^6:
       1  2  3
      32 60  8
      100
       1  2  3
      41 57  2
      100
       1  2
      51 49
      100
       1  2
      63 37
      100
       1  2
      84 16
      100
           
    6. rnovelty (strong standard nested) with cutoff=2*10^5, 4*10^5, 8*10^5, 2*10^6, 4*10^6:
       1  2  3  4
      19 69 11  1
      100
       1  2  3
      36 62  2
      100
       1  2
      54 46
      100
       1  2
      66 34
      100
       1  2
      68 32
      100
           
      So rnovelty+ seems here (n=553, strong standard nested) better than rnovelty.
    7. cutoff=4*10^6 with sapsnr (strong standard nested):
       1  2
      96  4
      100
           
      Thus actually sapsnr seems best here (n=553, strong standard nested).
    8. cutoff=4*10^6 with saps (strong standard nested):
       1  2
      99  1
      100
           
  • n=555, novelty+ (aloamo)
    1. cutoff=10^6:
       1  2  3  4  5  6  7
      13 30 35 10  6  4  2
      100
           
    2. cutoff=2*10^6 (aloamo)
       1  2  3  4  5
      42 47  4  6  1
      100
           
  • n=560, novelty+ (aloamo):
    1. cutoff=10^6:
       1  2  3  4  5  6  7  8
       8 26 21 17 13 11  3  1
      100
           
    2. cutoff=2*10^6 (aloamo):
       1  2  3  4  5
      30 32 20 15  3
      100
           
  • n=570: For cutoff in 10^6, 2*10^6, 4*10^6, 8*10^6, cutoff=16*10^6 (novelty+, aloamo) we get the following min-distributions:
     1  2  3  4  5  6  7  8  9 10
     1  6 15 13 18 14 10 14  6  3
    100
     1  2  3  4  5  6  7  8
     1 16 21 21 17  6 11  7
    100
     1  2  3  4  5  6  7
     2 32 32 21  8  3  2
    100
     1  2  3  4  5
     5 63 16 11  5
    100
     1  2  3
    27 58 15
    100
       
    adaptnovelty+ with cutoff in 4*10^6, 16*10^6 reaches
     1  2  3  4
     2 22 73  3
    100
     1  2  3
    20 55 25
    100
       
    (so within this cutoff-range novelty+ is better than adaptnovelty+). Let's consider this as unsatisfiable.
  • OKsolver_2002 for n=553:
    1. Without preprocessing and without symmetry breaking:
      • > OKsolver_2002-O3-DNDEBUG -M -D16 -F GreenTao_3-2-4-4_553.cnf
               
        Looks possible.
      • Running it on a 64-bit machine ("cspasiphae"), it is much slower than on the old 32-bit laptp: It needs roughly 40s for 10000 nodes (and on cs-wsok it is more than 80s), while on csltok (32-bit, 1.7GHz) it needs roughly 20s for 10000 nodes!)
      • Aborted after 1631 monitoring nodes (average time 6m per monitoring node, average node count 87600). So with some parallelisation (and a more efficient implementation for 64-bit machines) it might be possible (say with 10 machines in 2 weeks).
      • Using the standard strong nested translation: Running it at monitoring-level 20, until monitor-node 13 the prediction was, say, 3 years, but then it got stuck, and didn't make progress after a few hundred million nodes and a few days. However, as discussed below, this translation can likely be improved.
      • precosat236 and picosat913 apparently didn't make progress after a few days on the standard strong nested translation.
      • Using the logarithmic translation: somewhat hard to say, since the first 40000 monitoring nodes at monitoring depth 30 are skipped, but then it seems to process them mostly without jumps (which would take a long time).
      • However, as discussed further below together with preprocessing, it seems natural that for three values the simple logarithmic translation, which just adds the fourth binary clause without preprocessing, is deficient, since the subsumption resolution with that fourth clause should be performed.
    2. With preprocessing and without symmetry breaking:
      > OKsolver_2002-m2pp -M -D16 -F GreenTao_3-2-4-4_553.cnf
           \endverbatm
           Didn't complete a monitoring node after 3 m and 150000 nodes (now no
           autarkies were found, different from the run without preprocessing,
           where there are many). </li>
           <li> The standard strong nested translation doesn't look much different
           than without preprocessing. </li>
           <li> Using the logarithmic translation: now the initial jump doesn't
           happen as above (which might just be irrelevant), and so the prediction
           is that it takes years. </li>
           <li> It seems the major problem is the "polynomial overhead" (it takes
           about 0.16s for one node), and with a much improved implementation of the
           OKsolver_2002 it might become feasible. </li>
           <li> Interesting that preprocessing reduced the maximal clause-length
           from 8 to 4 (while only eliminating 4 variables) --- of course,
           this is the 2-subsumption resolution between the single binary
           remainder clauses per original variable and the 4 binary clauses
           making up the old arithmetic progressions for two values! This process
           should be already included in the logarithmic translation. </li>
          </ol>
         </li>
         <li> march_pl: aloamo aborted after 10000m; some progress was made (154*10^6
         nodes processed, 1424 resolvents added). </li>
         <li> satz215: aloamo aborted after 2800m. </li>
         <li> minisat2 for n=553: aloamo aborted after 129431786 conflicts; unclear
         whether something has been achieved. </li>
         <li> picosat913: aloamo aborted after 2800m. </li>
         <li> precosat236: aloamo aborted after 2800m. </li>
        </ul>
      
      
        \todo greentao_4(2,2,4,4) > 588
        <ul>
         <li> Let's use novelty+ as the main Ubcsat-solver (aloamo). </li>
         <li> n=560:
          <ol>
           <li> cutoff=10^5: Only min=1 reached once in 100 runs. </li>
           <li> cutoff=10^6: Finds one satisfying assignment in 100 runs
           (seed=1415197577, osteps=723855). </li>
          </ol>
         </li>
         <li> n=565: cutoff=2*10^6 found a solution (seed=1961628490,
         osteps=1873226). </li>
         <li> n=570:
          <ol>
           <li> cutoff=10^5: Only min=2 reached in 100 runs. </li>
           <li> cutoff=10^6:
           \verbatim
       1  2  3  4
       7 62 28  3
      100
           
    3. cutoff=2*10^6: One solution found:
       0  1  2  3
       1 14 72 13
      100
      > E[E$min==0,]
         sat min  osteps  msteps       seed
      65   1   0 1403508 1403508 2325307179
           
  • n=575, cutoff=4*10^6 found one solution in 100 runs:
    > E = read_ubcsat("GreenTao_4-2-2-4-4_575.cnf_OUT")
     0  1  2  3
     1 24 70  5
    100
    > E[E$min==0,]
       sat min  osteps  msteps     seed
    83   1   0 3483852 3483852 16671608
       
  • n=576, cutoff=8*10^6 found two solutions:
    > E = read_ubcsat("GreenTao_4-2-2-4-4_576.cnf_OUT")
     0  1  2
     2 38 60
    100
    > E[E$min==0,]
       sat min  osteps  msteps       seed
    51   1   0 2153855 2153855 3258497817
    76   1   0 7167424 7167424 1485882798
       
  • n=577, cutoff=8*10^6 found four solutions:
    > E = read_ubcsat("GreenTao_4-2-2-4-4_577.cnf_OUT")
     0  1  2
     4 45 51
    100
    > E[E$min==0,]
       sat min  osteps  msteps       seed
    14   1   0 4257866 4257866 2950525585
    39   1   0 6706276 6706276 3190160765
    44   1   0  993412  993412  557624388
    88   1   0 7500128 7500128 2192412699
       
  • n=578, cutoff=8*10^6 found two solutions:
    > E = read_ubcsat("GreenTao_4-2-2-4-4_578.cnf_OUT")
     0  1  2  3
     2 39 58  1
    100
    > E[E$min==0,]
       sat min  osteps  msteps      seed
    44   1   0 7670173 7670173 507583806
    95   1   0 2771712 2771712 457551247
       
  • n=579, cutoff=8*10^6 found 9 solutions in 456 runs:
    > E = read_ubcsat("GreenTao_4-2-2-4-4_579.cnf_OUT")
      0   1   2   3
      9 110 336   1
    456
    > E[E$min==0,]
        sat min  osteps  msteps       seed
    122   1   0 2586652 2586652 2079796651
    133   1   0 6589542 6589542 1027139407
    142   1   0 6180698 6180698 1112107542
    206   1   0 7075206 7075206 1607625335
    225   1   0 1535855 1535855 3261883268
    251   1   0 6498298 6498298 1816856192
    440   1   0 5000770 5000770 4060946138
    448   1   0 6636397 6636397 4118168529
    456   1   0 6359963 6359963  843130387
       
  • n=580
    1. cutoff=8*10^6:
      > E = read_ubcsat("GreenTao_4-2-2-4-4_580.cnf_OUT")
       1  2  3
      27 71  2
      100
           
      But by another 5 runs a solution was found (seed=2467546148, osteps=1805111).
  • n=581, cutoff=16*10^6: found one solution in 44 runs (seed=4268383518, osteps=9958990).
  • n=582, cutoff=16*10^6: found one solution in 16 runs (seed=4174937477, osteps=8389525).
  • n=583
    1. cutoff=16*10^6:
       1  2
      17 83
      100
           
    2. cutoff=32*10^6
       1  2
       2 13
      15
           
      Then in another 100 runs one solution was found (seed=976475738, osteps=11027365).
  • n=584
    1. cutoff=32*10^6
       1  2
      31 69
      100
      > summary(E$osteps[E$min==1])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
        536800  5037000 12270000 12320000 17450000 30670000
        0   1   2
        1 103 265
      369
      > summary(E$osteps[E$min==0])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
      14750000 14750000 14750000 14750000 14750000 14750000
      > summary(E$osteps[E$min==1])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
        723300  6490000 11910000 13420000 21220000 31230000
      > summary(E$osteps[E$min==2])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
         98950   989600  1800000  2308000  2968000 11240000
           
    2. Best local search algorithm from Ubcsat-suite for the standard nested translation:
      > E = run_ubcsat("GreenTao_N_4-2-2-4-4_584.cnf")
           
      evaluated by plot(E$alg,E$best): Only one algorithm reached min=1, namely saps:
      > table(E$best[E$alg=="saps"])
       1  2  3  4  5  6  7  8  9 10 11 12 13
       1  2  5  5  7 13 14 16 17 10  6  3  1
      > table(E$best[E$alg=="rnovelty"])
       2  3  4  5  6
      10 33 46  9  2
           
      Of course, this could be just chance.
    3. saps (weak nested translation) with cutoff=2*10^5, 4*10^5, 8*10^5, 1.6*10^6:
       1  2  3  4  5  6  7  8  9 10
       2  4  4  4 12 19 18 18 12  7
      100
      
       1  2  3  4  5  6  7  8
      10  5 13 13 18 20 11 10
      100
      
       1  2  3  4  5  6  7
       8 10 24 16 24 12  6
      100
      
       1  2  3  4  5  6  7
      32 16 21 20  7  3  1
      100
       0  1  2  3  4  5  6
       2 21  8  8 15  5  1
      60
           
      So it seems clear that the (weak) standard nested translation is superior over the aloamo-translation.
    4. rnovelty with cutoff=2*10^5 (nested translation):
       2  3  4  5
      17 46 32  5
      100
           
      So at least for these cutoffs, saps seems better for finding a solution.
  • n=585
    1. cutoff=8*10^6 (aloamo,novelty+)
        1   2   3
       87 885  28
      1000
           
    2. cutoff=16*10^6 (aloamo,novelty+)
       1  2
      18 82
      100
           
    3. cutoff=32*10^6 (aloamo,novelty+)
       1  2
      17 83
      100
      > summary(E$osteps)
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
         76780   806200  1754000  3155000  3024000 30470000
      > summary(E$osteps[E$min==1])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
        313400  1651000  5439000  8654000 10490000 30470000
      
        1   2
       66 326
      392
      > summary(E$osteps)
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
         56830  1048000  2186000  4052000  3940000 30100000
      > summary(E$osteps[E$min==1])
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
        517100  3349000 10820000 11870000 18610000 30100000
           
    4. Best local search algorithm from Ubcsat-suite for the (weak) standard nested translation:
      > E = run_ubcsat("GreenTao_N_4-2-2-4-4_585.cnf")
           
      evaluated by plot(E$alg,E$best):
      > table(E$best[E$alg=="rnovelty"])
       2  3  4  5  6  7
       6 28 49 15  1  1
      > table(E$best[E$alg=="sapsnr"])
       2  3  4  5  6  7  8  9 10 11 12 13
       5  6  4  2  8 17 14 16 14  7  6  1
      > table(E$best[E$alg=="rnoveltyp"])
       2  3  4  5  6
       4 35 43 14  4
      > table(E$best[E$alg=="walksat_tabu_nonull"])
       2  3  4  5  6  7  8  9
       2 13 17 26 22 10  9  1
      > table(E$best[E$alg=="walksat_tabu"])
       2  3  4  5  6  7  8
       2 10 27 19 21 16  5
      > table(E$best[E$alg=="novelty"])
       2  3  4  5  6  7  8
       2  4 27 33 26  7  1
      > table(E$best[E$alg=="walksat"])
       2  3  4  5  6  7  8  9 10 11
       1 12 16 23 21 10  6  6  3  2
      > table(E$best[E$alg=="noveltyp"])
       2  3  4  5  6  7
       1  4 31 43 19  2
      > table(E$best[E$alg=="saps"])
       2  3  4  5  6  7  8  9 10 11 12 13
       1  3  8  4 11 18 20 16 10  6  2  1
      > table(E$best[E$alg=="gwsat"])
       2  3  4  5  6  7  8  9 10 11 12
       1  1  2  6 12 22 19 20 10  6  1
           
      So here rnovelty seems best.
    5. rnovelty (weak standard nested translation) with cutoff=10^6, 4*10^6, 8*10^6:
       1  2  3  4
       2 55 42  1
      100
      
       1  2  3
       3 80 17
      100
      > summary(EN$osteps[EN$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       111300  221000  330700  984100 1421000 2510000
      > summary(EN$osteps[EN$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        38660  228200  371700  804900 1010000 3525000
      > summary(EN$osteps[EN$min==3])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        66530  167100  342700  497700  653500 2410000
      
       2  3
      91  9
      100
           
    6. sapsnr with cutoff=1.6*10^6 (weak nested translation):
       1  2  3  4  5  6  8
      31 18 33  8  6  3  1
      100
           
      Thus sapsnr is definitely better than rnovelty here, and the (weak) standard translation is superior to the aloamo-translation.
    7. saps with cutoff=1.6*10^6 (weak nested translation):
       0  1  2  3  4  5  6
       1 24 18 24 18 12  3
      100
      > ESN[ESN$min==0,]
         sat min osteps msteps       seed
      48   1   0 942735 942735 3414697231
           
    8. Finding a best algorithm for the strong standard nested translation:
      > E = run_ubcsat("GreenTao_SN_4-2-2-4-4_585.cnf")
           
      using plot(E$alg,E$best):
      > table(E$best[E$alg=="sapsnr"])
       1  3  4  5  6  7  8  9 10 11 12
       1  2 12  4  8 21 22 15 10  4  1
      > table(E$best[E$alg=="rnovelty"])
       2  3  4  5  6
      10 36 38 14  2
      > table(E$best[E$alg=="rnoveltyp"])
       2  3  4  5  6
       9 38 40 12  1
      > table(E$best[E$alg=="walksat_tabu_nonull"])
       2  3  4  5  6  7  8  9
       3  7 19 22 24 13 10  2
      > table(E$best[E$alg=="noveltyp"])
       2  3  4  5  6  7
       2 16 41 32  8  1
      > table(E$best[E$alg=="walksat_tabu"])
       2  3  4  5  6  7  8  9
       2  9 15 28 19 16 10  1
           
    9. rnovelty with cutoff=10^6 (strong nested translation):
       1  2  3  4
       2 75 22  1
      100
           
    10. sapsnr with cutoff=10^6 (strong nested translation):
       1  2  3  4  5  6
      18 24 17 18 13 10
      100
           
    So the question (for now) is to decide between the weak and the strong (standard) nested translation, and between saps and sapsnr.
  • n=586
    1. saps with cutoff=2*10^6, weak standard nested translation:
        1   2   3   4   5   6   7
      169  73 112  80  36  26   4
      500
           
    2. sapsnr with cutoff=2*10^6, weak standard nested translation:
        0   1   2   3   4   5   6   7
        1 134  86  84  42  25  10   1
      383
           
      (seed=2960943394, osteps=137554).
  • n=587
    1. saps with cutoff=2*10^6, weak standard nested translation:
      > EN = read_ubcsat("GreenTao_N_4-2-2-4-4_587.cnf_OUT")
       0  1  2  3  4  5  6  7
       2 45 26 45 31 23 10  1
      183
      > EN[EN$min==0,]
          sat min osteps msteps       seed
      82    1   0 813381 813381  698013339
      115   1   0 888991 888991 2520556202
           
  • n=588
    1. saps with cutoff=10^6, logarithmic translation:
       1  2  3  4  5  6  7  8
      12 17 16 18 13 17  1  1
      95
           
    2. Best local search algorithm from Ubcsat-suite for logarithmic translation:
      > E = run_ubcsat("GreenTao_L_4-2-2-4-4_588.cnf")
           
      evaluated by plot(E$alg,E$best):
      > table(E$best[E$alg=="walksat_tabu"])
       1  2  3  4  5  6  7  8  9
       1  2 14 25 20 16 15  6  1
      > table(E$best[E$alg=="rnoveltyp"])
       2  3  4  5  6
      22 45 28  4  1
      > table(E$best[E$alg=="rnovelty"])
       2  3  4  5  6
      20 51 20  8  1
      > table(E$best[E$alg=="novelty"])
       2  3  4  5  6  7
       3 21 41 29  5  1
      > table(E$best[E$alg=="noveltyp"])
       2  3  4  5  6
       2 31 39 25  3
      > table(E$best[E$alg=="sapsnr"])
       2  3  4  5  6  7  8  9 10 11 12 13
       1  5  4  9 11 13 23 13 17  2  1  1
      > table(E$best[E$alg=="saps"])
       2  3  4  5  6  7  8  9 10 11 12 13
       1  1  1  4 13 15 21 21 14  4  4  1
           
      So here rnovelty+ seems best, while likely the success of walksat-tabu is just chance (but one needs to try it out).
    3. rnovelty+ with cutoff=10^6, logarithmic translation:
       1  2  3
       3 44 12
      59
           
      So again it seems that rnovelty+ is not suitable for finding solutions, and the performance for low cutoffs is misleading.
    4. walksat-tabu with cutoff=10^6, logarithmic translation:
      2 3
      8 2
      10
           
      Also walksat-tabu seems inefficient here.
    5. sapsnr with cutoff=10^6, logarithmic translation:
       1  2  3  4  5  6  7  8  9
      28 47 43 38 25 30  5  2  1
      219
           
    6. sapsnr with cutoff=2*10^6, logarithmic translation:
      
           
    7. Now we consider the weak standard reduced translation.
    8. Best local search algorithm from Ubcsat-suite:
      > E = run_ubcsat("GreenTao_R_4-2-2-4-4_588.cnf")
           
      evaluated by plot(E$alg,E$best):
      > table(E$best[E$alg=="sapsnr"])
       1  2  3  4  5  6  7  8  9 10 11 12 13
       1  3  1  5  1  4 12 18 21 16 12  5  1
      > table(E$best[E$alg=="walksat_tabu_nonull"])
       1  2  3  4  5  6  7  8  9 10
       1  2  5 14 20 23 21  8  3  3
      > table(E$best[E$alg=="rnoveltyp"])
       2  3  4  5  6
      18 36 29 16  1
           
    9. sapsnr with cutoff=10^6, weak standard reduced translation:
       1  2  3  4  5  6  7  8
       5 11  9 17 19 25 11  2
      99
           
    10. saps with cutoff=2*10^6, weak standard nested translation:
       1  2  3  4  5  6  7
      77 47 70 61 36 31  2
      324
           
    11. sapsnr with cutoff=2*10^6, weak standard nested translation:
       0  1  2  3  4  5  6  7
       1 45 32 47 28 19 15  2
      189
           
      (seed=2449845146, osteps=1366309).
    12. Next we consider the strong standard reduced translation.
    13. Best local search algorithm from Ubcsat-suite:
      > E = run_ubcsat("GreenTao_SR_4-2-2-4-4_588.cnf")
           
      evaluated by plot(E$alg,E$best):
      > table(E$best[E$alg=="sapsnr"])
       1  2  3  4  5  6  7  8  9 10 11 12 13 14
       1  1  1  4  5  4  9 23 19 16  7  8  1  1
      > table(E$best[E$alg=="saps"])
       1  4  6  7  8  9 10 11 12 13
       1  3  4 19 19 23 15 12  2  2
           
    14. The current best combination seems the weak standard nested translation with sapsnr.
  • n=589
    1. Weak standard nested translation, sapsnr, cutoff=2*10^6
       1  2  3  4  5  6  7  8
      98 66 81 52 28 21  1  1
      348
           
    2. Weak standard nested translation, sapsnr, cutoff=4*10^6
        1   2   3   4   5   6
      176  76  54  22   9   1
      338
           
    3. Weak standard nested translation, sapsnr, cutoff=8*10^6
        1   2   3   5
      151  31  17   1
      200
           

Definition in file GreenTao_te_m-4-4.hpp.