OKlibrary  0.2.1.6
GreenTao_2-3-6.hpp File Reference

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

Go to the source code of this file.


Detailed Description

Investigations on greentao_2(3,6)

Problems are generated by output_greentao2nd_stdname(3,6,n) at Maxima level, or by "GTSat 3 6 n" at C++ level. The conjecture is greentao_2(3,6) = 2072.

Todo:
Finding the best algorithm from ubcsat
  • adaptnovelty+ seems best:
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 18008
    BestStep_Mean = 88748.500000
    Steps_Mean = 100000.000000
    Steps_Max = 100000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 20.200000
    BestSolution_Median = 20.000000
    BestSolution_Min = 18.000000
    BestSolution_Max = 22.000000
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 33208
    BestStep_Mean = 695169.500000
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 9.700000
    BestSolution_Median = 9.500000
    BestSolution_Min = 7.000000
    BestSolution_Max = 12.000000
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 42551
    BestStep_Mean = 3400237.000000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 7.700000
    BestSolution_Median = 7.500000
    BestSolution_Min = 7.000000
    BestSolution_Max = 9.000000
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 49276
    BestStep_Mean = 25508521.900000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 6.100000
    BestSolution_Median = 6.000000
    BestSolution_Min = 5.000000
    BestSolution_Max = 7.000000
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_2-3-6_2250.cnfClauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 72631
    BestStep_Mean = 172037848.800000
    Steps_Mean = 1000000000.000000
    Steps_Max = 1000000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 5.000000
    BestSolution_Median = 5.000000
    BestSolution_Min = 5.000000
    BestSolution_Max = 5.000000
       
    (Seems that 5 falsified clauses is the minimum.)
  • Also "walksat-tabu -v nonull" seems better than rnovelty+ (but not as good as adaptnovelty+):
    > ubcsat-okl -alg  walksat-tabu -v nonull -runs 10 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 24728
    BestStep_Mean = 66136.100000
    Steps_Mean = 100000.000000
    Steps_Max = 100000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 21.300000
    BestSolution_Median = 22.000000
    BestSolution_Min = 13.000000
    BestSolution_Max = 25.000000
    > ubcsat-okl -alg  walksat-tabu -v nonull -runs 10 -cutoff 1000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 32283
    BestStep_Mean = 642215.000000
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 14.500000
    BestSolution_Median = 14.500000
    BestSolution_Min = 11.000000
    BestSolution_Max = 16.000000
       
  • rnovelty+ seems third from the ubcsat-range (version 1.0.0):
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 100000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 22267
    BestStep_Mean = 51646.200000
    Steps_Mean = 100000.000000
    Steps_Max = 100000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 24.600000
    BestSolution_Median = 24.000000
    BestSolution_Min = 21.000000
    BestSolution_Max = 28.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 43269
    BestStep_Mean = 495302.000000
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 18.200000
    BestSolution_Median = 19.500000
    BestSolution_Min = 11.000000
    BestSolution_Max = 23.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 42383
    BestStep_Mean = 4779885.400000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 11.500000
    BestSolution_Median = 12.000000
    BestSolution_Min = 10.000000
    BestSolution_Max = 13.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2250.cnf
    Clauses = 185490
    Variables = 2250
    TotalLiterals = 558633
    FlipsPerSecond = 39750
    BestStep_Mean = 51162593.300000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 7.300000
    BestSolution_Median = 7.000000
    BestSolution_Min = 6.000000
    BestSolution_Max = 9.000000
       
  • Preprocessing:
    1. Due to the highly constraint character of these problems, the minisat2 preprocessor achieves a considerable reduction in the number of variables.
    2. While for example for greentao_2(4,5) no variable was eliminated.
    3. However, actually these "simplified" problems seem to be harder (at least for adaptnovelty+):
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-6_2071_pre.cnf
      Clauses = 88303
      Variables = 2071
      TotalLiterals = 465266
      FlipsPerSecond = 89232
      BestStep_Mean = 4078732.700000
      Steps_Mean = 10000000.000000
      Steps_Max = 10000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 1.100000
      BestSolution_Median = 1.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 2.000000
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2071_pre.cnf
      Clauses = 88303
      Variables = 2071
      TotalLiterals = 465266
      FlipsPerSecond = 83669
      BestStep_Mean = 9849960.900000
      Steps_Mean = 94840863.900000
      Steps_Max = 100000000.000000
      PercentSuccess = 10.00
      BestSolution_Mean = 0.900000
      BestSolution_Median = 1.000000
      BestSolution_Min = 0.000000
      BestSolution_Max = 1.000000
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-6_2071.cnf
      Clauses = 158884
      Variables = 2071
      TotalLiterals = 478584
      FlipsPerSecond = 78718
      BestStep_Mean = 4601845.300000
      Steps_Mean = 9364095.600000
      Steps_Max = 10000000.000000
      PercentSuccess = 30.00
      BestSolution_Mean = 1.000000
      BestSolution_Median = 1.000000
      BestSolution_Min = 0.000000
      BestSolution_Max = 2.000000
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2071.cnf
      Clauses = 158884
      Variables = 2071
      TotalLiterals = 478584
      FlipsPerSecond = 101111
      BestStep_Mean = 42545701.800000
      Steps_Mean = 52277744.000000
      Steps_Max = 100000000.000000
      PercentSuccess = 90.00
      BestSolution_Mean = 0.100000
      BestSolution_Median = 0.000000
      BestSolution_Min = 0.000000
      BestSolution_Max = 1.000000
           
      (Perhaps there is a problem with the gaps regarding the variable indices? The preprocessed file kept the old variable names. Hopefully not.)
