OKlibrary  0.2.1.6
GreenTao_3-3.hpp File Reference

Investigations on greentao_3(3) = 137. More...

Go to the source code of this file.


Detailed Description

Investigations on greentao_3(3) = 137.

Aloamo-translation generated by output_greentaod_stdname(3,3,n) or output_greentaod_sb_stdname(3,3,n) at Maxima-level, and by "GTdSat 3 3 n" at C++ level.

Standard nested translation generated by output_greentao_standnest_stdname([3,3,3],n) or output_greentao_standnest_strong_stdname([3,3,3],n).

Logarithmic translation generated by output_greentao_logarithmic_stdname([3,3,3],n).

Standard reduced translation generated by output_greentao_reduced_stdname([3,3,3],n) or output_greentao_reduced_strong_stdname([3,3,3],n).

Todo:
DONE (available now) Symmetry breaking:
  • The only available symmetry since the symmetry between the partitions, i.e., one vertex can be put into the first partition.
  • For vdW-problems it seems that the middle vertices are best used here (they have also the highest degrees); but here we should consider the vertex degrees.
  • The variable of maximal degree is prime number 3.
  • So perhaps we should always use this for symmetry breaking.
Todo:
adaptnovelty+
  • n=125 easily found satisfiable by adaptnovelty+.
  • n=132 easily found satisfiable by adaptnovelty+.
  • n=135 easily found satisfiable by adaptnovelty+.
  • n=136 easily found satisfiable by adaptnovelty+.
  • n=137: adaptnovelty+ with runs=1000 and cutoff=10^6 yields
    Clauses = 3614
    Variables = 411
    TotalLiterals = 10431
    FlipsPerSecond = 1189726
    BestStep_Mean = 162376.034000
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 1.000000
    BestSolution_Median = 1.000000
    BestSolution_Min = 1.000000
    BestSolution_Max = 1.000000
       
  • n=138: adaptnovelty+ yields (nearly) constantly minimum=1 with cutoff=10^6.
  • n=150: cutoff=10*10^6 yields minimum=1; with 10 runs and with 100 runs.
  • n=200: adaptnovelty+ doesn't seem to achieve better than a minimum=10.
