OKlibrary  0.2.1.6
GreenTao_2-3-7.hpp File Reference

Investigations on greentao_2(3,7) More...

Go to the source code of this file.

## Detailed Description

Investigations on greentao_2(3,7)

Problems are generated by output_greentao2nd_stdname(3,7,n) at Maxima level, or by "GTSat 3 7 n" at C++ level.

Todo:
Finding the best algorithm from ubcsat
Todo:
Survey propagation
• For n=5000, 7500, 10000, 12500 survey propagation apparently thinks the problem is unsatisfiable, i.e., we always get
```> survey_propagation -l GreenTao_2-3-7_XX000.cnf
<bias>:nan
fixed 1 biased var (+0 ucp)
.:-)
<bias>:nan
```
However these problems are all satisfiable.
• the same behaviour for n=15000 (but here we don't know whether it's satisfiable).
Todo:
greentao_2(3,7) > 13800
• n=5000: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=10000.
• n=7500: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=100000.
• n=10000: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=1000000 (seed=3610283050).
• n=12500
1. ```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2-3-7_12500.cnf
Clauses = 4722593
Variables = 12500
TotalLiterals = 14173471
FlipsPerSecond = 6550
BestStep_Mean = 779318.300000
Steps_Mean = 1000000.000000
Steps_Max = 1000000.000000
PercentSuccess = 0.00
BestSolution_Mean = 14.200000
BestSolution_Median = 14.000000
BestSolution_Min = 8.000000
BestSolution_Max = 19.000000
```
2. Found satisfiable (first run) with cutoff=10*10^6 (seed=348690330).
• n=13750
1. A cutoff=100*10^6 yields in 10 runs a minimum of 2 and a maximum of 4.
2. cutoff=10^9:
```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_2-3-7_13750.cnf
sat  min     osteps     msteps       seed
1 0     2  162139042 1000000000 1446773825
2 0     1  481815784 1000000000 3328367368
3 1     0  569156743  569156743 1397463094
```
• n=13800
1. cutoff=10^8: In 36 runs one solution was found:
```> E = read_ubcsat("GreenTao_2-3-7_13800.cnf_OUT2")
0  1  2  3  4
1  3 10 17  5
36
> E[E\$min==0,]
sat min   osteps   msteps      seed
21   1   0 77868065 77868065 793605254
```
2. cutoff=10^9: three runs yield twice min=1 and once min=2.
3. cutoff=2*10^9: one run yields min=2.
4. So perhaps a cutoff=10^8 is more appropriate here.
• n=13825
``` 1  2  3  4  5
2 24 56 37  8
127
1  2  3  4  5
1 25 51 47  3
127
\endverbartim
</li>
</ol>
</li>
<li> n=13850
<ol>
\verbatim
5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 27
1  2  4 27 27 36 48 46 38 41 37 16 14 15 10  4  1  2  1
370
```
``` 3  4  5  6  7  8  9 10 12 13
5 15 24 17 15 22 16 11  3  1
129
```
``` 1  2  3  4  5  6  7  8  9
1 10 38 64 54 22 11  1  1
202
```
``` 1  2  3  4  5
1  2 10  5  3
21
2 3 4
5 8 7
20
2  3  4  5  6
15 49 31  2  3
100
```
``` 1  2  3
1  3 10
14
```
6. So lets consider this for now as unsatisfiable.
• n=14000
1. cutoff=10^9: 4 runs yield min=3.
2. cutoff=2*10^9: 1 run yields min=3.
3. So let's consider this for now as unsatisfiable.
• n=14375
1. cutoff=10^9: three times min=6. So let's consider this unsatisfiable for now.
• n=15000
1. ```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-7_15000.cnf
sat  min     osteps     msteps       seed
1 0    36    9340701   10000000 1782442807
2 0    39    5704494   10000000  470832140
3 0    37    8891559   10000000 3612813694
4 0    33    9055929   10000000 1719584600
5 0    41    9854280   10000000  433897223
```
2. cutoff multiplied with 10:
```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-7_15000.cnf
sat  min     osteps     msteps       seed
1 0    17   43895806  100000000 1613156495
2 0    23   98468694  100000000 3089531980
3 0    25   57245388  100000000  293693136
```
If this should be satisfiable then it's tough.
3. cutoff=10^9 yields
```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_2-3-7_15000.cnf
sat  min     osteps     msteps       seed
1 0    19  760636579 1000000000 1303145336
2 0    19  960310544 1000000000 1126725316
```
One would need cutoff=4*10^9, but perhaps it's unsatisfiable.
4. ```> ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 4000000000 -i GreenTao_2-3-7_15000.cnf
sat  min     osteps     msteps       seed
1 0    15 3386525961 4000000000 1699695039
```
So if it's still satisfiable, then it's a rather hard problem.

Definition in file GreenTao_2-3-7.hpp.