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

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

Go to the source code of this file.


Detailed Description

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

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

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

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

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

Todo:
greentao_4(2,3,3,3) = 151
  • Let's start with adaptnovelty+ and the logarithmic translation (seems best here).
  • n=150 easy (with cutoff=10^5; 3 solutions in 100 runs).
  • n=151: 100 runs with cutoff=10^6 didn't find a solution (98 times min=1, twice min=2).
  • OKsolver_2002 for n=151
    1. For the logarithmic translation, without symmetry breaking and without preprocessing, it seems that it will take several hundred days.
    2. With minisat2-preprocessing while otherwise the same it doesn't look much different.
    3. Weak nested standard translation, without symmetry breaking and without preprocessing:
      > OKsolver_2002-O3-DNDEBUG -M -D16 GreenTao_N_4-2-3-3-3_151.cnf
       65524:      0   2581.88  1.69E+08     0.00s     2.06s     0y   0d  0h  0m 25s     1     0   75
       65528:      0   2581.72  1.69E+08     0.00s     2.06s     0y   0d  0h  0m 17s     1     0   75
       65529:12765013   2776.48  1.82E+08 10206.27s     2.22s     0y   0d  0h  0m 16s 37975     0   75
       65530:13311450   2979.57  1.95E+08 10473.31s     2.38s     0y   0d  0h  0m 14s 34869     0   75
       65532:      0   2979.48  1.95E+08     0.00s     2.38s     0y   0d  0h  0m 10s     1     0   75
       65533:6034022   3071.51  2.01E+08  4741.86s     2.45s     0y   0d  0h  0m  7s 13521     0   77
       65534:      0   3071.47  2.01E+08     0.00s     2.45s     0y   0d  0h  0m  5s     1     0   77
       65535:16202856   3318.66  2.17E+08 13016.92s     2.65s     0y   0d  0h  0m  3s 41924     0   77
      
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         9
      c initial_number_of_variables           451
      c initial_number_of_clauses             14985
      c initial_number_of_literal_occurrences 51930
      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   11325
      c running_time(sec)                     252816.1
      c number_of_nodes                       324842537
      c number_of_single_nodes                830588
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                1451148120
      c number_of_pure_literals               76171692
      c number_of_autarkies                   0
      c number_of_missed_single_nodes         853329
      c max_tree_depth                        82
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 2536092
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_N_4-2-3-3-3_151.cnf
           
      So tree-pruning seems to be efficient here, but with the last monitoring node it falls into a hole; one needed to look at the branchings --- it could well be that what has been achieved is just to consider some nodes for the first colour, and still most of them remain (in the last monitoring node) for inspection.
    4. Strong nested standard translation, without symmetry breaking and without preprocessing: perhaps not so much different from the weak form.
    5. Strong reduced standard translation, without symmetry breaking and without preprocessing: While with the nested (standard) translation the first 2^15 nodes are reasy, now from the beginning we have high node counts, and also now often (but not always!) the processing time per node is much higher. Perhaps this is due to inefficient working of the OKsolver_2002. It could also be that the total solution time would be lower (since here the hard problems appear at the beginning). But for now aborted (since yet the strong reduced translation never performed well).
  • minisat2:
    1. Simple logarithmic translation aborted after 34 restarts (182314933 conflicts, 133210 s).
    2. Weak nested standard translation: determines unsatisfiability in 33 restarts (92925583 conflicts, 43611.9 s).
Todo:
greentao_5(2,2,3,3,3) >= 154
  • The conjecture is greentao_5(2,2,3,3,3) = 154.
  • Likely the simple logarithmic translation isn't best here anymore.
  • n=152: easily found satisfiable by sapsnr and weak nested standard translation (cutoff=10^5).
  • n=153, weak nested standard translation, rnovelty, cutoff=10^6: In run 477 a solution was found (seed=105677245, osteps=141802):
      0   1   2   3
      1 184 290   2
    477
       
  • n=154
    1. Weak standard nested translation, rnovelty, cutoff=10^6:
        1   2   3   4
      228 761   8   3
      1000
           
    2. rnovelty+, cutoff=10^6:
         1    2    3
       677 1318    5
      2000
           
    3. rnovelty, cutoff=2*10^6:
        1   2   3   4
      249 747   3   1
      1000
           
    4. rnovelty, cutoff=4*10^6:
        1   2   3
      265 729   6
      1000
           
    5. rnovelty, cutoff=8*10^6:
        1   2   3
      267 731   2
      1000
      > summary(EN2$osteps[EN2$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        14340  160400  341700  718500  676100 7094000
      > summary(EN2$osteps[EN2$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         1733   34550   69400  109400  125800 2773000
           
    6. rnovelty+, cutoff=8*10^6:
        1   2
      822 178
      1000
           
      So rnovelty+ is definitely better than rnovelty.
  • Best local search algorithm from Ubcsat-suite for the weak nested standard translation:
    > E = run_ubcsat("GreenTao_N_5-2-2-3-3-3_155.cnf")
       
    evaluated by plot(E$alg,E$best) and eval_ubcsat_dataframe(E):
    rnovelty :
     1  2  3
     4 53 43
    rnoveltyp :
     1  2  3  4
     3 49 46  2
    walksat_tabu :
     1  2  3  4
     3 39 52  6
    walksat_tabu_nonull :
     1  2  3  4
     2 37 49 12
    sapsnr :
     1  2  3  4  5
     2 21 48 24  5
    saps :
     1  2  3  4  5
     2 17 43 31  7
    noveltyp :
     1  2  3  4
     1 24 66  9
    adaptnoveltyp :
     1  2  3  4  5
     1 13 52 33  1
    gwsat :
     1  2  3  4  5  6
     1  8 35 39 14  3
    rsaps :
     1  2  3  4  5  6  7
     1  2 10 31 26 26  4
    novelty :
     2  3  4
    17 65 18
    irots :
     2  3  4  5
    11 47 38  4
    rots :
     2  3  4  5  6
     7 35 44 13  1
    hwsat :
     2  3  4  5  6  7  8  9
     4 13 31 30 17  3  1  1
    walksat :
     2  3  4  5  6  7  8  9
     2 11 17 20 21 18  9  2
    hsat :
     3  4  5  6  7  8  9 10 11 12
     2  1 10 20 24 15 11  7  5  5
    samd :
     3  4  5  6  7  8  9 10 11 12 13
     1  5  8 16 26 16 13  8  3  3  1
    gsat_tabu :
     3  4  5  6  7  8  9 10 11 12
     1  3  9 16 21 13 20 12  4  1
    gsat :
     4  5  6  7  8  9 10 12
     2 10 11 26 26 17  7  1
    gsat_simple :
     5  6  7  8  9 10 11 12 13 14
     6 14 23 16 17  6 13  2  2  1
       
  • Weak nested standard translation, rnovelty, cutoff=10^6:
     1  2  3
    14 83  3
    100
       
  • Weak nested standard translation, sapsnr, cutoff=10^6:
      1   2   3
    183 736  81
    1000
       
    So actually sapsnr might be better.

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