OKlibrary  0.2.1.6
GreenTao_te_m-3-4.hpp File Reference

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,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,4])

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

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

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

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

Todo:
greentao_3(2,3,4) = 117
  • Easy for OKsolver_2002:
    > OKsolver_2002-O3-DNDEBUG GreenTao_3-2-3-4_116.cnf
    s SATISFIABLE
    c sat_status                            1
    c initial_maximal_clause_length         4
    c initial_number_of_variables           348
    c initial_number_of_clauses             8061
    c initial_number_of_literal_occurrences 17337
    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   7018
    c running_time(sec)                     2.0
    c number_of_nodes                       2384
    c number_of_single_nodes                0
    c number_of_quasi_single_nodes          0
    c number_of_2-reductions                11743
    c number_of_pure_literals               0
    c number_of_autarkies                   21
    c number_of_missed_single_nodes         3
    c max_tree_depth                        76
    c number_of_table_enlargements          0
    c number_of_1-autarkies                 46284
    c number_of_new_2-clauses               0
    c maximal_number_of_added_2-clauses     0
    c file_name                             GreenTao_3-2-3-4_116.cnf
    > OKsolver_2002-O3-DNDEBUG GreenTao_3-2-3-4_117.cnf
    s UNSATISFIABLE
    c sat_status                            0
    c initial_maximal_clause_length         4
    c initial_number_of_variables           351
    c initial_number_of_clauses             8198
    c initial_number_of_literal_occurrences 17633
    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   7137
    c running_time(sec)                     2.4
    c number_of_nodes                       2703
    c number_of_single_nodes                0
    c number_of_quasi_single_nodes          0
    c number_of_2-reductions                14339
    c number_of_pure_literals               0
    c number_of_autarkies                   24
    c number_of_missed_single_nodes         11
    c max_tree_depth                        77
    c number_of_table_enlargements          0
    c number_of_1-autarkies                 57409
    c number_of_new_2-clauses               0
    c maximal_number_of_added_2-clauses     0
    c file_name                             GreenTao_3-2-3-4_117.cnf
       
Todo:
greentao_4(2,2,3,4) = 120
  • n=117,118: minisat2 determines satisfiability in 13 restarts.
  • n=119: minisat2 determines satisfiability in 15 restarts.
  • n=120: minisat2 determines unsatisfiability in 13 restarts.
  • n=130
    1. OKsolver_2002 without symmetry breaking and without preprocessing apparently falls into a deep hole:
      > OKsolver_2002-O3-DNDEBUG -M -D30 GreenTao_4-2-2-3-4_130.cnf
      227528557:    113      0.00  2.24E+04     0.80s     0.00s     0y   0d  0h  1m 15s     0     1   85
      
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         4
      c initial_number_of_variables           520
      c initial_number_of_clauses             18821
      c initial_number_of_literal_occurrences 39254
      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   17550
      c running_time(sec)                     253.6
      c number_of_nodes                       44429
      c number_of_single_nodes                37
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                344658
      c number_of_pure_literals               0
      c number_of_autarkies                   519
      c number_of_missed_single_nodes         5154
      c max_tree_depth                        126
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 5648488
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_4-2-2-3-4_130.cnf
           
    2. OKsolver_2002 without symmetry breaking and with preprocessing seems to be able to solve it in 2 days (csltok), so preprocessing seems to help.
    3. minisat2 determines unsatisfiability in 18 restarts (261912 conflicts) without symmetry breaking, and behaves *identical* on the symmetry-breaking instance.
    4. picosat913 needs 4 times longer without minisat2 preprocessing and still twice as long with minisat2 preprocessing.
    5. So likely again minisat2 is best here (and the conflict-driven approach achieves something).
Todo:
greentao_5(2,2,2,3,4) = 128
  • Best local search solver:
    > E = run_ubcsat("GreenTao_5-2-2-2-3-4_125.cnf")
       
    evaluated by plot(E$alg,E$best): hard to say, since many algorithms determined satisfiability, but saps is best, followed perhaps by gwsat, adaptnovelty+ and sapsnr.
  • n=125: minisat2 determines satisfiability in 17 restarts.
  • n=127: minisat2 determines satisfiability in 20 restarts.
  • n=128: minisat2 determines unsatisfiability in 21 restarts.
  • n=130: minisat2 determines unsatisfiability in 20 restarts
  • n=140: minisat2 determines unsatisfiability in 24 restarts (20m on csltok; there seems to be the pattern, that short before the search-end the average length of learned clauses jumps (over 100)).