Todo:
OKsolver_2002
  • n=100 easily satisfiable by OKsolver_2002.
  • n=137:
    1. First the aloamo translation.
    2. Without symmetry breaking and without preprocessing:
      > OKsolver_2002-O3-DNDEBUG -D14 -M -F GreenTao_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status=0 initial_maximal_clause_length=3 initial_number_of_variables=411 initial_number_of_clauses=3614 initial_number_of_literal_occurrences=10431 running_time(s)=358228.8 number_of_nodes=517673976 number_of_single_nodes=8226277 number_of_quasi_single_nodes=0 number_of_2-reductions=4048438213 number_of_pure_literals=0 number_of_autarkies=473887 number_of_missed_single_nodes=14846911 max_tree_depth=58 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=3256102327 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=411 file_name=GreenTao_3-3-3-3_137.cnf
           
      The plot of the numbers of nodes shows some kind of periodic patterns. The relation between nodes and time is very linear:
      > NE = lm(E$time ~ E$nodes)
      > summary(NE)
      Residuals:
            Min        1Q    Median        3Q       Max
      -23.61630  -0.02370   0.01408   0.02322  67.70912
      Coefficients:
                    Estimate Std. Error t value Pr(>|t|)
      (Intercept) -1.408e-02  2.040e-02   -0.69     0.49
      E$nodes      6.924e-04  1.879e-07 3685.43   <2e-16 ***
      Residual standard error: 2.255 on 13850 degrees of freedom
      Multiple R-squared: 0.999,      Adjusted R-squared: 0.999
      F-statistic: 1.358e+07 on 1 and 13850 DF,  p-value: < 2.2e-16
           
      The number of nodes was highest at the beginning, and then, piecewise, the sub-problems got easier. Average 2-reduction per node is 7.8, and this yields 411/7.8 ~ 53, close to the depth.
    3. Without symmetry breaking and with preprocessing:
      > OKsolver_2002-m2pp -D10 -M -F GreenTao_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status=0 initial_maximal_clause_length=6 initial_number_of_variables=272 initial_number_of_clauses=3202 initial_number_of_literal_occurrences=12536 running_time(s)=6105.7 number_of_nodes=9573917 number_of_single_nodes=64902 number_of_quasi_single_nodes=0 number_of_2-reductions=63127589 number_of_pure_literals=22228 number_of_autarkies=12674 number_of_missed_single_nodes=88075 max_tree_depth=52 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=227225 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=136 file_name=GreenTao_3-3-3-3_137.cnf_m2pp_4279
           
      The relation between time and nodes is very linear:
      > TN = lm(E$time ~ E$nodes)
      > summary(TN)
      Residuals:
             Min         1Q     Median         3Q        Max
      -9.8510128 -0.0243738 -0.0152368  0.0005773  8.8206325
      Coefficients:
                   Estimate Std. Error t value Pr(>|t|)
      (Intercept) 1.740e-02  2.580e-02   0.675      0.5
      E$nodes     6.361e-04  6.845e-07 929.331   <2e-16 ***
      Residual standard error: 0.7391 on 891 degrees of freedom
      Multiple R-squared: 0.999,      Adjusted R-squared: 0.999
      F-statistic: 8.637e+05 on 1 and 891 DF,  p-value: < 2.2e-16
           
      The average number of 2-reductions is 6.6, and 272 / 6.6 ~ 41.
    4. With symmetry breaking and without preprocessing:
      > OKsolver_2002-O3-DNDEBUG -M -D10 -F GreenTao_sb_3-3_137.cnf
      s UNSATISFIABLE
      c sat_status=0 initial_maximal_clause_length=3 initial_number_of_variables=411 initial_number_of_clauses=3616 initial_number_of_literal_occurrences=10433 running_time(s)=118149.6 number_of_nodes=169930659 number_of_single_nodes=2708740 number_of_quasi_single_nodes=0 number_of_2-reductions=1325866058 number_of_pure_literals=0 number_of_autarkies=157007 number_of_missed_single_nodes=4893085 max_tree_depth=56 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=3 reduced_number_of_clauses=80 reduced_number_of_literal_occurrences=270 number_of_1-autarkies=2150926704 number_of_initial_unit-eliminations=3 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=445 file_name=GreenTao_sb_3-3_137.cnf
           
      W.r.t. the number of nodes symmetry breaking achieves a little bit better than the factor of 3 which is "expected". Time is highly linear in the nodes:
      > TN = lm(E2$time ~ E2$nodes)
      > summary(TN)
      Residuals:
           Min       1Q   Median       3Q      Max
      -33.3498  -0.7968  -0.5493  -0.1532  83.9398
      Coefficients:
                   Estimate Std. Error  t value Pr(>|t|)
      (Intercept) 5.506e-01  1.915e-01    2.875  0.00413 **
      E2$nodes    6.923e-04  4.250e-07 1628.727  < 2e-16 ***
      Residual standard error: 5.359 on 933 degrees of freedom
      Multiple R-squared: 0.9996,     Adjusted R-squared: 0.9996
      F-statistic: 2.653e+06 on 1 and 933 DF,  p-value: < 2.2e-16
           
      The average number of 2-reductions is highly concentrated around the median 7.7. 411 / 7.7 ~ 53, which is close to the depth. The number of single nodes is rather linear in the number of nodes:
      > SN = lm(E2$singles ~ E2$nodes)
      > summary(SN)
      Residuals:
           Min       1Q   Median       3Q      Max
      -3259.76   -82.93   -58.47    44.21  2392.32
      Coefficients:
                   Estimate Std. Error t value Pr(>|t|)
      (Intercept) 8.393e+01  1.722e+01   4.874 1.29e-06 ***
      E2$nodes    1.548e-02  3.822e-05 405.008  < 2e-16 ***
      Residual standard error: 481.8 on 933 degrees of freedom
      Multiple R-squared: 0.9943,     Adjusted R-squared: 0.9943
      F-statistic: 1.64e+05 on 1 and 933 DF,  p-value: < 2.2e-16
           
      The number of autarkies is quite linear in the number of nodes, with outliers, but the central axis is perfectly matched by
      > AN = lm(E2$autarkies ~ E2$nodes)
      > summary(AN)
      Residuals:
           Min       1Q   Median       3Q      Max
      -816.997  -14.188   -4.524   -4.293 2029.113
      Coefficients:
                   Estimate Std. Error t value Pr(>|t|)
      (Intercept) 4.293e+00  5.215e+00   0.823    0.411
      E2$nodes    9.003e-04  1.157e-05  77.790   <2e-16 ***
      Residual standard error: 145.9 on 933 degrees of freedom
      Multiple R-squared: 0.8664,     Adjusted R-squared: 0.8663
      F-statistic:  6051 on 1 and 933 DF,  p-value: < 2.2e-16
           
    5. With symmetry breaking and with preprocessing:
      > OKsolver_2002-m2pp -D10 -M -F GreenTao_sb_3-3_137.cnf
      s UNSATISFIABLE
      c sat_status=0 initial_maximal_clause_length=6 initial_number_of_variables=270 initial_number_of_clauses=3127 initial_number_of_literal_occurrences=12164 running_time(s)=800.1 number_of_nodes=1240869 number_of_single_nodes=6668 number_of_quasi_single_nodes=0 number_of_2-reductions=8108302 number_of_pure_literals=2701 number_of_autarkies=1427 number_of_missed_single_nodes=9847 max_tree_depth=55 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=8226 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=172 file_name=GreenTao_sb_3-3_137.cnf_m2pp_18152
           \verbatim
           Average 2-reductions ~ 6.5, and 270 / 6.5 ~ 41. Symmetry breaking is
           surprisingly effective here.
           </li>
           <li> The above "symmetry breaking" is "simple symmetry breaking",
           which should be the right form since we have k=3 here throughout. </li>
           <li> The above is the aloamo-translation; now with the (simple)
           logarithmic translation:
           \verbatim
      > OKsolver_2002-O3-DNDEBUG -M -D16 GreenTao_L_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         6
      c initial_number_of_variables           274
      c initial_number_of_clauses             3203
      c initial_number_of_literal_occurrences 18670
      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   137
      c running_time(sec)                     588.3
      c number_of_nodes                       997516
      c number_of_single_nodes                341
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                7829390
      c number_of_pure_literals               210
      c number_of_autarkies                   291
      c number_of_missed_single_nodes         1705
      c max_tree_depth                        48
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 9672
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_L_3-3-3-3_137.cnf
           
      So the logarithmic translation seems much better.
    6. And furthermore one would assume that the strong reduced translation, which uses {{1},{2},{-1,-2}} for the three values plus {{1,2}} should be even better:
      > OKsolver_2002-O3-DNDEBUG -M -D16 GreenTao_SR_3-3-3-3_136.cnf
      s SATISFIABLE
      c sat_status                            1
      c initial_maximal_clause_length         6
      c initial_number_of_variables           272
      c initial_number_of_clauses             3163
      c initial_number_of_literal_occurrences 12380
      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   136
      c running_time(sec)                     93.9
      c number_of_nodes                       134508
      c number_of_single_nodes                3762
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                848045
      c number_of_pure_literals               293
      c number_of_autarkies                   146
      c number_of_missed_single_nodes         3467
      c max_tree_depth                        44
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 1423
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_SR_3-3-3-3_136.cnf
      
      > OKsolver_2002-O3-DNDEBUG -M -D16 GreenTao_SR_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         6
      c initial_number_of_variables           274
      c initial_number_of_clauses             3203
      c initial_number_of_literal_occurrences 12538
      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   137
      c running_time(sec)                     3994.1
      c number_of_nodes                       5576907
      c number_of_single_nodes                150800
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                35551956
      c number_of_pure_literals               22901
      c number_of_autarkies                   12982
      c number_of_missed_single_nodes         124384
      c max_tree_depth                        52
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 144265
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_SR_3-3-3-3_137.cnf
           
    7. Strange the weaker performance (from the L-translation one obtains the SR-translation by performing two subsumption-resolutions): Likely the heuristics by some reason is not efficient here? Now we have much more nodes, and also many more single nodes (many also directly at level 16, and actually the root node is a single, where the branching variable is nbv(3,1), set to 1 first) and also more autarkies.) This needs to be investigated.
    8. Perhaps it plays a role that for the three colours, the first are handled (after translation) by 3-clauses, the last by 6-clauses: Perhaps this makes it unbalanced. One could try to randomise this.
    9. Minisat2-Preprocessing for the strong reduced translation has apparently only a small influence, and should be negligible.
    10. Standard symmetry-breaking, which would set nbv(3,1) to true, would had no effect on the SR-translation, since the root node is a single here; this seems to be interesting --- prime number 3 doesn't play a role in the unsatisfiability!
    11. The weak standard nested translation:
      > OKsolver_2002-O3-DNDEBUG -M -D10 GreenTao_N_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         6
      c initial_number_of_variables           272
      c initial_number_of_clauses             3066
      c initial_number_of_literal_occurrences 15330
      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   0
      c running_time(sec)                     3234.0
      c number_of_nodes                       7068419
      c number_of_single_nodes                22744
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                30832450
      c number_of_pure_literals               1931502
      c number_of_autarkies                   2933
      c number_of_missed_single_nodes         26010
      c max_tree_depth                        65
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 1527371
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_N_3-3-3-3_137.cnf
           
    12. The strong standard nested translation:
      > OKsolver_2002-O3-DNDEBUG -M -D10 GreenTao_SN_3-3-3-3_137.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         6
      c initial_number_of_variables           274
      c initial_number_of_clauses             3203
      c initial_number_of_literal_occurrences 15604
      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   137
      c running_time(sec)                     2588.2
      c number_of_nodes                       4368169
      c number_of_single_nodes                15562
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                26137544
      c number_of_pure_literals               15036
      c number_of_autarkies                   12148
      c number_of_missed_single_nodes         17394
      c max_tree_depth                        66
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 748506
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_SN_3-3-3-3_137.cnf
           
      So here the strong nested form is somewhat better than the weak nested form.
  • OKsolver_2002 without tree-pruning:
    1. Without preprocessing and without symmetry breaking:
      > system_directories/bin/OKsolver_2002_NTP-O3-DNDEBUG -M -D16 -F GreenTao_3-3_137.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         3
      c initial_number_of_variables           411
      c initial_number_of_clauses             3614
      c initial_number_of_literal_occurrences 10431
      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   411
      c running_time(sec)                     726528.6
      c number_of_nodes                       1236624567
      c number_of_single_nodes                0
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                9821525375
      c number_of_pure_literals               0
      c number_of_autarkies                   1019283
      c number_of_missed_single_nodes         0
      c max_tree_depth                        58
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 168173441743
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_3-3_137.cnf
      > E = read_oksolver_mon("GreenTao_3-3_137.cnf.mo")
      62846
      > plot_oksolver_mon_nodes(E)
      ldstep= 13 step= 8192 left= 128 right= 65536
      obs/count= 1.042856 nodes-range= 1 1248779 ave-nodes-range= 5039.079 34624.96
      > summary_oksolver(E)
      Nodes:
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
            1.0      19.0     804.5   19680.0   11700.0 1249000.0
      2-reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        0.500   7.440   7.900   8.003   8.170  44.000
      Single nodes:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
            0       0       0       0       0       0
      Autarkies:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         0.00    0.00    0.00   16.22    4.00 1514.00
      Time ~ nodes:
      [1] 0.999718
       (Intercept)      E$nodes
      0.0622892181 0.0005843438
      Single nodes ~ nodes:
      [1] NaN
      (Intercept)     E$nodes
                0           0
      Autarkies ~ nodes:
      [1] 0.723745
        (Intercept)       E$nodes
      -1.3708555637  0.0008939138
      > hist_oksolver_mon_nodes(E)
      Median= 9.651948
      Mean= 14.26423
      > hist_oksolver_mon_nodes(E,breaks="st")
      Median= 9.651948
           
      The node distribution shows two clear peakes, one around 4, the other around the mean.
    2. With symmetry breaking and with preprocessing:
      > system_directories/bin/OKsolver_2002_NTP-O3-DNDEBUG -M -D10 -F GreenTao_sb_3-3_137-m2pp.cnf
      s UNSATISFIABLE
      c sat_status                            0
      c initial_maximal_clause_length         6
      c initial_number_of_variables           270
      c initial_number_of_clauses             3127
      c initial_number_of_literal_occurrences 12164
      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   172
      c running_time(sec)                     2855.8
      c number_of_nodes                       4972865
      c number_of_single_nodes                0
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                32618680
      c number_of_pure_literals               7938
      c number_of_autarkies                   4427
      c number_of_missed_single_nodes         0
      c max_tree_depth                        55
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 30488
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_sb_3-3_137-m2pp.cnf
      > E = read_oksolver_mon("GreenTao_sb_3-3_137-m2pp.cnf.mo")
      1024
      > plot_oksolver_mon_nodes(E)
      ldstep= 7 step= 128 left= 128 right= 1024
      obs/count= 1 nodes-range= 6 858348 ave-nodes-range= 2983.664 6898.701
      > plot_oksolver_mon_nodes(E,ldstep=6)
      ldstep= 6 step= 64 left= 128 right= 1024
      obs/count= 1 nodes-range= 6 858348 ave-nodes-range= 2983.664 6898.701
      > summary_oksolver(E)
      Nodes:
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
           6.0    145.0    354.5   4856.0    976.2 858300.0
      2-reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        1.830   6.328   6.540   6.542   6.750   8.530
      Single nodes:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
            0       0       0       0       0       0
      Autarkies:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        0.000   0.000   0.000   4.323   0.000 361.000
      Time ~ nodes:
      [1] 0.9998242
       (Intercept)      E$nodes
      0.0052467076 0.0005731962
      Single nodes ~ nodes:
      [1] NaN
      (Intercept)     E$nodes
                0           0
      Autarkies ~ nodes:
      [1] 0.6404928
       (Intercept)      E$nodes
      1.8800399269 0.0005030981
      > hist_oksolver_mon_nodes(E,breaks="st")
      Median= 8.46964
      Mean= 12.24565
           
      Subdividing into 16 intervals, exactly at the edge from 8 to 9 we have a sharp peak for the node counts (at monitoring nodes). The distribution of node counts has one peak, at the median, and a heavy tail.
    3. So roughly tree-pruning achieves to speed-up the running time by a factor from 2 to 3, being more efficient in the presence of symmetry breaking with preprocessing.
