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

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

Go to the source code of this file.

## Detailed Description

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

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

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

Todo:
greentao_3(3,4,4) > 1662
• Creating problems via output_greentao_stdname([3,4,4],n).
• n=600 trivially satisfiable.
• n=700 trivially satisfiable.
• n=900 trivially satisfiable.
• n=1000 trivially satisfiable.
• n=1100 still easy to solve (cutoff=100*10^3).
• n=1200 still easy to solve (cutoff=10^6).
• n=1300 rather easy to solve (cutoff=10^6).
• n=1400: one solution in 10 runs with cutoff=10^6.
• n=1500: only min=3 for 10 runs with cutoff=10*10^6; cutoff=100*10^6 found a solution in the third run (osteps=39412430, seed=1928236138).
• n=1512: one run in 10 with cutoff=100*10^6 found a solution (osteps=37551993, seed=4046775428). While another 100 runs with this cutoff actually found no solution.
• n=1518
1. 9 runs with cutoff=100*10^6 yield only a minimum of 2.
2. cutoff=500*10^6: run 18 found a solution (osteps=309459026, seed=3122222825).
• n=1525
1. 10 runs with cutoff=100*10^6 yield only min=2.
2. cutoff=500*10^6: run 16 yields a solution (msteps=375313903, seed=2274305602).
• n=1531: cutoff=5*10^8 yields a solution (seed=1692755539) in run 12.
• n=1532
1. cutoff=5*10^8 yields in 10 runs only once min=1.
2. cutoff=10^9 yields in run 15 a solution (seed=1453937791).
• n=1534
1. cutoff=5*10^8 yields in 23 runs only 4 times min=1.
2. cutoff=10^9 yields in run 6 a solution (seed=1913394293).
• n=1535
1. cutoff=10^9 yields in 9 runs only min=2.
2. cutoff=2*10^9 yields in run 18 a solution (seed=238771004, osteps=47373687).
• n=1537
1. 16 runs with cutoff=5*10^8 only yield min=1 twice.
2. cutoff=10^9 yields in 12 runs min=1 twice, so a cutoff of 2*10^9 would be needed.
3. cutoff=10^8, 1000 runs: In run 213 a solution was found (seed=2884500780, osteps=42486702).
• n=1538
1. cutoff=10^9: 2 solutions found with 214 runs (seed=1006777768, osteps=507922529).
• n=1539
1. cutoff=10^9: one solution found in 34 runs (seed=2866671762, osteps=167931793).
• n=1540: cutoff=10^9 found two solutions in 164 runs (seed=163883519, osteps=337015990).
• n=1541
1  2  3  5
2 13  1  1
17
> summary(E\$osteps)
Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
204200000 287600000 469700000 496300000 700700000 900400000

2. Further 51 runs found one solution (seed=1306721667, osteps=428867613).
• n=1542: cutoff=10^9 (adaptnovelty+): one solution found in 148 runs (seed=1219495006, osteps=466488791).
• n=1543: cutoff=10^9: in 474 runs one solution was found (seed=2142163637, osteps=918202991). It seems we need to double the cutoff.
• n=1544: cutoff=2*10^9
1   2   3
41 137   6
184
0   1   2   3   4
1  63 261  22   1
348

(seed=2955200386, osteps=664563809).
• n=1545:
1  2  3
13 35  4
52
1  2  3
28 87  8
123

2. Weak standard nested, rnovelty+, cutoff=10^7: found a solution in the first run (seed=1652015207, osteps=1816932).
• n=1550
1. Looks (at first sight) unsatisfiable: 10 runs with cutoff=10^8 yield min=3 (twice; so cutoff=10^9 would be needed).
2. cutoff=5*10^8: 13 runs only yield min=2, so a cutoff of 2.5*10^9 would be needed.
3. cutoff=10^8, 1000 runs yields
1   2   3   4   5   6   7   8   9
1  17  75 123 166 241 232 133  12
1000