Todo:
greentao_6(2,...,2,3,4) = 136
  • Best local search solver:
    > E = run_ubcsat("GreenTao_6-2-2-2-2-3-4_135.cnf")
       
    evaluated by plot(E$alg,E$best): the following four solvers seem best:
    > table(E$best[E$alg=="gwsat"])
     0  1  2  3
     2 21 69  8
    > table(E$best[E$alg=="rnovelty"])
     0  1  2  3
     2 20 71  7
    > table(E$best[E$alg=="sapsnr"])
     0  1  2  3
     1 32 66  1
    > table(E$best[E$alg=="rnoveltyp"])
     0  1  2  3
     1 17 70 12
    > table(E$best[E$alg=="saps"])
     1  2
    49 51
       
  • Repeated the evaluation for n=140: for cutoff=100000 no solver could find a satisfying assignment, while 8 found min=1; sapsnr looks best, followed by saps. Using cutoff=10^6: Now saps looks clearly best.
  • n=130: minisat2 determines satisfiability in 13 restarts.
  • n=135: minisat2 determines satisfiability in 24 restarts; so perhaps unsatisfiability can still be determined here, but for satisfiable cases ubcsat is to be used.
  • n=136:

    1. cutoff=10^6 with saps: 97 times min=1, 3 times min=2.
    2. cutoff=10^6 with sapsnr: 68 times min=1, 32 times min=2.
    3. cutoff=10^6 with gwsat: 93 times min=1, 7 times min=2.
    4. cutoff=10^6 with rnovelty: 78 times min=1, 21 times min=2, once min=3.
    5. minisat2: determined unsatisfiability in 31 restarts (55800700 conflicts, 106321 s (csltok)).
    6. Until now only the strong standard translation was used; now using the weak standard nested translation.
    7. OKsolver_2002
      1. Without symmetry breaking: As it is often the case, the second branch is much harder, and local maxima of node-counts for monitoring nodes occur at the nodes which complete a branching at lower levels. Aborted after 3 hours:
        > OKsolver_2002-O3-DNDEBUG -M -D20 GreenTao_N_6-2-2-2-2-3-4_136.cnf
        520192: 225216      3.88  4.07E+06   880.30s     0.01s     0y   0d  1h 58m 18s   119     0  213
        s UNKNOWN
        c sat_status                            2
        c initial_maximal_clause_length         20
        c initial_number_of_variables           679
        c initial_number_of_clauses             37955
        c initial_number_of_literal_occurrences 203255
        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   9180
        c running_time(sec)                     17821.8
        c number_of_nodes                       4659973
        c number_of_single_nodes                1568
        c number_of_quasi_single_nodes          0
        c number_of_2-reductions                16952345
        c number_of_pure_literals               155029
        c number_of_autarkies                   0
        c number_of_missed_single_nodes         57156
        c max_tree_depth                        336
        c number_of_table_enlargements          18
        c number_of_1-autarkies                 6876472
        c number_of_new_2-clauses               0
        c maximal_number_of_added_2-clauses     0
        c file_name                             GreenTao_N_6-2-2-2-2-3-4_136.cnf
               
        This is the first time that I see that "table enlargements" happened; this should be investigated further (yet only a relatively small number of nodes were created?).
      2. With the strong nested standard translation it doesn't seem better; again, after just 100000 nodes there are 8 table enlargements?!
    8. minisat2 determines unsatisfiability in 29 restarts (21805719 conflicts, 38567.2 s), so the problem got (as usual) somewhat easier with the weak standard nested translation.
    9. n=140:
      1. None of the ubcsat-algorithms found a solution in 100 runs and with cutoff=10^6.
    Todo:
    greentao_7(2,...,2,3,4) >= 142
    • n=140: cutoff=10^5 using saps found 3 solutions in 100 runs (e.g., seed=4007050970, osteps=26801).
    • n=141
      1. cutoff=10^6 using saps:
         0  1  2
         9 78 13
        100
             
        (best solution: seed=414927092, osteps=73582).
      2. cutoff=10^6 using adaptnovelty+:
         0  1  2
        37 62  1
        100
             
    • n=142
      1. cutoff=10^6 using saps:
         1  2
        77 23
        100
             
      2. cutoff=10^7 using saps:
         1  2
        99  1
        100
        > summary(E$osteps)
           Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
           2209   70730  195600  919500  709400 9654000
             
      3. Determining the best Ubcsat-algorithm (cutoff=10^6):
        > E = run_ubcsat("GreenTao_7-2-2-2-2-2-3-4_142.cnf", cutoff=1000000,runs=100)
        > plot(E$alg,E$best)
        > table(E$best[E$alg=="adaptnoveltyp"])
          1
        100
        > table(E$best[E$alg=="gwsat"])
         1  2
        99  1
        > table(E$best[E$alg=="noveltyp"])
         1  2
        93  7
        > table(E$best[E$alg=="saps"])
         1  2
        78 22
             
        So actually adaptnovelty+ seems (again) best.
      4. cutoff=10^7 using adaptnovelty+:
        > E = read_ubcsat("GreenTao_7-2-2-2-2-2-3-4_142.cnf_OUT3")
          1
        100
        100
        > summary(E$osteps)
           Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
          43740  113900  205500  252300  346500  850900
             
      5. It seems minisat2 could need months here.
    • n=145
      1. cutoff=10^6 using saps:
         1  2
        39 61
        100
             
    • n=150:
      1. cutoff=10^5 using saps:
         1  2  3  4
         8 52 38  2
        100
             
      2. cutoff=10^6 using saps:
         1  2
        44 56
        100
             
    Todo:
    greentao_8(2,...,2,3,4) >= 151
    • n=145: adaptnovelty+ with cutoff=10^7 finds 29 solutions in 29 runs.
    • n=150
      1. aloamo-translation, adaptnovelty+ with cutoff=10^7 found solution easily (seed=361186873).
      2. Logarithmic translation with rnovelty+ and cutoff=2*10^6 found a solution in 56 runs.
      3. Walksat seems to be better here, and found a solution with cutoff=2*10^6 in 4 runs.
      4. And walksat-tabu seems even better: first 10 runs with cutoff=2*10^6 found each a solution.
    • n=151
      1. Logarithmic translation, rnovelty+, cutoff=2*10^6:
          1   2
        526 474
        1000
             
      2. Logarithmic translation, walksat-tabu with cutoff=10^6: In 1000 runs always min=1 was reached. Same with cutoff=2*10^6.
      3. Running OKsolver_2002 on the logarithmic translation looks hopeless.
      4. OKsolver_2002 with the weak standard nested translation made some progress, but then it felt into a hole.
      5. minisat2 with weak standard nested translation:
      6. minisat2 with strong standard nested translation: aborted after 34 restarts (the typical oscillation, and no progress visible).
    • n=155: adaptnovelty+ with cutoff=10^7 produced in 100 runs always min=1, so looks unsatisfiable.

Definition in file GreenTao_te_m-3-4.hpp.