Todo:
march_pl
  • n=137:
    1. First the aloamo-translation.
    2. Without symmetry breaking: stopped after 9 days (progress unclear).
    3. With symmetry breaking:
      c main():: nodeCount: 6473650
      c main():: dead ends in main: 114820
      c main():: lookAheadCount: 199038706
      c main():: unitResolveCount: 51538014
      c main():: time=874.280029
      c main():: necessary_assignments: 150625
      c main():: bin_sat: 0, bin_unsat 0
      c main():: doublelook: #: 11816985, succes #: 9269815
      c main():: doublelook: overall 6.191 of all possible doublelooks executed
      c main():: doublelook: succesrate: 78.445, average DL_trigger: 4303.527
      s UNSATISFIABLE
          
      This seems to be comparable with OKsolver_2002 (though march_pl uses more nodes).
    4. The strong reduced translation: at least no easy success (unclear how much progress after 27 m).
Todo:
satz215
  • n=137:
    1. Without symmetry breaking and without preprocessing:

    2. Without symmetry breaking and with preprocessing:
      > satz215-m2pp GreenTao_3-3-3-3_137.cnf
      NB_MONO= 1035059, NB_UNIT= -1785284987, NB_BRANCHE= 315959129, NB_BACK= 161499026
      Program terminated in 5.792 seconds.
      satz215 GreenTao_3-3-3-3_137.cnf_m2pp_18554 5.792 315959129 161499026 1880335698 722573320 0 411 3202 0 519236838 94536004
           
      perhaps 18h (csltok); strange that symmetry breaking has such an effect (a factor of 100 regarding the tree size)?!
    3. With symmetry breaking and without preprocessing:
      > satz215 GreenTao_sb_3-3_137.cnf
      NB_MONO= 0, NB_UNIT= 761352811, NB_BRANCHE= 23477136, NB_BACK= 12034648
      Program terminated in 0.231 seconds.
      satz215 GreenTao_sb_3-3_137.cnf 0.231 23477136 12034648 745507284 61984415 0 411 3616 -80 26757608 9227479
           
      So symmetry breaking alone is substantially more efficient here than preprocessing.
    4. With symmetry breaking and with preprocessing:
      NB_MONO= 20243, NB_UNIT= 70999817, NB_BRANCHE= 3163421, NB_BACK= 1594481
      Program terminated in 0.116 seconds.
      satz215 GreenTao_sb_3-3_137.cnf_m2pp_18306 0.116 3163421 1594481 404432467 18289941 0 411 3127 0 49387462 9601974
           
      Unclear how much time was spent (satz215 only uses standard C time-measurement), but perhaps 18m (on csltok). So it's slower than OKsolver_2002, and it takes more nodes, but still reasonable. Apparently the double look-ahead can achieve something.