so perhaps 100 * 1000 runs would be needed to find a solution.
4. cutoff = 10^9 yields
1  2  3  4  5  6
5 46 35  6  6  2
100

5. Weak standard nested, rnovelty+, cutoff=10^7:
0   1   2   3
243 212  42   3
500
> summary(E\$osteps[E\$min==0])
Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
599300 3286000 4930000 5318000 7516000 9961000

• n=1600: Weak standard nested, rnovelty+, cutoff=10^7 found a solution in run 21 (seed=2913780691, osteps=8089572).
• n=1650:
1. Weak standard nested, rnovelty+, cutoff=10^7:
2  3  4  5  6  7  8  9 10 11 12 13 14 15 16
3  3 20 29 56 68 86 77 50 50 26 12  9 10  1
500

2. cutoff=2*10^7:
0  2  3  4  5  6  7  8  9 10 11 12 13
1  1 14 41 57 84 68 51 32 11  5  3  1
369

(seed=3892552022, osteps=16215921).
3. Best local search algorithm from Ubcsat-suite:
E = run_ubcsat("GreenTao_N_3-3-4-4_1650.cnf", runs=200,cutoff=1000000)

evaluated by plot(E\$alg,E\$best):
> table(E\$best[E\$alg=="rnoveltyp"])
6  7  8  9 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
1  1  2  3  8  3  4  9 11  8 14 12 18 17 12 13  8 12  9  3  6  7  6  4  5  1
33 37
2  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 28 29 30 31 32 33
1  1  5  4  6 11  6  9  7 12  7 13 15 10 11 14 14  9  6  8 11  3  4  7  1  1
34 35 40
2  1  1
> table(E\$best[E\$alg=="walksat_tabu"])
12 15 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
1  1  1  2  1  1  6  4 13 13 19 17 14 14 19 19 13  9  7  9  6  6  1  3  1

confirming that rnovelty+ seems best here.
• n=1660: weak standard nested translation, rnovelty+ with cutoff=16*10^7 found in 157 runs one solution (seed=3193141014, osteps=87677992), while with cutoff=32*10^7 in 39 runs only min=2 was reached.
• n=1661: weak standard nested translation, rnovelty+
1. cutoff=32*10^7:
2  3  4  5
12 40 40  7
99
1  2  3  4  5  6
1 17 62 48 10  2
140

2. cutoff=64*10^7
1  2  3  4
2 12 23  7
48

In further 15 runs one solution was found (seed=3028693870, osteps=187092298).
• n=1662: weak standard nested translation, rnovelty+, cutoff=64*10^7 found a solution in 38 runs (seed=1319314469, seed=298802296).
• n=1663: weak standard nested translation, rnovelty+
1. cutoff=64*10^7
1   2   3   4   5
9  63 131  50   5
258
1   2   3   4   5
4  61 150  74   2
291

2. cutoff=10^9
1  2  3  4
3 19 20  1
43

• n=1665: weak standard nested translation, rnovelty+
1. cutoff=16*10^7:
2  3  4  5  6  7  8
1  9 32 22  5  1  1
71
1  2  3  4  5  6  7
1  5 24 33 23  4  1
91

2. cutoff=32*10^7:
1  2  3  4  5  6
3 24 68 51 17  2
165

• n=1670
1. Weak standard nested, rnovelty+, cutoff=2*10^7:
1  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17
1  3  8 17 37 50 69 69 91 51 42 35 12 10  4  1
500

2. rnovelty+, cutoff=4*10^7:
3  4  5  6  7  8  9 10 11 14
2  4 17 21 35 26 14 12  7  1
139

3. rnovelty, cutoff=4*10^7:
2   3   4   5   6   7   8   9  10  11  12  13  14  15
2   4  23  37  82 117  98  77  34  19   3   2   1   1
500

4. rnovelty+, cutoff=8*10^7:
2   3   4   5   6   7   8   9  10
6  21  36 121 137 108  47  21   3
500

