OKlibrary  0.2.1.6
GreenTao_te_m-3-3-4.hpp File Reference

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,3,4]) More...

Go to the source code of this file.


Detailed Description

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,3,4])

The aloamo-translation is generated by output_greentao_stdname(append(create_list(2,i,1,m),[3,3,4]),n) and output_greentao_sb_stdname(append(create_list(2,i,1,m),[3,3,4]),n) at Maxima-level, and by "GTSat 2 ... 2 3 3 4 n" at C++ level.

The nested translation is generated by output_greentao_standnest_stdname(append(create_list(2,i,1,m),[3,3,4]),n) and output_greentao_standnest_strong_stdname(append(create_list(2,i,1,m),[3,3,4]),n).

The logarithmic translation is generated by output_greentao_logarithmic_stdname(append(create_list(2,i,1,m),[3,3,4]),n).

The reduced translation is created by output_greentao_reduced_stdname(append(create_list(2,i,1,m),[3,3,4]),n) resp. output_greentao_reduced_strong_stdname(append(create_list(2,i,1,m),[3,3,4]),n).

Todo:
greentao_4(2,3,3,4) >= 453
  • The conjecture is greentao_4(2,3,3,4) = 453.
  • First considering the weak standard nested translation with rnovelty+.
  • n=442, cutoff=10^6: finds one solution in 15 runs (seed=2776413455, osteps=327557).
  • n=443
    1. cutoff=10^6: in 100 runs no solutions was found.
    2. cutoff=2*10^6: finds in run 78 one solution (seed=3773007564, osteps=1936809).
  • n=444, cutoff=4*10^6: finds a solution in run 10 (seed=2050602575, osteps=2112736).
  • n=445, cutoff=4*10^6: finds a solution in run 7 (seed=4168291728, osteps=2670307).
  • n=446, cutoff=4*10^6: finds a solution in run 2 (seed=3913893840, osteps=3235502).
  • n=447, cutoff=4*10^6: in 332 runs 13 solutions were found (seed=1711609145, osteps=865779).
  • n=448, cutoff=4*10^6: in run 131 a solution was found (seed=4208191351, osteps=3277920).
  • n=449, cutoff=6*10^6: in run 54 a solution was found (seed=3969099878, osteps=2013315).
  • n=450, cutoff=6*10^6: in run 162 a solution was found (seed=1486592823, osteps=2486421).
  • n=451, cutoff=6*10^6: in run 13 a solution was found (seed=3091775367, osteps=5018123).
  • n=452 cutoff=6*10^6
    1. cutoff=6*10^6: In run 11 a solution was found (seed=592938116, osteps=3809907).
    2. cutoff=10^7:
       0  1  2
       4 75 21
      100
           
      So perhaps actually walksat-tabu-nonull is better (for higher cutoffs).
    3. walksat-tabu-nonull, cutoff=10^7:
       0  1  2
       5 84 11
      100
           
    4. rnovelty, cutoff=10^7:
       1  2
      70 30
      100
           
      So here we have a case where an algorithms seem good, because it finds reasonably many cases with min=1, but actually it fails to realise min=0 !
    5. walksat-tabu, cutoff=10^7:
       0  1  2  3
       3 68 12  1
      84
           
      So walksat-tabu-nonull seems better.
  • n=453
    1. cutoff=6*10^6:
        1   2   3
      214 169  17
      400
           
    2. cutoff=10^7:
        1   2   3
      310 151   5
      466
           
    3. Best local search algorithm from Ubcsat-suite:
      > E = run_ubcsat("GreenTao_N_4-2-3-3-4_453.cnf", runs=100,cutoff=1000000)
           
      evaluated by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
      rnovelty :
       1  2  3  4  5
       7 34 44 14  1
      rnoveltyp :
       1  2  3  4
       7 29 41 23
      walksat_tabu_nonull :
       1  2  3  4  5  6
       5 18 33 29 10  5
      noveltyp :
       1  2  3  4  5
       2 27 54 15  2
      walksat_tabu :
       1  2  3  4  5  6
       2 15 25 33 22  3
      novelty :
       1  2  3  4  5
       1  5 53 38  3
      gwsat :
       1  3  4  5  6  7  8  9
       1  5 14 28 30 15  6  1
           
    4. walksat-tabu-nonull with cutoff=10^7
        1   2   3
      323  74   3
      400
           
      Since it's faster than rnovelty+, it seems to be superior.
    5. walksat-tabu, cutoff=10^7:
       1  2  3
      65 32  3
      100
           
      So it seems that the nonull-option improves performance (though at the cost of running time).
