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

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

Go to the source code of this file.

Detailed Description

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

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

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

Todo:
greentao_3(3,3,4) >= 434
• Created by output_greentao_stdname([3,3,4],n) and output_greentao_sb_stdname([3,3,4],n).
• n=150 trivially satisfiable by adaptnovelty+.
• n=200 trivially satisfiable by adaptnovelty+.
• n=300 trivially satisfiable by adaptnovelty+.
• n=400 easily satisfiable by adaptnovelty+ (cutoff=100*10^3).
• n=412 found satisfiable by adaptnovelty+ with cutoff=10*10^6 (e.g., seed=573073979).
• n=419 found satisfiable by adaptnovelty+ with cutoff=10*10^6 (seed=1429074341).
• n=425 found satisfiable by adaptnovelty+ with cutoff=10*10^6 (40 runs needed; seed=610774669).
• n=428: cutoff=50*10^6 found a solution after 17 runs (seed=621103542).
• n=429: cutoff=50*10^6 yields 13 solutions in 358 runs (e.g., seed=2019144865).
• n=430: cutoff=50*10^6 yields 1 solution in 276 runs (seed=3076580871).
• n=431: cutoff=200*10^6 yields in 4 runs constantly min=1, and so does cutoff=50*10^6 in 10 runs, but using 730 runs (cutoff=50*10^6) one solution was found (seed=731527187).
• n=432: found satisfiable by adaptnovelty+ with cutoff=50*10^6 (seed=769951307, osteps=40681058); 1 solution in 1000 runs:
```Clauses = 20506
Variables = 1296
TotalLiterals = 61906
FlipsPerSecond = 753471
BestStep_Mean = 15526608.088000
Steps_Mean = 49990681.058000
Steps_Max = 50000000.000000
PercentSuccess = 0.10
BestSolution_Mean = 1.320000
BestSolution_Median = 1.000000
BestSolution_Min = 0.000000
BestSolution_Max = 2.000000
```
• n=433
1. cutoff=60*10^6 found in 175 runs one solution (seed=3663211116).
2. Until now only the aloamo-translation has been considered; the weak standard nested translation with rnovelty+ and cutoff=10*10^6 yields
``` 1  2
85 15
100
```
while cutoff=20*10^6 yields
```> E=read_ubcsat("GreenTao_N_3-3-3-4_433.cnf_OUT")
0   1  2
1 177  1
179
```
(seed=3770956838, osteps=19094627).
• n=434:
1. cutoff=60*10^6:
```> ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 60000000 -i GreenTao_3-3-3-4_434.cnf
Clauses = 20673
Variables = 1302
TotalLiterals = 62410
FlipsPerSecond = 754097
BestStep_Mean = 15831901.495000
Steps_Mean = 60000000.000000
Steps_Max = 60000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 1.467000
BestSolution_Median = 1.000000
BestSolution_Min = 1.000000
BestSolution_Max = 2.000000
```
2. cutoff=200*10^6:
```> ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 200000000 -i GreenTao/GreenTao_3-3-3-4_434.cnf
Clauses = 20673
Variables = 1302
TotalLiterals = 62410
FlipsPerSecond = 758972
BestStep_Mean = 58144942.258000
Steps_Mean = 200000000.000000
Steps_Max = 200000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 1.070000
BestSolution_Median = 1.000000
BestSolution_Min = 1.000000
BestSolution_Max = 2.000000
```
3. Let's finally consider a higher number of runs, 20000, but with just cutoff=50*10^6:
```> ubcsat-okl -alg adaptnovelty+ -runs 20000 -cutoff 50000000 -i GreenTao/GreenTao_3-3-3-4_434.cnf -solve | tee GreenTao_3-3-3-4.out
1     2
9253 10747
20000
```
So let's consider this case as "unsatisfiable".
4. OKsolver_2002
1. Without preprocessing and without symmetry-breaking:
```> OKsolver_2002-O3-DNDEBUG -M -D30 -F GreenTao_3-3-3-4_434.cnf
s UNKNOWN
c sat_status                            2
c initial_maximal_clause_length         4
c initial_number_of_variables           1302
c initial_number_of_clauses             20673
c initial_number_of_literal_occurrences 62410
c number_of_initial_unit-eliminations   0
c reddiff_maximal_clause_length         0
c reddiff_number_of_variables           0
c reddiff_number_of_clauses             0
c reddiff_number_of_literal_occurrences 0
c number_of_2-clauses_after_reduction   1302
c running_time(sec)                     6689.7
c number_of_nodes                       478637
c number_of_single_nodes                0
c number_of_quasi_single_nodes          0
c number_of_2-reductions                5829494
c number_of_pure_literals               0
c number_of_autarkies                   4810
c number_of_missed_single_nodes         19
c max_tree_depth                        113
c number_of_table_enlargements          0
c number_of_1-autarkies                 210768130
c number_of_new_2-clauses               0
c file_name                             GreenTao_3-3-3-4_434.cnf
```
average 2-reductions ~ 12.2, where 1302/12.2 ~ 107, while speed is 72 nodes per second.
2. With preprocessing and without symmetry-breaking:
```> OKsolver_2002-m2pp -M -D30 -F GreenTao_3-3-3-4_434.cnf
s UNKNOWN
c sat_status                            2
c initial_maximal_clause_length         8
c initial_number_of_variables           864
c initial_number_of_clauses             19175
c initial_number_of_literal_occurrences 65558
c number_of_initial_unit-eliminations   0
c reddiff_maximal_clause_length         0
c reddiff_number_of_variables           0
c reddiff_number_of_clauses             0
c reddiff_number_of_literal_occurrences 0
c number_of_2-clauses_after_reduction   432
c running_time(sec)                     87501.4
c number_of_nodes                       7410032
c number_of_single_nodes                8
c number_of_quasi_single_nodes          0
c number_of_2-reductions                89745142
c number_of_pure_literals               10442
c number_of_autarkies                   0
c number_of_missed_single_nodes         309
c max_tree_depth                        80
c number_of_table_enlargements          0
c number_of_1-autarkies                 1045400
c number_of_new_2-clauses               0
c file_name                             GreenTao_3-3-3-4_434.cnf_m2pp_19403
```
(without reaching a monitoring node); 2red/nds ~ 12.11, where 864 / 12.11 ~ 71, 84.7 nds/sec. This looks like an improvement.
3. Without preprocessing and with symmetry-breaking:
```> OKsolver_2002-O3-DNDEBUG -M -D30 -F GreenTao_sb_3-3-3-4_434.cnf
s UNKNOWN
c sat_status                            2
c initial_maximal_clause_length         4
c initial_number_of_variables           1302
c initial_number_of_clauses             20674
c initial_number_of_literal_occurrences 62412
c number_of_initial_unit-eliminations   0
c reddiff_maximal_clause_length         0
c reddiff_number_of_variables           0
c reddiff_number_of_clauses             0
c reddiff_number_of_literal_occurrences 0
c number_of_2-clauses_after_reduction   1303
c running_time(sec)                     146231.2
c number_of_nodes                       12297953
c number_of_single_nodes                0
c number_of_quasi_single_nodes          0
c number_of_2-reductions                151996719
c number_of_pure_literals               0
c number_of_autarkies                   116929
c number_of_missed_single_nodes         445
c max_tree_depth                        120
c number_of_table_enlargements          0
c number_of_1-autarkies                 5390584354
c number_of_new_2-clauses               0
c file_name                             GreenTao_sb_3-3-3-4_434.cnf
```
(without reaching a monitoring node); 2red/nds ~ 12.36, where 1302 / 12.36 ~ 105, 84.1 nds/sec. Looks worse than with preprocesssing, while slightly better than without anything.
4. With preprocessing and with symmetry-breaking:
```> OKsolver_2002-m2pp -M -D30 -F GreenTao_sb_3-3-3-4_434.cnf
s UNKNOWN
c sat_status                            2
c initial_maximal_clause_length         8
c initial_number_of_variables           864
c initial_number_of_clauses             19175
c initial_number_of_literal_occurrences 65558
c number_of_initial_unit-eliminations   0
c reddiff_maximal_clause_length         0
c reddiff_number_of_variables           0
c reddiff_number_of_clauses             0
c reddiff_number_of_literal_occurrences 0
c number_of_2-clauses_after_reduction   432
c running_time(sec)                     105686.7
c number_of_nodes                       7765574
c number_of_single_nodes                7
c number_of_quasi_single_nodes          0
c number_of_2-reductions                94065922
c number_of_pure_literals               10670
c number_of_autarkies                   0
c number_of_missed_single_nodes         319
c max_tree_depth                        81
c number_of_table_enlargements          0
c number_of_1-autarkies                 1081511
c number_of_new_2-clauses               0
c file_name                             GreenTao_sb_3-3-3-4_434.cnf_m2pp_9920
```
(without reaching a monitoring node); 2red/nds ~ 12.11, where 864 / 12.11 ~ 71, 73.5 nds/sec. Apparently the preprocessing actually got rid off the added (one) symmetry-breaking clause, and no traces left??
5. minisat2: also looks hopeless:
```> minisat2 GreenTao_3-3-3-4_434.cnf
| 1474310789 |     864    19175    65558 |   262983   177338     59 |  0.000 % |
*** INTERRUPTED ***
restarts              : 40
conflicts             : 1575350950     (544 /sec)
decisions             : 1884366472     (1.86 % random) (651 /sec)
propagations          : 83941261019    (29000 /sec)
conflict literals     : 94551775063    (16.96 % deleted)
Memory used           : 386.03 MB
CPU time              : 2.89452e+06 s
```
6. So to determine unsatisfiability here, new ideas/algorithms are needed.
7. The above is all for the aloamo-translation. Now we consider the weak standard nested translation.
8. Best Ubcsat-solver:
```> E = run_ubcsat("GreenTao_N_3-3-3-4_434.cnf", runs=100,cutoff=1000000)
> plot(E\$alg,E\$best)
> eval_ubcsat_dataframe(E)

rnoveltyp :
1  2  3  4
8 44 42  6
1  2  3  4
7 44 39 10
rnovelty :
1  2  3  4
6 53 33  8
noveltyp :
1  2  3  4  5
4 25 54 15  2
novelty :
1  2  3  4
3 36 53  8
gwsat :
1  2  3  4  5  6  7
1  5 22 40 21 10  1
```
9. rnovelty+ with cutoff=4*10^6:
```> E=read_ubcsat("GreenTao_N_3-3-3-4_434.cnf_OUT")
1  2
61 39
100
```
10. rnovelty+ with cutoff=2*10^7:
```> E=read_ubcsat("GreenTao_N_3-3-3-4_434.cnf_OUT")
1   2
877 123
1000
```
11. OKsolver_2002 (without symmetry-breaking and without preprocessing): looks hopeless; same with preprocessing (apparently not much is changed).
12. minisat2: looks hopeless:
```| 436832686 |     864    18743    90269 |   193132    29758     43 |  0.000 % |
*** INTERRUPTED ***
restarts              : 37
conflicts             : 437344653      (786 /sec)
decisions             : 496767675      (1.91 % random) (893 /sec)
propagations          : 16236183376    (29195 /sec)
conflict literals     : 21117220859    (27.85 % deleted)
Memory used           : 114.55 MB
CPU time              : 556126 s
```
• n=437
1. cutoff=10*10^6 with 65 runs only achieved 5 times min=1.
2. cutoff=100*10^6 with 10 runs achieved 6 times min=1 and 4 times min=2. More runs:
```> ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 100000000 -i GreenTao_3-3-3-4_437.cnf
Clauses = 20918
Variables = 1311
TotalLiterals = 63157
FlipsPerSecond = 748371
BestStep_Mean = 29088565.360000
Steps_Mean = 100000000.000000
Steps_Max = 100000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 1.330000
BestSolution_Median = 1.000000
BestSolution_Min = 1.000000
BestSolution_Max = 2.000000
```
3. cutoff=10^9 doesn't seem effective:
```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_3-3-3-4_437.cnf
Clauses = 20918
Variables = 1311
TotalLiterals = 63157
FlipsPerSecond = 724933
BestStep_Mean = 91967835.900000
Steps_Mean = 1000000000.000000
Steps_Max = 1000000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 1.000000
BestSolution_Median = 1.000000
BestSolution_Min = 1.000000
BestSolution_Max = 1.000000
```
where the maximum of osteps is 170234040.
4. So if this n is to be considered further, then with 1000 runs and a cutoff of 200*10^6: Aborted after 440 runs, with most of them yielding min=1 and some min=2.
• n=450
1. ```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_3-3-3-4_450.cnf
Clauses = 22012
Variables = 1350
TotalLiterals = 66488
FlipsPerSecond = 799233
BestStep_Mean = 4388254.200000
Steps_Mean = 10000000.000000
Steps_Max = 10000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 3.300000
BestSolution_Median = 3.000000
BestSolution_Min = 3.000000
BestSolution_Max = 4.000000
> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_3-3-3-4_450.cnf
Clauses = 22012
Variables = 1350
TotalLiterals = 66488
FlipsPerSecond = 761899
BestStep_Mean = 23395422.200000
Steps_Mean = 100000000.000000
Steps_Max = 100000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 2.100000
BestSolution_Median = 2.000000
BestSolution_Min = 2.000000
BestSolution_Max = 3.000000
> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_3-3-3-4_450.cnf
Clauses = 22012
Variables = 1350
TotalLiterals = 66488
FlipsPerSecond = 718685
BestStep_Mean = 436206673.400000
Steps_Mean = 1000000000.000000
Steps_Max = 1000000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 1.500000
BestSolution_Median = 1.500000
BestSolution_Min = 1.000000
BestSolution_Max = 2.000000
```
2. This needs to be investigated further, but first we look at smaller n.
3. Since osteps for cutoff=10^9 comes close to the cutoff value, let's try 10 runs with cutoff=4*10^9.
• n=500 looks unsatisfiable: cutoff=100*10^3 and 10 runs yields a minimum=14, cutoff=10^6 yields minimum=8, cutoff=10*10^6 yields minimum=7.
Todo:
greentao_3(3,3,5) > 1989
• For n > 1000 one needs to use
```set_heap_size_ecl(2^30);
```
• n=1000 easy for adaptnovelty+ with cutoff=100000.
• n=1200 easy for adaptnovelty+ with cutoff=100000.
• n=1400 easy for adaptnovelty+ with cutoff=10^6.
• n=1600 easy for adaptnovelty+ with cutoff=10^6.
• n=1800
• cutoff=10^6 yields in 10 runs min=3.
• cutoff=5*10^6 found in 10 runs one solution (seed=992240675).
• n=1850
1. cutoff=5*10^6 yields in 10 runs min=2.
2. cutoff=25*10^6 found in 10 runs one solution (seed=2209127524).
• n=1875: cutoff=10^8 found in run 6 a solution (seed=195078017).
• n=1887: cutoff=2*10^8 produced 5 solutions in 100 runs (e.g., seed=2857056001, osteps=22392426
• n=1900
1. cutoff=25*10^6 yields in 10 runs only min=2.
2. cutoff=10^8 yields in 10 runs min=1 twice; so could be investigated using more runs.
3. cutoff=2*10^8: 100 runs min=1, max=3, mean=1.77.
4. cutoff=4*10^8 found in 54 runs one solution (seed=1090357734, osteps=5547490).
• n=1910: cutoff=4*10^8 found in 59 runs one solution (seed=3723062408, osteps=187616262).
• n=1920: cutoff=4*10^8 found in 49 runs one solution (seed=1165735423, osteps=232394841).
• n=1921:
1. cutoff=10^9:
```> E2 = read_ubcsat("GreenTao_3-3-3-5_1921.cnf_OUT")
1  2  3
19 78  3
100
1   2   3
167 612  27
806
```
2. cutoff=2*10^9: In 27 runs one solution was found (seed=4076787552, osteps=1932855399).
3. So apparently a higher cutoff is needed.
• n=1925
1. cutoff=10^9 yields
```> E2 = read_ubcsat("GreenTao_3-3-3-5_1925.cnf_OUT")
1  2  3
8 59  9
76
1  2  3
11 79 10
100
```
2. cutoff=2*10^9: 76 runs yield
``` 1  2  3
13 62  1
```
Another 57 runs yield
``` 0  1  2
1 11 45
57
```
(the solution has osteps=857758539 and seed=4288803153)
• n=1926 found satisfiable (seed=1969942517, osteps=1115197460).
• n=1927
1. cutoff=4*10^9
``` 1  2
36 64
100
```
another 19 runs found one solution (seed=3593018407, osteps=138183620).
• n=1928, cutoff=4*10^9: In 100 runs one solution was found (seed=733180643, osteps=3800942926).
• n=1929 found satisfiable (seed=1305993935, osteps=2072609418):
```> E = read_ubcsat("GreenTao_3-3-3-5_1929.cnf_OUT")
0   1   2   3
1  32 109   2
144
```
• n=1930
1. cutoff=4*10^8 yields (length, table)
```[1] 100
1  2  3  4
2 40 57  1
```
2. cutoff=10^9 yields
```E = read_ubcsat("GreenTao_3-3-3-5_1930.cnf_OUT2")
1  2  3
4 69 27
100
```
3. cutoff=2*10^9
```E = read_ubcsat("GreenTao_3-3-3-5_1930.cnf_OUT3")
1 2 3
3 5 1
9
1  2  3
10 84  6
100
1  2  3
1 14  2
17
```
4. Now with cutoff=4*10^9: 131 runs yield 23 times min=1 (rest min=2). In another 405 runs one solution was found (seed=2789358783, osteps=2164367412).
• n=1931:
``` 1  2  3
5 29  1
35
```
2. Weak nested translation, rnovelty+, cutoff=10^7: In run 6 a solution was found (seed=1383005715, osteps=9198721).
• n=1940
1. Weak nested translation, rnovelty+, cutoff=10^7:
``` 0  1  2  3  4  5  6  7
1  5 13 23 32 19  5  2
100
```
(seed=1131255522, osteps=7633695).
2. cutoff=2*10^7:
``` 0  1  2  3  4  5
1  7 34 34 19  5
100
```
(seed=2316712870, osteps=1698213).
3. Best ubcsat-solver: Evaluating
```E = run_ubcsat("GreenTao_N_3-3-3-5_1940.cnf", runs=200,cutoff=1000000)
```
by plot(E\$alg,E\$best):
```> table(E\$best[E\$alg=="rnovelty"])
2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 19
2  2  8  6 19 24 28 24 22 23 14 14  3  3  2  4  2
> table(E\$best[E\$alg=="rnoveltyp"])
3  4  5  6  7  8  9 10 11 12 13 14 15 16 17
6  4 11 22 31 16 29 23 23 17  4  7  2  3  2
> table(E\$best[E\$alg=="walksat_tabu_nonull"])
5  6  7  8  9 10 11 12 13 14 15 16 17 19 20
2  2  2 10 20 16 22 28 29 28 23 11  5  1  1
> table(E\$best[E\$alg=="walksat_tabu"])
5  6  7  8  9 10 11 12 13 14 15 16 17 22
1  1 12  6 13 19 17 32 34 32 20  9  3  1
```
• n=1950:
1. Weak standard nested translation, rnovelty+, cutoff=10^7:
``` 0  1  2  3  4  5  6  7  8
1 11 18 51 57 31 22  7  2
200
```
(seed=4280674293, osteps=2424310).
2. Weak standard nested translation, rnovelty+, cutoff=2*10^7:
``` 1  2  3  4  5  6
8 38 54 67 28  5
200
```
• n=1960: Weak standard nested translation, rnovelty+, cutoff=10^7:
```  1   2   3   4   5   6   7   8   9
9  36  67 110 113  54  16   6   2
413
```
while with rnovelty (also cutoff=10^7):
```  0   1   2   3   4   5   6   7   8   9
1   9  26  75 103 119  56  24   8   1
422
```
(seed=2613143980, osteps=8752208). Finally with rnovelty and cutoff=10^8 a solution was found in 31 runs.
• n=1970
1. Weak standard nested translation, rnovelty+, cutoff=10^7:
``` 1  2  3  4  5  6  7  8  9
1  3 19 45 47 63 24 12  4
218
```
2. Weak standard nested translation, rnovelty, cutoff=10^7:
``` 2  3  4  5  6  7  8  9 11
9 40 59 60 43 42 10  6  1
270
```
• n=1970: Weak standard nested translation with rnovelty+ and cutoff=10^8 found a solution (seed=3847181900, osteps=15562348).
• n=1980: Weak standard nested translation with rnovelty+ and cutoff=10^8 found 2 solutions in 70 runs (seed=1878198536, osteps=10033702), while rnovelty with the same cutoff found none in 71 runs (and no min=1 in 18 runs with cutoff=2*10^8), so rnovelty+ seems better.
• n=1985, weak standard nested translation, rnovelty+, cutoff=10^8: finds one solution in 74 runs (seed=280301594, osteps=85326534) (while 63 runs with cutoff=2*10^8 didn't find a solution).
• n=1986, weak standard nested translation, rnovelty+, cutoff=10^8: in 374 runs two solutions were found (seed=2398771372, osteps=42038499).
• n=1987, weak standard nested translation, rnovelty+:
1. cutoff=10^8:
```  1   2   3   4   5   6
5  33 101 106  28   5
278
1   2   3   4   5   6
9  20  91 111  43   3
277
```
2. cutoff=2*10^8:
```1 2 3 4
2 7 8 8
25
```
In another 23 runs one solution was found (seed=2461337687, osteps=171230996).
• n=1988, weak standard nested translation, rnovelty+
1. cutoff=2*10^8:
``` 1  2  3  4  5
9 16 41 19  1
86
1  2  3  4
1 20 36 28
85
1  2  3  4  5  6
4 10 37 14  2  1
68
```
2. cutoff=4*10^8: In altogether 226 runs one solution was found (seed=2410474560, osteps=75173657; while 18 runs with cutoff=8*10^8 didn't find a solution).
• n=1989, weak standard nested translation, rnovelty+:
1. cutoff=10^8: in 17 runs one solution was found (seed=2102824829, osteps=59988664).
2. cutoff=4*10^8: 21 runs didn't find a solution.
• n=1990, weak standard nested translation:
1. rnovelty+, cutoff=10^8:
```  1   2   3   4   5   6
5  48 160 206  70  11
500
1   2   3   4   5   6   7
6  63 163 178  80   9   1
500
1   2   3   4   5   6   7
10  76 201 250 104   9   1
651
```
2. rnovelty+, cutoff=2*10^8:
``` 1  2  3  4  5
2 28 45 23  2
100
```
3. rnovelty+, cutoff=4*10^8:
``` 1  2  3  4
9 53 79 15
156
1  2  3  4
8 63 83 10
164
```
Todo:
Upper bounds
• Running minisat2 on GreenTao_3-3-3-4_431.cnf for a day (33 restarts) doesn't seem to make progress.
• We now need to investigate GreenTao_3-3-3-4_434.cnf further.
• Apparently the symmetry-breaking clause doesn't make things easier for minisat2.
• Running OKsolver_2002-O3-DNDEBUG / -m2pp with "-M -D20" for a while doesn't show any progress (max_tree_depth=104 resp. 68 reached, and the bit symmetry-breaking shouldn't make a big difference; the only positive thing here is that some autarkies are found (in the non-preprocessed case; but we can't see how efficient they are).

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