5. rnovelty, cutoff=8*10^7:
3  4  5  6  7  8  9 10 11
5 15 29 45 21 16  7  2  1
141

So rnovelty+ seems better.
6. rnovelty+, cutoff=16*10^7:
2   3   4   5   6   7   8
7  46 131 146 118  41   9
498
1   2   3   4   5   6   7   8
3   6  30 126 125  73  34   4
401

7. rnovelty+, cutoff=32*10^7:
1  2  3  4  5  6  7
2 10 21 55 45  8  1
142

5  7  8  9 10 11 13
2  5  3  7  5  6  1
29

Looks inappropriate.
Todo:
greentao_3(3,4,5) > 8300
• n=2000 trivial for adaptnovelty+ (70% success with cutoff=10^4).
• n=2200 trivial for adaptnovelty+ (70% success with cutoff=10^4).
• n=3000 trivial for adaptnovelty+ (90% success with cutoff=10^5).
• n=4000 simple for adaptnovelty+ (100% success with cutoff=10^6).
• n=5000 simple for adaptnovelty+ (40% success with cutoff=10^6).
• n=6000 simple for adaptnovelty+ (100% success with cutoff=10^7).
• n=7000
1. cutoff=10^7 yields min=4 in 10 runs.
2. cutoff=10^8: 100% success.
• n=7250: cutoff=10^8 found a solution in run 2 (seed=2722596453, osteps=65636246).
• n=7375: cutoff=10^8 found one solution in 20 runs (seed=161549167, osteps=73817861).
• n=7438: cutoff=10^8 found two solutions in 77 runs (seed=3688103311, osteps=67497802).
• n=7479: cutoff=10^8 finds a solution (seed=1752281516, osteps=79570476).
• n=7490: cutoff=10^8 finds one solution in 40 runs (seed=1381313198, osteps=32116058).
• n=7500:
1. cutoff=10^8:
> ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 100000000 -i GreenTao_3-3-4-5_7500.cnf | tee GreenTao_3-3-4-5_7500.cnf_OUT
2  4  5  7  8  9 10 12 13 14 16 18 19
1  5  3  2  3  1  1  1  1  1  2  1  2
24
> summary(E\$osteps)
Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
20480000 65180000 73430000 70900000 84870000 98250000

2. In further 110 runs one solution was found (seed=173131959, cutoff=85955523).
3. Let's increase the cutoff to 2*10^8.
• n=7600, cutoff=2*10^8 (adaptnovelty+): in 249 runs one solution was found (seed=3054809508, osteps=165824921). It seems one should double the cutoff.
• n=7650
2  5  6  7  8  9 10 11 12 14 15
1  2  4  2  1  3  4  2  2  3  2
26
2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17
1  4  8  1  7  4 10  9 15 18 11  2  4  1  2  3
100

2. Weak standard nested translation, rnovelty+, cutoff=10^6 finds a solution in the first run (seed=1527646207, osteps=920073).
• n=7700
3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 21
1  1  2  3  6  5  4  9 12 12 13 10  3  5  5  7  1  1
100
5  6  7  8  9 10 11 12 13 14 15 16 17 19
1  3  4  8  9 12 10 10 10 14  4  9  5  1
100
3  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21
1  1  2  2  3 10 13  7 10  8 12  6 12  3  2  3  2  3
100

2. Weak standard nested translation, rnovelty+, cutoff=2*10^6:
1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 18 23 26
5  2 18 18 19 21 23 29 22 10 11  8  5  2  7  1  1  1
203

while with cutoff=4*10^6 two solutions were found in 7 runs (seed=1076160763, osteps=3425039).
• n=7750, weak standard nested translation, rnovelty+, cutoff=4*10^6: In 92 runs 5 solutions were found (seed=3051660126, osteps=2154632).
• n=7900, weak standard nested translation, rnovelty+, cutoff=8*10^6: In 60 runs one solution was found (seed=2495938585, osteps=4986167).
• n=8000
1. cutoff=10^8, aloamo:
> ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 100000000 -i GreenTao_3-3-4-5_8000.cnf | tee GreenTao_3-3-4-5_8000.cnf_OUT
24 26 27 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 51 53
1  3  1  1  3  5  3  1  5  2  4  4  1  4  1  5  3  5  2  2  3  5  1  4  2  1
58
1
73
> summary(E\$osteps)
Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
15540000 37710000 68590000 64060000 84820000 99420000

