OKlibrary  0.2.1.6
GreenTao_4-3-3-3-4.hpp File Reference

Investigations on greentao_4(3,3,3,4) More...

Go to the source code of this file.


Detailed Description

Investigations on greentao_4(3,3,3,4)

Boolean problems using the aloamo-translation are generated by output_greentao_stdname([3,3,3,4],n) or output_greentao_sb_stdname([3,3,3,4],n) at Maxima-level, and by "GTSat 3 3 3 4 n" at C++ level.

Boolean problems using the standard nested translation are generated by output_greentao_standnest_stdname([3,3,3,4],n) at Maxima-level.

Todo:
Best local search algorithm
  • Evaluating
    E = run_ubcsat("GreenTao_4-3-3-3-4_800.cnf", runs=100,cutoff=10000,monitor=TRUE)
       
    by plot(E$alg,E$best), the best algorithms seems sapsnr.
  • However, considering n=1000, now gsat-tabu, adaptnovelty+, rots and samd seem best (for cutoff=10000), while sapsnr became rather weak!
  • Testing these four algorithms with cutoff=10^6:
    E = run_ubcsat("GreenTao_4-3-3-3-4_1000.cnf", runs=100,cutoff=1000000,monitor=TRUE, include_algs=list("gsatt", "anovp", "rots", "samd"))
       
    (currently algorithms-names are inappropriately handled by run_ubcsat): adaptnovelty+ is clearly best: the best min(=6), and a very small spread; the second is samd, but with worst min, and a far larger spread.
