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.