Todo:
greentao_2(3,6) >= 2072
  • Conjecture: greentao_2(3,6) = 2072.
    1. While with a cutoff of 100*10^6 n=2071 is easily handled, no success with n=2072,
    2. See "Upper bounds" below.
  • n = 2062 found satisfiable by ubcsat-adaptnovelty+ with msteps = 24408280 and seed = 1309685658 (cutoff = 100*10^6).
  • n = 2070 found satisfiable by ubcsat-adaptnovelty+ with msteps = 17943201 and seed = 2009708202 (cutoff = 100*10^6).
  • n = 2071 found satisfiable by ubcsat-adaptnovelty+ with msteps = 11332054 and seed = 1169059362 (cutoff = 100*10^6).
  • n = 2072 looks unsatisfiable:
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2072.cnf
    Clauses = 159039
    Variables = 2072
    TotalLiterals = 479052
    FlipsPerSecond = 119377
    BestStep_Mean = 15846549.300000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.000000
    BestSolution_Median = 1.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 1.000000
       
  • Further 57 runs yield all min=1.
  • And also after preprocessing with Minisat2 (see below) no satisfying assignment is found:
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-6_2072_pre.cnf
    Clauses = 88791
    Variables = 2072
    TotalLiterals = 467889
    FlipsPerSecond = 78648
    BestStep_Mean = 2783465.900000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.600000
    BestSolution_Median = 2.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 2.000000
       
  • n = 2074 looks unsatisfiable:
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2074.cnf
    Clauses = 159321
    Variables = 2074
    TotalLiterals = 479898
    FlipsPerSecond = 117038
    BestStep_Mean = 11611872.900000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.000000
    BestSolution_Median = 1.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 1.000000
       
  • n = 2078 seems unsatisfiable:
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-6_2078.cnf
    Clauses = 159895
    Variables = 2078
    TotalLiterals = 481629
    FlipsPerSecond = 110868
    BestStep_Mean = 19625287.200000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.000000
    BestSolution_Median = 1.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 1.000000
       
  • n = 2094 seems unsatisfiable
    > ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 100000000 -i GreenTao_2_3_6_2094.cnf
    Clauses = 162248
    Variables = 2094
    TotalLiterals = 488703
    FlipsPerSecond = 93403
    BestStep_Mean = 10185143.160000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.890000
    BestSolution_Median = 2.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 2.000000
       
  • n = 2125 might be unsatisfiable:
    > ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 10000000 -i GreenTao_2_3_6_2125.cnf
    Clauses = 166757
    Variables = 2125
    TotalLiterals = 502284
    FlipsPerSecond = 84973
    BestStep_Mean = 4796045.770000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 2.740000
    BestSolution_Median = 3.000000
    BestSolution_Min = 2.000000
    BestSolution_Max = 4.000000
    > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2_3_6_2125.cnf
    Clauses = 166757
    Variables = 2125
    TotalLiterals = 502284
    FlipsPerSecond = 89403
    BestStep_Mean = 13475345.800000
    Steps_Mean = 100000000.000000
    Steps_Max = 100000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 2.000000
    BestSolution_Median = 2.000000
    BestSolution_Min = 2.000000
    BestSolution_Max = 2.000000
       
  • n = 2250 looks unsatisfiable: see above.
  • n = 2500 looks unsatisfiable:
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 100000 -i GreenTao_2_3_6_2500.cnf
    Clauses = 226059
    Variables = 2500
    TotalLiterals = 680712
    FlipsPerSecond = 13038
    BestStep_Mean = 68629.200000
    Steps_Mean = 100000.000000
    Steps_Max = 100000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 61.900000
    BestSolution_Median = 62.500000
    BestSolution_Min = 57.000000
    BestSolution_Max = 64.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2_3_6_2500.cnf
    Clauses = 226059
    Variables = 2500
    TotalLiterals = 680712
    FlipsPerSecond = 13062
    BestStep_Mean = 495738.100000
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 54.000000
    BestSolution_Median = 55.000000
    BestSolution_Min = 47.000000
    BestSolution_Max = 57.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2_3_6_2500.cnf
    Clauses = 226059
    Variables = 2500
    TotalLiterals = 680712
    FlipsPerSecond = 12799
    BestStep_Mean = 4374264.300000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 50.300000
    BestSolution_Median = 50.500000
    BestSolution_Min = 46.000000
    BestSolution_Max = 53.000000
       
  • n = 3000 looks unsatisfiable:
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 100000 -i GreenTao_2_3_6_3000.cnf
    Clauses = 318899
    Variables = 3000
    TotalLiterals = 960054
    FlipsPerSecond = 7081
    BestStep_Mean = 52997.600000
    Steps_Mean = 100000.000000
    Steps_Max = 100000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 137.300000
    BestSolution_Median = 137.500000
    BestSolution_Min = 126.000000
    BestSolution_Max = 146.000000
    > ubcsat-okl -alg rnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2_3_6_3000.cnf
           sat  min     osteps     msteps       seed
          1 0   132     899782    1000000  257061986
          2 0   133     533282    1000000 3225188000
       