Todo:
greentao_5(2,2,3,3,4) >= 472
  • The conjecture is greentao_5(2,2,3,3,4) = 472.
  • First considering the weak standard nested translation with rnovelty+.
  • n=460, cutoff=10^7: found a solution in run 100 (seed=689351359, osteps=6436295).
  • n=461
    1. cutoff=2*10^7:
       1  2
      40 60
      100
           
    2. walksat-tabu-nonull, cutoff=2*10^7 finds a solution in run 22 (seed=164496226, osteps=16042190).
  • n=462, cutoff=2*10^7, walksat-tabu-nonull: found a solution in the first run (seed=89229228, osteps=8204248).
  • n=463, cutoff=2*10^7, walksat-tabu-nonull: found a solution in run 88 (seed=3466211155, osteps=17673628).
  • n=464
    1. cutoff=2*10^7, walksat-tabu-nonull:
       1  2  3
      21 65 14
      100
           
    2. cutoff=4*10^7, walksat-tabu-nonull: in run 18 a solution was found (seed=3466303736, osteps=17253883).
  • n=465, cutoff=4*10^7, walksat-tabu-nonull: found a solution in run 63 (seed=3647398344, osteps=32380993).
  • n=466
    1. cutoff=4*10^7, walksat-tabu-nonull
       1  2  3
      32 59  9
      100
           
    2. cutoff=4*10^7, rnovelty+ finds a solution in the first run (seed=409569711, osteps=25887086).
  • n=467, cutoff=4*10^7, rnovelty+: found a solution in run 16 (seed=3217946404, osteps=24166244).
  • n=468
    1. cutoff=4*10^7, rnovelty+:
       1  2  3
      32 67  1
      100
           
    2. cutoff=4*10^7, walksat-tabu-nonull:
       1  2  3
      16 74 10
      100
           
    3. cutoff=4*10^7, rnovelty
       1  2  3
      13 82  5
      100
           
    4. But with cutoff=4*10^6 in run 188 a solution was found (seed=2945992972, osteps=2263637).
    5. So perhaps (yet) we use more runs and fewer steps.
  • n=469, rnovelty+, cutoff=4*10^6: in run 529 a solution was found (seed=2454496664, osteps=3555403).
  • n=470, rnovelty+:
    1. cutoff=4*10^6:
       1  2  3  4
       1 48 97 28
      174
           
    2. cutoff=10^7: in run 128 a solution was found (seed=4019815590, osteps=7671202).
  • n=471, rnovelty+
    1. cutoff=10^7:
        1   2   3   4
       45 377 257  15
      694
           
    2. cutoff=2*10^7: in run 46 a solution was found (seed=2641525455, osteps=13744258).
  • n=472, rnovelty+
    1. cutoff=2*10^7
        1   2   3   4
       12 136  51   1
      200
           
    2. cutoff=4*10^7
        1   2   3
       30 156  14
      200
           
    3. Best local search algorithm from Ubcsat-suite:
      > E = run_ubcsat("GreenTao_N_5-2-2-3-3-4_472.cnf", runs=100,cutoff=500000)
           
      evaluated by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
      rnovelty :
       2  3  4  5  6  7  8
       1  8 22 36 22  9  2
      rnoveltyp :
       3  4  5  6  7  8
       6 26 33 22 11  2
      noveltyp :
       3  4  5  6  7  8
       3 21 23 34 12  7
      walksat_tabu_nonull :
       3  4  5  6  7  8  9 10 11
       3  8 14 26 22 19  5  2  1
      walksat_tabu :
       3  4  5  6  7  8  9 10
       2  8 11 25 29 16  7  2
      gwsat :
       3  4  6  7  8  9 10 11 12 13 14 15
       1  1 10  7 12 14 20 20  6  6  1  2
           
      So rnovelty seems best.
    4. rnovelty, cutoff=4*10^7:
        1   2   3
       10 167  11
      188
           
      Thus actually rnovelty+ seems better (at least for higher cutoffs).

Definition in file GreenTao_te_m-3-3-4.hpp.