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
      > E2 = read_ubcsat("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 maximal_number_of_added_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 maximal_number_of_added_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 maximal_number_of_added_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 maximal_number_of_added_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
      adaptnoveltyp :
       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
      > E2 = read_ubcsat("GreenTao_3-3-3-5_1921.cnf_OUT2")
        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
      > E2 = read_ubcsat("~/GreenTao_3-3-3-5_1925.cnf_OUT2")
       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
      > E = read_ubcsat("GreenTao_3-3-3-5_1930.cnf_OUT4")
       1  2  3
      10 84  6
      100
      > E2 = read_ubcsat("GreenTao_3-3-3-5_1930.cnf_OUT5")
       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. (aloamo, adaptnovelty+) cutoff=4*10^9:
       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.