Todo:
OKsolver_2002
  • It appears that OKsolver would need, say, 50 years for n=5000 on the laptop.
  • With a cluster, this would be feasible; and perhaps optimising the heuristics yields something.
  • Also higher n could be tried.
  • n=2072
    1. Without preprocessing:
      > OKsolver_2002-O3-DNDEBUG -M -D30 -F GreenTao_2-3-6_2072.cnf
       Daten/GreenTao/GreenTao_2-3-6_2072.cnf,   30, 1073741824
           8:     28      3.50  3.76E+09     4.09s     0.51s    17y 148d 14h 15m  3s     0     0   27
      s UNKNOWN
      c sat_status=2 initial_maximal_clause_length=6 initial_number_of_variables=2071 initial_number_of_clauses=159039 initial_number_of_literal_occurrences=479052 running_time(s)=42598.1 number_of_nodes=173575 number_of_single_nodes=0 number_of_quasi_single_nodes=0 number_of_2-reductions=3510562 number_of_pure_literals=118091 number_of_autarkies=0 number_of_missed_single_nodes=0 max_tree_depth=94 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=0 reduced_number_of_clauses=0 reduced_number_of_literal_occurrences=0 number_of_1-autarkies=34995218 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=0 file_name=Daten/GreenTao/GreenTao_2-3-6_2072.cnf
           
      has average 2-reductions ~ 20.23, where 2071 / 20.16 ~ 102.3, while speed is 4.07 nodes per second.
    2. With preprocessing:
      > OKsolver_2002-m2pp -M -D30 -F Daten/GreenTao/GreenTao_2-3-6_2072.cnf
      s UNKNOWN
      c sat_status=2 initial_maximal_clause_length=15 initial_number_of_variables=1316 initial_number_of_clauses=88791 initial_number_of_literal_occurrences=467889 running_time(s)=33314.6 number_of_nodes=74584 number_of_single_nodes=0 number_of_quasi_single_nodes=0 number_of_2-reductions=1314662 number_of_pure_literals=17611 number_of_autarkies=0 number_of_missed_single_nodes=0 max_tree_depth=112 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=0 reduced_number_of_clauses=0 reduced_number_of_literal_occurrences=0 number_of_1-autarkies=338411 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=0 file_name=Daten/GreenTao/GreenTao_2-3-6_2072.cnf_m2pp_32660
           
      has average 2-reduction ~ 17.63, where 1316 / 17.68 ~ 74.6, while speed is 2.24 nodes per second.
    3. This looks as if here something strange happened: Why is it so slow? Why is the depth so big?
      • It could be that long clauses cause somehow bad performance; but this shouldn't be the case.
      • There could be structural differences, for example with the preprocessed version somehow more rounds are needed for the reduction.
      • Or it could be that the depth (which is the maximal depth of some leaf) for the preprocessed case is misleading, some sort of outlier, while most of the time work is spent higher up in the tree, where instances are bigger (and there are less 2-reductions).
    4. Without tree pruning and without preprocessing:
      OKplatform> system_directories/bin/OKsolver_2002_NTP-O3-DNDEBUG -M -D30 -F Daten/GreenTao/GreenTao_2-3-6_2072.cnf
       Daten/GreenTao/GreenTao_2-3-6_2072.cnf,   30, 1073741824
           8:     28      3.50  3.76E+09     3.82s     0.48s    16y  94d  3h 55m 17s     0     0   27
      s UNKNOWN
      c sat_status=2 initial_maximal_clause_length=6 initial_number_of_variables=2071 initial_number_of_clauses=159039 initial_number_of_literal_occurrences=479052 running_time(s)=26182.4 number_of_nodes=125379 number_of_single_nodes=0 number_of_quasi_single_nodes=0 number_of_2-reductions=2530109 number_of_pure_literals=86545 number_of_autarkies=0 number_of_missed_single_nodes=0 max_tree_depth=94 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=0 reduced_number_of_clauses=0 reduced_number_of_literal_occurrences=0 number_of_1-autarkies=25338066 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=0 file_name=Daten/GreenTao/GreenTao_2-3-6_2072.cnf
           
      average 2-reductions ~ 20.18, speed ~ 4.79 nodes per second.
    5. Without tree pruning and with preprocessing:
      OKplatform> system_directories/bin/OKsolver_2002_NTP-O3-DNDEBUG -M -D30 -F Daten/GreenTao/GreenTao_2-3-6_2072-m2pp.cnf
       Daten/GreenTao/GreenTao_2-3-6_2072-m2pp.cnf,   30, 1073741824
       s UNKNOWN
      c sat_status=2 initial_maximal_clause_length=15 initial_number_of_variables=1316 initial_number_of_clauses=88791 initial_number_of_literal_occurrences=467889 running_time(s)=26011.9 number_of_nodes=68988 number_of_single_nodes=0 number_of_quasi_single_nodes=0 number_of_2-reductions=1211382 number_of_pure_literals=16289 number_of_autarkies=0 number_of_missed_single_nodes=0 max_tree_depth=112 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=0 reduced_number_of_clauses=0 reduced_number_of_literal_occurrences=0 number_of_1-autarkies=314872 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=0 file_name=Daten/GreenTao/GreenTao_2-3-6_2072-m2pp.cnf
          
      average 2-reductions ~ 17.56, speed ~ 2.65 nodes per second.
    6. So tree-pruning is actually a bit more expensive than anticipated (at least one these instances), but it is not the cause of the weak performance on preprocessed instances.
Todo:
Minisat2
  • minisat2 seems also not achieving something:
    > minisat2 GreenTao_2-3-6_2072.cnf
    ...
    |  57525118 |    1316    88791   467889 |   568094   272657     40 |  0.000 % |
    
    *** INTERRUPTED ***
    restarts              : 32
    conflicts             : 57658225       (229 /sec)
    decisions             : 63767800       (1.80 % random) (253 /sec)
    propagations          : 4376843220     (17368 /sec)
    conflict literals     : 2291143690     (40.74 % deleted)
    Memory used           : 203.70 MB
    CPU time              : 252005 s
       
Todo:
march_pl
  • It seems in phase 1 of the preprocessing 68553 clauses and 397 variables are removed, while in phase 2 65386 clauses are added.
  • Apparently the maximal clause-length has not been increased in this process (so perhaps march_pl is less aggressive than minisat2).
  • Like the other solvers, it seems hopeless (and the feedback-quality of march_pl is rather poor).

Definition in file GreenTao_2-3-6.hpp.