Todo:
Lower bounds: greentao_4(3,3,3,4) > 1052
  • n=800 easily found satisfiable by sapsnr (cutoff=10*10^3, runs=100).
  • n=850
    1. cutoff=10^4: adaptnovelty+ reaches in 100 runs min=17 (while sapsnr reaches min=12, and samd reaches min=15).
    2. cutoff=10^5: adaptnovelty+ reaches in 100 runs min=1, while sapsnr finds a solution in run 31 (seed=1051937617).
  • n=900
    1. cutoff=10^4: adaptnovelty+ reaches in 100 runs min=22 (while sapsnr reaches min=29, and samd reaches min=22).
    2. cutoff=10^5: adaptnovelty+ reaches in 100 runs min=3 (while sapsnr reaches min=21, and samd reaches min=5).
    3. cutoff=10^6: adaptnovelty+ finds a solution in run 2 (seed=446607350).
  • n=950
    1. cutoff=10^6, using adaptnovelty+: reaches min=1 (median=4, mean=4.3).
    2. cutoff=10^7 (adaptnovelty+): found a solution in run 3 (seed=3537296603).
  • n=975
    1. cutoff=10^7 (adaptnovelty+): A solution was found in run 60 (seed=839702132, osteps=9609423).
  • n=988
    1. cutoff=10^7 (adaptnovelty+): A solution was found in run 19 (seed=825817361, osteps=8785207).
  • n=989
    1. cutoff=10^7 (adaptnovelty+):
       1  2  3  4  5  6  7
       2 14 22 30 21  9  2
      100
           
    2. cutoff=2*10^7 (adaptnovelty+):
       1  2  3  4  5  6
       4 32 45 14  4  1
      100
           
    3. cutoff=8*10^7 (adaptnovelty+) finds a solution in run 9 (seed=3728380835, osteps=58003122).
  • n=990: cutoff=8*10^7 finds a solution in run 76 (seed=2964724610, osteps=19062436).
  • n=991
    1. cutoff=10^7 (adaptnovelty+):
       1  2  3  4  5  6  7
       1  8 21 28 30  8  4
      100
           
    2. cutoff=8*10^7 (adaptnovelty+):
       1  2  3  4
      18 68 13  1
      100
           
    3. cutoff=16*10^7 (adaptnovelty+): finds a solution in run 5 (seed= 2464081211, osteps=118475284).
  • n=994
    1. cutoff=10^7 (adaptnovelty+):
      > ubcsat-okl -alg adaptnovelty+ -cutoff 10000000 -runs 100 -solve -i GreenTao_4-3-3-3-4_994.cnf | tee GreenTao_4-3-3-3-4_994.cnf_OUT
       1  2  3  4  5  6  7  8
       1  2 13 20 37 18  7  2
           
    2. Checking all algorithms with cutoff=10^6:
      > E = run_ubcsat("GreenTao_4-3-3-3-4_994.cnf", runs=100,cutoff=1000000,monitor=TRUE)
           
      The best algorithms seem to be gwsat, gsat_tabu, adaptnoveltyp and samd, with adaptnoveltyp clearly best (reaching also the best min=6).
    3. cutoff=16*10^7 (adaptnovelty+): finds a solution in run 7 (seed= 2045601853, osteps=122505356).
  • n=995
    1. cutoff=16*10^7 (adaptnovelty+):
       1  2  3
      25 74  1
      100
      > summary(E$osteps)
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
        3958000  31940000  57640000  63860000  88740000 159400000
           
    2. cutoff=32*10^7 (adaptnovelty+): found a solution in run 93 (seed=3734716363, osteps=136285731).
  • n=996: with cutoff=32*10^7 adaptnovelty+ found a solution in run 81 (seed=3070906952, osteps=244941203).
  • n=997: cutoff=32*10^7 (adaptnovelty+) found a solution in run 20 (seed=2765449941, osteps=202286569).
  • n=998
    1. cutoff=32*10^7 (adaptnovelty+):
      > E = read_ubcsat("GreenTao_4-3-3-3-4_998.cnf_OUT");
       1  2
      14 37
      51
      > summary(E$osteps)
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
        3491000  46060000  74970000 107200000 146400000 276500000
      
      > ubcsat-okl -alg adaptnovelty+ -runs 500 -cutoff 320000000 -i GreenTao_4-3-3-3-4_998.cnf | tee GreenTao_4-3-3-3-4_998.cnf_OUT
      > E2 = read_ubcsat("GreenTao_4-3-3-3-4_998.cnf_OUT")
        0   1   2   3
        2 171 323   4
      500
      > summary(E2$osteps)
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
        3559000  52810000  90070000 111600000 155000000 313400000
           
      (best solution: seed=2845522946, osteps=48802626).
  • n=999: cutoff=32*10^7 (adaptnovelty+) found 3 solutions in 65 runs (seed=3665124127, osteps=129828231).
  • n=1000
    1. cutoff=10*10^3 with 100 runs reaches only min=68 (sapsnr), while using cutoff=100*10^3 we get min=65, so let's assume for now that it's unsatisfiable.
    2. However, using adaptnovelty+ with cutoff=100*10^3 we reach min=17, so here adaptnovelty+ is much better!
    3. cutoff=10^6: adaptnovelty+ reaches in 100 runs min=4 (while sapsnr reaches min=50, and samd reaches min=8).
    4. cutoff=10^7 (adaptnovelty+): reaches in 100 runs min=1 (where median=5 and mean=5.01).
    5. cutoff=10^8 (adaptnovelty+):
      > ubcsat-okl -alg adaptnovelty+ -cutoff 100000000 -runs 100 -solve -i GreenTao_4-3-3-3-4_1000.cnf | tee GreenTao_4-3-3-3-4_1000.cnf_OUT
       1  2  3  4
       6 51 40  3
           
    6. cutoff=16*10^7 (adaptnovelty+):
       1  2  3
      14 74 12
      100
      > summary(E$osteps)
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
        4633000  36250000  57420000  66770000  93560000 156800000
           
    7. cutoff=32*10^7 (adaptnovelty+): in 103 runs one solution was found (seed=1507582452, osteps=21453179).
  • n=1001, cutoff=32*10^7 (adaptnovelty+): in 132 runs one solution was found (seed=348166976, osteps=247927263).
  • n=1002, cutoff=5*10^8 (adaptnovelty+): in 62 runs one solution was found (seed=599457750, osteps=71235234).
  • n=1003, cutoff=5*10^8 (adaptnovelty+): in 18 runs one solution was found (seed=3062595810, osteps=481408747).
  • n=1004, cutoff=5*10^8 (adaptnovelty+): in 243 runs one solution was found (seed=3799196791, osteps=499062687). It seems the cutoff should be increased.
  • n=1005, cutoff=10^9 (adaptnovelty+): in 26 runs one solution was found (seed=425251625, osteps=922264601).
  • n=1006, cutoff=10^9 (adaptnovelty+): in 29 runs two solutions were found (seed=1667268345, osteps=342601286).
  • n=1010, cutoff=10^9 (adaptnovelty+): in 91 runs one solution was found (seed=4034341891, osteps=669592854).
  • n=1015
    1. Using the standard nested translation, with cutoff=10^7: In 317 runs one solution was found (seed=548029005, osteps=8867169):
       0  1  2  3  4  5  6  7  8
       1  8 30 71 76 66 48 16  1
      317
           
  • n=1020
    • aloamo
      1. cutoff=10^9 (aloamo, adaptnovelty+)
          1   2   3
         18 227 111
        356
          1   2   3   4
         17 222 126   2
        367
               
    • Weak standard nested translation
      1. adaptnovelty+, cutoff=10^7:
          1   2   3   4   5   6   7   8   9  10
          4  26  59 110 136  95  46  21   2   1
        500
               
      2. sapsnr, cutoff=10^7:
         44  46  47  48  49  50  51  52  53  54  55  56
          1   8  12  21  30  52  76 114  70  69  36  11
        500
               
      3. Best local search algorithm, evaluating
        E = run_ubcsat("GreenTao_N_4-3-3-3-4_1020.cnf", runs=200,cutoff=1000000)
               
        by plot(E$alg,E$best):
        > table(E$best[E$alg=="rnoveltyp"])
         2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18
         2  6  8 10 20 22 15 21 25 17 21 13 10  4  3  2  1
        > table(E$best[E$alg=="novelty"])
         2  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 
         1  2  1  2  5  5  6 11  8  8 11 13 16 11 16 10 18 16  5 13  7  4  2  6  1  1
        30
         1
        > table(E$best[E$alg=="walksat_tabu_nonull"])
         5  6  7  8  9 10 11 12 13 14 15 16 17 18 19
         1  2  4  8 15 23 29 23 32 27 18 12  2  3  1
        > table(E$best[E$alg=="walksat_tabu"])
         5  6  7  8  9 10 11 12 13 14 15 16 17
         2  2  3  5 13 32 28 34 20 22 22 12  5
        > table(E$best[E$alg=="adaptnoveltyp"])
         7  8  9 10 11 12 13 14 15 16 17 18 19 21
         1  1  3  7 21 26 38 28 31 20 11  9  3  1
        > table(E$best[E$alg=="noveltyp"])
         8 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 34 35
         1  1  2  3  2  5  9  9  7  7  6  8  8  8 13 16 14  5 18 14 14  7  7  4  4  1
        36 38 39 40
         3  2  1  1
        > table(E$best[E$alg=="gwsat"])
        10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
         2  5  1  3  9  9 19 25 28  9 40 15 14  9  8  1  3
        
               
      4. rnoveltyp, cutoff=10^7 found a solution in run 14 (seed=1890651975, osteps=8736133).
    • Strong standard nested translation
      1. adaptnovelty+, cutoff=10^7:
          4   5   6   7   8   9  10  11  12
         15  46  94 120 115  81  21   6   2
        500
               
      2. Best local search algorithm, evaluating
        E = run_ubcsat("GreenTao_SN_4-3-3-3-4_1020.cnf", runs=200,cutoff=1000000)
               
        by plot(E$alg,E$best):
        > table(E$best[E$alg=="rnoveltyp"])
         5  8  9 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
         1  2  5  6  8 10 13 11 15 21 14 15 13 19  9 10 10  8  7  1  1  1
        > table(E$best[E$alg=="adaptnoveltyp"])
         7  9 10 11 12 13 14 15 16 17 18 19 21
         1  4  7 20 27 37 31 26 25 12  5  4  1
        > table(E$best[E$alg=="gwsat"])
         8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 26 29
         2  3  2  2  8  9 19 20 21 27 29 25 17  9  3  1  1  1  1
        > table(E$best[E$alg=="rnovelty"])
         8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 29 30
         1  3  3  3  7  7 14 13 19 18 19 16 18 10 11  7 13  9  2  3  3  1
        > table(E$best[E$alg=="walksat_tabu"])
        14 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
         1  1  1  4  1 10 17 16 21 21 21 30 14 12 20  5  4  1
               
      3. rnoveltyp, cutoff=10^7: in 12 runs only a min=6 was reached, so it seems inferior to the weak nested translation.
  • n=1025
    1. Weak standard nested translation, rnovelty+, cutoff=10^7:
      > E=read_ubcsat("GreenTao_N_4-3-3-3-4_1025.cnf_OUT")
       0  1  2  3  4  5  6  7  8
       1  7 26 53 80 52 29  8  1
      257
      > E[E$min==0,]
          sat min  osteps  msteps       seed
      257   1   0 2471159 2471159 4183213878
           
    2. Same, but with cutoff=2*10^7:
       0  2  3  4  5  6
       1 10 28 23  6  1
      69
      > E[E$min==0,]
         sat min  osteps  msteps      seed
      69   1   0 7048847 7048847 838582080
           
  • n=1030
    1. Weak standard nested translation, rnovelty+, cutoff=10^7:
        1   2   3   4   5   6   7   8   9
        6  21  60 119 103 112  51  21   7
      500
           
    2. Weak standard nested translation, rnovelty+, cutoff=2*10^7:
        1   2   3   4   5   6   7
       20  67 130 162  89  26   6
      500
           
    3. Weak standard nested translation with sapsnr and cutoff=4*10^7 only reached min=46.
    4. Weak standard nested translation, rnovelty+, cutoff=8*10^7: found a solution in run 29 (seed=927551785, osteps=14114027).
    5. Strong nested standard translation: Evaluating
      E = run_ubcsat("GreenTao_SN_4-3-3-3-4_1030.cnf", runs=200,cutoff=1000000)
           by plot(E$alg,E$best):
           \verbatim
      > table(E$best[E$alg=="rnoveltyp"])
       8  9 10 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
       1  1  2  2  1  2  5  5 12  8  8 10 15 20 21 13 13 16 12 13  5  5  3  2  2  2
      35
       1
      > table(E$best[E$alg=="rnovelty"])
       9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 34
       1  3  1  4  1  4  2 11 10  9 13  8 14 19 17 14 11 12 13  8 12  7  3  2  1
      > table(E$best[E$alg=="adaptnoveltyp"])
      10 11 12 13 14 15 16 17 18 19 20 21 22 23
       4  1 13 11 26 35 33 29 22  9 11  4  1  1
      > table(E$best[E$alg=="gwsat"])
      11 13 14 15 16 17 18 19 20 21 22 23 24 25 26
       2  6  9 13 21 23 22 22 29 18 12  7  7  5  4
           
      So also here seems rnovelty+ best.
    6. Strong nested standard translation, saps, cutoff=2*10^7:
      40 45 46 47 48 49 50 51 52 53 54
       1  2  5  5 15 17 25 25 23 16  3
      137
           
    7. Strong nested standard translation, rnovelty+, cutoff=2*10^7:
       5  6  7  8  9 10 11 12 13 14 15 16 17 18
       2  5 10 16 27 26 23 15 12 16  9  8  1  2
      172
           
      Thus the weak nested translation seems better than the strong.
    8. Logarithmic translation: Evaluating
      E = run_ubcsat("GreenTao_L_4-3-3-3-4_1030.cnf", runs=200,cutoff=1000000)
           
      by plot(E$alg,E$best):
      > table(E$best[E$alg=="adaptnoveltyp"])
       8  9 10 11 12 13 14 15 16 17 18 19 20 21
       2  1  5  5 24 19 36 32 26 21 15  7  6  1
      > table(E$best[E$alg=="gwsat"])
       9 10 11 12 13 14 15 16 17 18 19 20 21 22
       5  3  4 20 26 25 19 27 26 23  9  8  4  1
           
      It seems the weak nested translation is superior.
    9. Logarithmic translation, rnovelty+, cutoff=10^7:
      12 15 16 17 18 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
       1  3  1  2  3  4  4  3  2  9  2  8  6 15 12 16 25 10 24 23 20 26 36 22 24 21
      41 42 43 44 45
       9  8  3  1  1
      344
           
      And cutoff=2*10^7:
       8 13 14 15 16 17 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
       1  1  3  1  1  1  2  2  1  4  3  7  8  5 12 11  7  1 13 13  8 10 17 16  6  9
      39
       7
      170
           
    10. Logarithmic translation, adaptnovelty+, cutoff=10^7:
       2  3  4  5  6  7  8  9 10 11 13
       1  2  3 20 30 72 90 65 33 15  1
      332
        3   4   5   6   7   8   9  10  11  12
        3   9  26  58 106 107  93  77  18   3
      500
           
      and with cutoff=2*10^7:
       2  3  4  5  6  7  8  9 10 11
       1  7 19 53 84 92 68 35  3  1
      363
           
      while rnovelty+ with cutoff=4*10^7 achieves
       4  8 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
       1  1  1  1  2  2  3  2  3  7  4  2  4  6  6 11  9 12 10 26 24 18 19 26 20 19
      34 35 36 37 39
       8  8  2  2  2
      261
           
    11. So definitely the weak standard nested translation is superior.
    12. Weak standard reduced translation: Evaluating
      E = run_ubcsat("GreenTao_R_4-3-3-3-4_1030.cnf", runs=200,cutoff=1000000)
           
      by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
      adaptnoveltyp :
       9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
       4  3  9 10 12 16 30 35 28 27 14  8  2  1  1
      gwsat :
       9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
       1  1  7  8  9 25 21 22 31 24 23  9  9  6  3  1
           
    13. Strong standard reduced translation: Evaluating
      E = run_ubcsat("GreenTao_SR_4-3-3-3-4_1030.cnf", runs=200,cutoff=1000000)
           
      by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
      adaptnoveltyp :
       8  9 10 11 12 13 14 15 16 17 18 19 20 21 22
       1  2  2 11 15 18 25 20 37 25 20 12  6  3  3
      gwsat :
      11 12 13 14 15 16 17 18 19 20 21 22 23 24
      10  6  7 10 22 34 20 27 15 17 13 12  4  3
      rnovelty :
      13 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
       1  2  2  1  3  3  3  2  7  5  2  6 10 13  9 11  9 11  9 14 14  8  9 12  4  7
           \endverbatm
           </li>
           <li> Strong standard reduced translation, adaptnovelty+, cutoff=10^7:
           \verbatim
        4   5   6   7   8   9  10  11  12  13  14
        2   4  13  42  77 106 102 100  40  11   3
      500
           
  • n=1040, weak standard nested translation
    1. rnovelty+: finds a solution with cutoff=8*10^7 in run 96 (seed=4254844099, osteps=39626357) (while 255 runs with cutoff=4*10^8 only obtained min=1 three times).
    2. adaptnovelty+: with cutoff=8*10^7 in 83 runs only min=2 was reached.
  • n=1050, rnovelty+, cutoff=8*10^7: finds in 293 runs one solution (seed=2097534984, osteps=68769314); another 232 runs:
     2  3  4  5  6  7  8  9
     7 25 75 75 36 10  3  1
    232
       
    while cutoff=16*10^7 yields:
     1  2  3  4  5  6  7
     2  7 36 50 17  2  1
    115
       
    and cutoff=32*10^7:
     1  2  3  4  5
     5 29 83 44  4
    165
       
  • n=1051, rnovelty+
    1. cutoff=32*10^7:
       2  3  4  5
       4 16 13  1
      34
           
    2. cutoff=64*10^7:
       1   2   3  4
       5  18  28  4
      55
           
      In 12 further runs one solution was found (seed=3594476808. osteps=511111838).
  • n=1052, rnovelty+, cutoff=64*10^7: In run 62 a solution was found (seed=990282986, osteps=230887851); further runs:
      1   2   3   4
     11  71 121  13
    216
       
  • n=1053, rnovelty+
    1. cutoff=10^7:
        3   4   5   6   7   8   9  10  11  12  13  14  15  16  17
        2   6  25  60  81 146 160 146 142 110  62  39  14   5   2
      1000
           
    2. cutoff=64*10^7:
       1  2  3  4
       4 19 56 15
      94
           
    3. Evaluating
      E = run_ubcsat("GreenTao_N_4-3-3-3-4_1053.cnf", runs=100,cutoff=1000000)
           
      by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
      rnoveltyp :
       8  9 11 12 13 14 15 16 17 18 19 20 21 22 23 24 26 27 28 29 30 33
       1  2  1  2  5  6  3 10  9 10  7  7  8  3  6  6  3  3  1  4  2  1
      walksat_tabu_nonull :
      10 11 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
       1  1  2  5  4  4 17 11  8 10  9  7  9  6  4  1  1
      rnovelty :
      11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
       2  4  7  3  4  7  7  7 12  6  7  7  5  9  2  1  4  3  3
      walksat_tabu :
      11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
       1  1  1  2  6  8 15 12 14 11  6  9  3  3  2  3  2  1
      adaptnoveltyp :
      13 14 15 16 17 18 19 20 21 22 23 24 25 26 28
       1  3  3  5  8 12 19 16 13  6  2  6  2  3  1
      gwsat :
      16 19 20 21 22 23 24 25 26 27 28 29 30 31 32 34 36
       1  1  2  5 12  9 10  7 12 14  8  7  3  5  1  2  1
           
      So also here rnovelty+ is best.
    4. cutoff=10^9
       1  2  3  4
       3 32 58  7
      100
       1  2  3  4
       5 44 78  6
      133
           
    5. cutoff=2*10^9, rnovelty+:
       1  2  3
       2 20  7
      29
           
  • n=1055
    1. rnovelty+, cutoff=16*10^7:
        1   2   3   4   5   6   7   8
        3  13  59 134 107  52  13   1
      382
           
  • n=1060
    1. rnovelty+, cutoff=8*10^7:
        2   3   4   5   6   7   8   9  10  11  12
        2  13  36  90 107 116  85  33  15   2   1
      500
           
      while cutoff=16*10^7 yields
        2   3   4   5   6   7   8   9  10
        4  38 103 142  72  53  20   3   2
      437
       2  3  4  5  6  7  8
       1 10 27 42 26 10  3
      119
           
      and cutoff=32*10^7 yields
       2  3  4  5  6  7
       3 12 22 17  4  1
      59
       1  2  3  4  5  6
       1  1  1 13  6  1
      23
           

Definition in file GreenTao_4-3-3-3-4.hpp.