Todo:
minisat2
  • n=137:
    1. First the aloamo-translation.
    2. Determines unsatisfiability with 2257091 conflicts (24 restarts) in less than 2 minutes.
    3. Using symmetry breaking, actually 2686891 conflicts are needed; let's assume that this is a random effect.
    4. Without preprocessing: 2748900 (24 restarts, a bit more than 2 minutes); so for minisat2 the preprocessing doesn't make a big difference.
    5. With the logarithmic translation only 1433824 conflicts (22 restarts) were needed.
    6. Strong reduced translation: 1549018 conflicts (23 restarts).
    7. Weak reduced translation: 2052041 conflicts (23 restarts).
  • n=150: seems not to make progress.
Todo:
picosat913
  • n=137:
    1. picosat913 is not as fast as minisat2: 6 1/2 minutes, 10000685 conflicts (aloamo-translation).
    2. With strong reduced translation: 8 minutes, 6993282 conflicts.
    3. With minisat2-preprocessing:
    4. With symmetry-breaking:
    5. With minisat2-preprocessing and with symmetry-breaking:
Todo:
precosat236
  • n=137:
    1. precosat236 is a bit slower than minisat2: nearly 2 1/2 minutes, 1226906 conflicts (so fewer conflicts).
    2. With symmetry breaking:
Todo:
Why is minisat2 so much faster than OKsolver_2002 ?
  • The four possible reasons seem to be:
    • (i) preprocessing
    • (ii) full resolution versus tree-resolution
    • (iii) finding an easy small sub-problem
    • (iv) faster processing (this doesn't seem to play an important role here, since minisat2 needs much less nodes than OKsolver_2002).
  • (i) can be examined by using minisat2's preprocessing for the OKsolver_2002, as well as for the other lookahead-solver, and also running minisat2 without preprocessing.
    1. It helps the conflict-driven solvers a bit, but not so much (at least in this case).
    2. So there is something else they are doing well here.
    3. It seems that look-ahead solvers are much more helped by preprocessing here (at least the OKsolver_2002); however still the number of nodes is one magnitude bigger compared with the conflict-driven solvers.
    4. When using also symmetry breaking, then the node-count of OKsolver_2002 is similar to the best node count of conflict-driven solvers; this simple symmetry-breaking is surprisingly effective at least for the OKsolver (perhaps the heuristics can be much improved?!), while it doesn't seem to help at all for conflict-driven solvers.
  • For (ii) one needed to inspect the resolution refutation produced by minisat2.
  • Easier to look at (iii), where we only need to see whether the clauses used as axioms for the resolution refutation can be easily refuted by OKsolver_2002.

Definition in file GreenTao_3-3.hpp.