looks unsatisfiable (although one might try cutoff=2*10^8).
2. Weak standard nested translation, rnovelty+, cutoff=16*10^6 find in 6 runs one solution (seed=3908229136, osteps=11449398).
• n=8100, weak standard nested translation, rnovelty+
1. cutoff=16*10^6: found in 91 runs no solution.
2. cutoff=32*10^6: found in 39 runs two solutions (seed=2882427028, osteps=23392210).
• n=8200, weak standard nested translation, rnovelty+
1. cutoff=32*10^6:
3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 19 20 24
2  1  6  1  7  9  7  5  2  9 10  1  2  2  3  2  1  1
71

Using cutoff=64*10^6, in run 10 a solution was found (seed=2296183965, cutoff=20180202).
• n=8250, weak standard nested translation, rnovelty, cutoff=2*10^8
• n=8300, weak standard nested translation, rnovelty+
1. cutoff=32*10^6:
5  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
1  1  1  1  1  2  3  6  3  2  1  6  3  5  5  4  1  1  3  5  1  1  1  2  2  1
31 33
1  3
67
7  8  9 10 11 12 13 14 15 16 17 19 20 21 22 23 25 27 28 29 32
1  1  2  5  1  1  3  3  5  5  5  2  3  1  2  1  2  1  1  2  1
48
5  9 10 11 12 13 14 15 16 17 18 19 20 22 23 24 26 27 28 29 32
1  2  3  3  3  3  1  1  2  4  6  3  2  2  1  1  1  1  2  1  2
45

2. cutoff=64*10^6:
5  6  7  8  9 10 11 12 13 14 15 16 17 19 21 26 32
3  1  5  4  4  3  5  4  1  6  3  4  1  3  1  1  1
50
3  5  6  8  9 10 11 12 14 15 16 17 20 22
1  1  1  1  2  2  3  3  2  1  1  1  3  2
24
2  3  5  6  7  8 10 11 12 13 14 15 17 18 19
1  1  2  1  7  3  3  8  1  1  4  4  2  1  2
41

3. cutoff=128*10^6:
2  3  4  5  6  7  8  9 11 13 14 15 17 18
1  4  3  5  2  9  4  4  1  3  2  2  2  1
43

4. cutoff=2*10^8
3 4 5 6 8 9 12
2 2 3 1 2 2  1
13
2  3  4  5  6  7  8  9 12
1  2  4  3  4  1  4  3  1
23

5. walksat-tabu-nonull using cutoff=128*10^6 reaches in 5 runs only a min=72, while in 6 runs with cutoff=256*10^6 only min=80 was reached.
6. Finding best algorithm from Ubcsat:
> E = run_ubcsat("GreenTao_N_3-3-4-5_8300.cnf",runs=100,cutoff=1000000)
> plot(E\$alg,E\$best)
> eval_ubcsat_dataframe(E)

rnovelty and rnovelty+ seem clearly best.
7. cutoff=2*10^8, rnovelty
1  2  3  4  5  6  7  8  9 10 11 12 15
2  3  5  7  3  5 13  8  3  1  2  2  1
55
1  2  3  4  5  6  7  8  9 10 11 12
2  3  6  5  8 12  3  7  4  1  2  2
55

So rnovelty seems better than rnovelty+.
8. cutoff=4*10^8, rnovelty: in run 68 a solution was found (seed=4131142001, osteps=350760305).
• n=8350, weak standard nested translation, rnovelty
1. cutoff=10^9:
1  2  3  4  5  6  7  8  9
2  6 17 18 17  8  3  1  1
73

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