OKlibrary  0.2.1.6
GreenTao_3-4-4-k.hpp File Reference

On investigations into Green-Tao numbers greentao_3(4,4,k) More...

Go to the source code of this file.


Detailed Description

On investigations into Green-Tao numbers greentao_3(4,4,k)

Aloamo-translations are generated by output_greentao_stdname([4,4,k],n) at Maxima-level, and by "GTSat 4 4 k n" at C++ level.

Standard nested translations are generated by output_greentao_standnest_stdname([4,4,k],n) resp. output_greentao_standnest_strong_stdname([4,4,k],n).

Todo:
greentao_3(4) > 5500
  • Let's start with the weak standard nested translation and with rnovelty+.
  • greentao_2(4) = 512.
  • n=1000 is satisfiable in 205 steps.
  • n=1500 is satisfiable in 404 steps.
  • n=2000 is satisfiable in 1050 steps.
  • n=2500 is satisfiable in 1339 steps.
  • n=3000 is satisfiable in 2831 steps.
  • n=3500 is satisfiable in 6780 steps (seems hard for OKsolver_2002, and also for minisat2).
  • n=4000 is satisfiable in 26560 steps.
  • n=4500: cutoff=300000 finds a solution in the second run.
  • n=4800: cutoff=2*10^6: in run 2 a solution was found (seed=2960182613, osteps=1914331).
  • n=4850, cutoff=4*10^6: in run 3 a solution was found (seed=914035932, osteps=3424650).
  • n=4875, cutoff=4*10^6: in run 5 a solution was found (seed=2573294237, osteps=3164363).
  • n=4878, cutoff=4*10^6: in run 4 a solution was found (seed=2807257037, osteps=3921866).
  • n=4879, cutoff=4*10^6: in run 2 a solution was found (seed=1576343301, osteps=2941962).
  • n=4880, cutoff=4*10^6: in run 18 a solution was found (seed=865787531, osteps=1866108).
  • n=4881, cutoff=4*10^6: in run 6 a solution was found (seed=4090407979, osteps=2922175).
  • n=4888, cutoff=4*10^6: in run 1 a solution was found (seed=899655214, osteps=3135106).
  • n=4900, cutoff=4*10^6: in run 14 a solution was found (seed=4066642292, osteps=2874713).
  • n=4920, cutoff=4*10^6: in run 6 a solution was found (seed=1123326814, osteps=2867343).
  • n=4940, cutoff=4*10^6:
     0  2  3  4  5  6  7  8  9 10 11 12
     1  5  8  9  9 11 11  8  1  1  3  4
    71
       
    Peculiar, that here min=1 was not reached at all (a similar pattern was also observed for smaller n).
  • n=4960, cutoff=4*10^6:
     0  2  3  4  5  6  7  8  9 10 11 12 13 14 15
     1  2  2  3  5  7  3  1  1  3  2  1  3  1  1
    36
       
    (seed=2637190941, osteps=3082622).
  • n=4980
    1. cutoff=4*10^6:
       2  3  4  5  6  7  8  9 10 11 12 13 14 15 16
       4  6  6  7 19 10  7 11  6  7  8  4  1  2  2
      100
           
    2. cutoff=6*10^6: in run 34 a solution was found (seed=3797733747, osteps=4589183).
  • n=5000:
    1. cutoff=2*10^6 no longer sufficient (in 4 runs only min=10 was reached).
    2. Also with cutoff=4*10^6 in 6 runs only min=9 was reached.
    3. cutoff=6*10^6: in run 12 a solution was found (seed=480226455, osteps=4944068).
  • n=5025, cutoff=6*10^6: In run 79 a solution was found:
     0  1  2  3  4  5  6  7  8  9 10 11 13 14 16 17 18 20
     1  2  4  2  8  6 12 11  7  6  3  5  2  5  1  1  2  1
    79
       
  • n=5037, cutoff=6*10^6: In run 11 a solution was found (seed=1166271130, osteps=4644862).
  • n=5038, cutoff=6*10^6: In run 4 a solution was found (seed=1817616388, osteps=4885226).
  • n=5039
    1. cutoff=6*10^6:
       1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 17
       2  4  6  9  4  7 12 10 14  8  7  4  5  3  4  1
      100
           
    2. cutoff=8*10^6: In run 4 a solution was found (seed=3337162132, osteps=7422949). </li
  • n=5040
    1. cutoff=6*10^6:
       1  3  4  5  6  7  8  9 10 11 12 13 14 15 16 18 21
       3  4  9  7 12  8  7  9  8 13  6  4  1  3  4  1  1
      100
           
    2. cutoff=8*10^6: In run 73 a solution was found (seed=1520163615, osteps=2557823).
  • n=5044
    1. cutoff=6*10^6
       1  2  3  4  5  6  7  8  9 10 11 12 13 15 16 21 22
       2  1  5  5  9 11  4 14  6 14 11  5  4  3  4  1  1
      100
           
    2. cutoff=8*10^6: In run 18 a solution was found (seed=3627982560, osteps=5531534).
  • n=5050:
    1. cutoff=6*10^6:
       2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 19 22
       2  5  6 11  6 15  5  6 14  6  3  4  6  4  3  2  1  1
      100
           
    2. cutoff=8*10^6:
       1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17
       3  5  4  9  9 17 10 10 13  3  4  3  3  4  1  1  1
      100
           
      In another 53 runs a solution was found (seed=4228182136, osteps=5806766).
  • n=5100:
    1. cutoff=6*10^6:
       4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 23 24
       4  5  1  5  7 12  7  8  5  8  9  3  4  4  3  7  3  3  1  1
      100
           
    2. cutoff=8*10^6:
       2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 19 20
       6  3  3  2  8 10  6 13  7  8  8  9 10  2  1  1  2  1
      100
           
    3. cutoff=10^7:
       1  3  4  5  6  7  8  9 10 11 12 13 14 15 17 19
       1  1  6 12 10 11  9 11 11 10  6  2  3  4  2  1
      100
           
    4. cutoff=12*10^6: Found a solution in run 21 (seed=3386167483, osteps=11712754).
  • n=5200, cutoff=12*10^6: In run 70 a solution was found (seed=918366649, osteps=10327030). The second lowest min-value was 4 (attained once).
  • n=5212, cutoff=22*10^6: Found a solution in run 63 (seed=3872761921, osteps=20471010).
  • n=5218, cutoff=22*10^6: Found a solution in run 11 (seed=2271186552, osteps=14944821).
  • n=5221, cutoff=22*10^6: Found a solution in run 18 (seed=2464071714, osteps=16846617).
  • n=5222
    1. Determining the best Ubcsat-algorithm (cutoff=10^6):
      > E = run_ubcsat("GreenTao_N_3-4-4-4_5222.cnf", cutoff=1000000,runs=100)
      > plot(E$alg,E$best)
      > eval_ubcsat_dataframe(E)
      
      rnovelty :
       29  35  36  38  40  41  43  44  46  47  48  49  50  51  52  53  54  56  57  58
        1   1   2   2   1   3   3   1   4   1   2   5   7   2   2   3   4   2   3   2
       59  60  61  62  63  64  65  66  67  68  69  70  72  73  74  75  77  78  79  81
        2   1   1   2   3   3   1   3   1   5   1   1   1   1   1   3   1   1   3   1
       83  86  89  90  92  93  94 102 105 108 117
        1   1   1   2   1   1   2   1   1   1   1
      rnoveltyp :
       32  35  38  39  40  41  42  43  44  45  46  47  48  49  51  52  53  54  55  56
        1   1   2   3   2   1   2   1   1   1   1   2   1   3   2   1   4   4   1   2
       57  58  59  60  61  62  63  64  65  66  67  68  70  71  73  74  75  76  77  79
        3   4   4   4   2   2   3   1   4   2   3   1   4   4   1   4   1   1   1   3
       81  82  83  84  85  86  87  88  95 104 110
        1   1   1   1   2   1   1   1   1   1   1
           
      so the choice of rnovelty+ seems alright.
    2. cutoff=22*10^6:
       1  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 22
       1  1  2 10  4 12  6  7 14 10  8  6  3  2  6  2  3  1  1  1
      100
           
    3. cutoff=30*10^6: in run 55 a solution was found (seed=778376479, osteps=21573027).
    4. It seems that here rnovelty+ scales very "precisely".
  • n=5223, cutoff=30*10^6: In 44 runs 3 solutions were found ( seed=989195251, osteps=12842765).
  • n=5224, cutoff=30*10^6: in 24 runs one solution was found (seed=1146463992, osteps=27161246).
  • n=5225, cutoff=22*10^6:
     2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 18 20 21
     2  3  5  6  5 12  7 16  8  9  5  3  5  5  5  2  1  1
    100
     1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 17 18 19 21
     1  1  6  4  7  7  9  9  7 15  7  5  3  3  7  4  2  2  1
    100
       
  • n=5230, cutoff=30*10^6: In 148 runs 6 solutions found (seed=4260631635, osteps=17640659).
  • n=5240, cutoff=30*10^6: In 13 runs 2 solutions found (seed=1341336538, osteps=18643682).
  • n=5250
    1. cutoff=12*10^6
       6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 27 28 29 33
       1  2  7  3  3  3  9  4 10  3  7  6  7  4  8  7  4  2  1  4  1  2  1  1
      100
           
    2. cutoff=22*10^6
       1  3  4  5  6  7  8  9 10 11 12 13 14 15 17 18 19 20 21 22
       1  3  1  3  1  5  9 12  7 13  8 10  7  7  5  4  1  1  1  1
      100
           
    3. cutoff=30*10^6: in 125 runs one solution was found (seed=3082049509, osteps=22913634). And in another 68 runs another solution was found (seed=1854998832, osteps=22610568).
  • n=5300
    1. cutoff=12*10^6:
       5 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 32 35
       1  4  3  4  5  4  7  8  3  6  9  3  6  6  6  5  3  5  2  3  2  3  1  1
      100
           
    2. cutoff=14*10^6:
       6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 28 29 30 31 34
       2  1  1  2  5  1  5  3  7  7  7  4  8  6  8  4  4  5  7  5  2  2  1  1  1  1
      100
           
    3. cutoff=16*10^6:
       4  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
       1  2  2  2  3  3  6  5  4  6  8  9  6  8  5  4  1  3  3  7  6  2  1  2  1
      100
           
    4. cutoff=18*10^6:
       5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 27 33
       1  1  1  3  5  1  4  4 11  6  6  8 14  5  4  8  6  2  5  2  1  1  1
      100
           
    5. cutoff=20*10^6:
       5  6  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 29 30
       1  1  7  3  7  6  6 12  5 10  7  2  8  4  1  2  4  5  1  5  1  1  1
      100
           
    6. cutoff=22*10^6:
       3  4  5  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 26 27
       1  2  1  6  3  1  6  2 10  8 10  7  5  9  9  7  3  2  2  2  2  1  1
      100
           
    7. cutoff=30*10^6:
       2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22
       1  2  2  3  3  6  9 10  9  6  5  7 11  3  8  4  5  3  1  1  1
      100
       2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 26
       1  2  3  2  5  6  7  9  6 14  9  8 11  5  4  1  1  1  2  1  1  1
      100
           
    8. cutoff=40*10^6:
       1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19
       1  2  7  2  5  6 12  7  7  4 10  6  9  3  6  1  1  1  1
      91
           
    9. cutoff=50*10^6:
       0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 17
       1  5  3  7  7 10  9  6  5  9  8  5  2  6  4  4  1
      92
           
      (seed=909863827, osteps=46960523).
  • n=5400
    1. cutoff=50*10^6:
       1  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
       1  2  1  2  2 11  8 13 16 13 13 11 16 14 31 19 13 12 10  5  5  3  3  1  1
      226
           
    2. cutoff=60*10^6:
       3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 25
       1  6  1  6  9 14 12 21 12 19 15 14 19 14 16 12  5  2  4  1  1  1
      205
           
    3. cutoff=70*10^6:
       1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22
       1  2  6  7  7  7 10 16 11 15 16 22 14 17 14  8  4  4  5  4  5  3
      198
           
    4. In 21 runs with cutoff=100*10^6 one solution was found (seed=1345591531, osteps=62329976).
  • n=5500
    1. cutoff=80*10^6:
       5  7  9 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 30
       1  3  1  3  2  4  2  8 10  7  3 10 10  6  6  5 11  2  4  1  1
      100
           
    2. cutoff=90*10^6:
       7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 28 30
       1  1  2  2  3  1  2  7  8  3 12  9 11  6  9  9  2  3  4  2  2  1
      100
           
    3. cutoff=100*10^6:
       5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 26 27 28
       1  1  3  1  3  1  4  5  5  7  8 12  7  4  7  4  6  6  6  2  5  1  1
      100
           
    4. cutoff=150*10^6:
       4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
       1  1  1  5  4  5  5  6  7  8  7 13 12  8  4  3  2  5  1  1  1
      100
           
    5. cutoff=200*10^6:
       2  3  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21
       1  2  2  2  4  6  8 13 10  4  9  8  9  4  4  3  2  1
      92
           
    6. cutoff=250*10^6:
       0  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 23
       1  2  3  3  8  5  4  7  3 10 11  8  7  4  6  5  3  1  2  1
      94
           
      (seed=2262234995, osteps=166756114).
  • n=5600:
    1. cutoff=150*10^6:
       8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
       2  1  1  1  6  1  7  5 11 12 19  9 22 20 32 28 30 28 16 22 22 22 16 19  9  7
      34 35 36
       4  5  1
      378
           
    2. cutoff=200*10^6:
       8  9 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  2  2  2  1  5  7  5  9 17 21 20 17 20 22 15 26 25 13 25  7  5  5  5  3  1
      35
       2
      283
           
    3. cutoff=250*10^6:
       7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
       2  2  3  2  2 10  4  4 14 10 17 22 17 24 28 26 25 29 17 17  8  8  6  1  3  2
      33
       1
      304
           

Definition in file GreenTao_3-4-4-k.hpp.