OKlibrary  0.2.1.6
GreenTao_te_m-3-5.hpp File Reference

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

Go to the source code of this file.


Detailed Description

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

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

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

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

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

Todo:
greentao_3(2,3,5) = 581
  • n=550
    1. OKsolver_2002 without preprocessing: the instance allows many autarkies and single-nodes, but full processing on csltok seems to take roughly a day, and after have processed roughly 25% of the monitoring nodes no solution was found:
      > OKsolver_2002-O3-DNDEBUG -M -D16 GreenTao_3-2-3-5_550.cnf
       15167:    330     97.85  6.41E+06     3.23s     1.08s     0y   0d 15h  7m  8s     0   116   44
      
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         5
      c initial_number_of_variables           1650
      c initial_number_of_clauses             166883
      c initial_number_of_literal_occurrences 348728
      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   152625
      c running_time(sec)                     16392.5
      c number_of_nodes                       1484482
      c number_of_single_nodes                41131
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                16689392
      c number_of_pure_literals               0
      c number_of_autarkies                   496261
      c number_of_missed_single_nodes         6
      c max_tree_depth                        44
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 157064664
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_3-2-3-5_550.cnf
           
    2. OKsolver_2002 with preprocessing: seems much worse (very slow processing of nodes); autarkies and single nodes apparently disappeared (while some pure literals showed up):
      > OKsolver_2002-m2pp -M -D16 GreenTao_3-2-3-5_550.cnf
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         27
      c initial_number_of_variables           956
      c initial_number_of_clauses             144252
      c initial_number_of_literal_occurrences 333179
      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   132796
      c running_time(sec)                     1004.4
      c number_of_nodes                       177
      c number_of_single_nodes                0
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                9193
      c number_of_pure_literals               68
      c number_of_autarkies                   0
      c number_of_missed_single_nodes         0
      c max_tree_depth                        43
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 4925
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_3-2-3-5_550.cnf_m2pp_9474
           
      (three monitoring nodes were processed). One should find out what kind of disaster here happened through preprocessing (is it that OKsolver_2002 can't handle long clauses, since its heuristics is insensitive to them? but why is processing so slow? perhaps because of the tree-pruning?).
    3. march_pl: aborted after 30m (csltok), where some "progress" was achieved (according to the star-output), but no assignment was found.
    4. minisat2
    5. ubcsat: saps determined satisfiability with cutoff=10^5 in run 17.
  • n=556: cutoff=10^6 and novelty+ found a solution in run 3 (seed=695982803, osteps=675537).
  • n=557: cutoff=10^6 and novelty+ found a solution in run 12 (seed=1721874736, osteps=723073).
  • n=558:
    1. cutoff=10^6 and novelty+:
        1   2
      188  12
      200
           
    2. cutoff=10^7 and novelty+: 100 runs yield constantly min=1.
    3. OKsolver_2002-O3-DNDEBUG with monitoring-depth 16 made good progress, until in the very last part a steep increase in the number of nodes (and in the depth) happened, culminating with the very last node, which was far harder than everything else:
      > tail GreenTao_3-2-3-5_558.cnf.mo
          65526  28603   324.692   306.370     3.510      0 13524    55    10.88
          65527  49012   325.435   577.380     3.519      0 23320    55    11.09
          65528  27549   325.850   331.270     3.524      0 13835    55    10.91
          65529 562334   334.427  6488.950     3.623   5378 191960    55    11.79
          65530 837667   347.205  9069.920     3.761  17668 251517    56    11.42
          65531 138580   349.314  1507.570     3.784      0 62472    56    10.89
          65532  80440   350.536   831.820     3.797      7 39280    56    11.08
          65533 1269559   369.904 13897.170     4.009  26180 410500    57    11.42
          65534 220228   373.258  2424.560     4.045      7 103785    57    10.93
          65535 1614247   397.885 17704.900     4.316  18279 543185    58    11.52
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         5
      c initial_number_of_variables           1674
      c initial_number_of_clauses             171716
      c initial_number_of_literal_occurrences 358797
      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   157077
      c running_time(sec)                     511654.4
      c number_of_nodes                       46513164
      c number_of_single_nodes                685702
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                533093485
      c number_of_pure_literals               0
      c number_of_autarkies                   15720875
      c number_of_missed_single_nodes         332
      c max_tree_depth                        72
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 663956927
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_3-2-3-5_558.cnf
      > plot_oksolver_mon_nodes(E)
      ldstep= 13 step= 8192 left= 128 right= 65535
      obs/count= 1.172691 nodes-range= 0 1614247 ave-nodes-range= 12.391 397.885
      > summary_oksolver(E)
      Nodes:
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
            0.0       5.0      19.0     466.7      87.0 1614000.0
      2-reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         0.25   10.36   11.51   12.30   12.99   68.00
      Single nodes:
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
          0.000     0.000     0.000     6.968     0.000 26180.000
      Autarkies:
          Min.  1st Qu.   Median     Mean  3rd Qu.     Max.
           0.0      2.0      9.0    157.5     34.0 543200.0
      Time ~ nodes:
      [1] 0.997862
      (Intercept)     E$nodes
      -0.04139706  0.01093504
      Single nodes ~ nodes:
      [1] 0.8307606
      (Intercept)     E$nodes
      -0.29176246  0.01555560
      Autarkies ~ nodes:
      [1] 0.9936747
      (Intercept)     E$nodes
        5.1898732   0.3263478
      > hist_oksolver_mon_nodes(E)
      Median= 4.247928
      Mean= 8.866372
      
      > plot(E$nodes,E$ave_reductions)
      
      > invest =function(lb) {
       S = E$nodes >= lb
       N = E$nodes[S]
       R = E$ave_reductions[S]
       plot(N,R)
       cat("Nodes:\n")
       print(summary(N))
       cat("Reductions:\n")
       print(summary(R))
       length(N)
      }
      
      > invest(1)
      Nodes:
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
            1.0       5.0      20.0     469.2      87.0 1614000.0
      Reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         0.25   10.36   11.51   12.30   12.99   68.00
      [1] 55575
      > invest(100)
      Nodes:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
          100     163     307    1957     770 1614000
      Reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         8.11   10.88   11.42   11.45   11.97   15.83
      [1] 12869
      > invest(1000)
      Nodes:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         1000    1418    2214    8408    4508 1614000
      Reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         9.26   11.02   11.45   11.45   11.87   14.17
      [1] 2610
      > invest(2000)
      Nodes:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         2002    2751    4194   14300    8294 1614000
      Reductions:
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         9.59   11.03   11.46   11.44   11.84   12.96
      [1] 1417
           
      (computation aborted). Subdividing the monitoring-range into 1024 intervals, an explosion happened in interval 1024.
    4. The last plot and its investigation is interesting, suggesting that there are two types of observation-nodes: One with low node-count and a wide range of 2-red-averages (from 0 to 70), while from, say, a node count of 100 on the range of 2-red-averages is very restricted (around 11.45). So perhaps 2-reductions are very much responsible for the node count?
    5. While autarkies here seem just to occur with a very stable frequency, and don't have much influence (regarding the given numbers --- but possibly the numbers would be much bigger without them). This needs further investigation.
    6. Perhaps QCA could be applicable?!
    7. Regarding the branching, perhaps the variables are all those about the first colour, since once we set one node to the first colour, all other nodes don't get this colour (a large number of 2-clauses). What then happens very late (interval 1024)?
    8. Also using -D20 doesn't bring more inside: Again doesn't complete the last monitoring node.
      csoliver@cs-oksvr:~/OKplatform> tail nohup.out
      1048575:1617278     30.85  3.23E+07 21846.88s     0.42s     0y   0d  0h  0m  0s 21310 544482   62
      
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         5
      c initial_number_of_variables           1674
      c initial_number_of_clauses             171716
      c initial_number_of_literal_occurrences 358797
      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   157077
      c running_time(sec)                     515655.7
      c number_of_nodes                       38185392
      c number_of_single_nodes                568919
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                437581299
      c number_of_pure_literals               0
      c number_of_autarkies                   12878659
      c number_of_missed_single_nodes         265
      c max_tree_depth                        66
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 4066478903
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_3-2-3-5_558.cnf
           
      so again it fall into a deep hole at the last monitoring node, and after 8590 m no progress visible --- interestingly the rather slow 32-bit machine csltok (see above) seems faster than this 64-bit machine!.
    9. minisat2 actually finds a satisfying assignment:
      > minisat2 GreenTao_3-2-3-5_558.cnf
      |  25566627 |     978   150454   346323 |   795555   412549     33 |  0.000 % |
      ===============================================================================
      restarts              : 30
      conflicts             : 30829712       (236 /sec)
      decisions             : 40539158       (1.70 % random) (310 /sec)
      propagations          : 3289905696     (25191 /sec)
      conflict literals     : 1175934931     (26.30 % deleted)
      Memory used           : 576.89 MB
      CPU time              : 130600 s
      
      SATISFIABLE
           
      Hopefully this can be verified for example by the OKsolver.
  • n=559:
    1. cutoff=10^6 and novelty+:
      > E=read_ubcsat("GreenTao_3-2-3-5_559.cnf_OUT")
        1   2   3
      172  27   1
      200
           
    2. In a second try one solution was found quickly:
      > ubcsat-okl -alg novelty+ -cutoff 1000000 -runs 10000 -i GreenTao_3-2-3-5_559.cnf | tee GreenTao_3-2-3-5_559.cnf_OUT
             sat  min     osteps     msteps       seed
          39 1     0     925169     925169  270520321
           
    3. minisat2: abort after nearly 26 days (csltok):
      ============================[ Search Statistics ]==============================
      | Conflicts |          ORIGINAL         |          LEARNT          | Progress |
      |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
      ===============================================================================
      | 291221740 |     982   151637   348951 |  1420456   492530     29 |  0.000 % |
      *** INTERRUPTED ***
      restarts              : 36
      conflicts             : 312341917      (140 /sec)
      decisions             : 407597722      (1.75 % random) (182 /sec)
      propagations          : 32165890883    (14369 /sec)
      conflict literals     : 10963422073    (26.69 % deleted)
      Memory used           : 794.32 MB
      CPU time              : 2.23859e+06 s
           
    4. OKsolver_2002
  • n=560, cutoff=10^6 (novelty+) finds in 1074 runs one solution (seed=449744216, osteps=402793).
  • n=561, cutoff=10^6 (novelty+) finds in 256 runs one solution (seed=4223011878, osteps=161530).
  • n=562
    1. adaptnovelty+ with cutoff=10^6:
      > E=read_ubcsat("GreenTao_3-2-3-5_562.cnf_OUT")
        1   2   3
       91 104   5
      200
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       122700  262800  352800  413600  529700  996600
           
      (looks worse than for n=575 ?!)
    2. Evaluation of all ubcsat-algorithms:
      > E = run_ubcsat("GreenTao_3-2-3-5_562.cnf", cutoff=1000000,runs=100)
      plot(E$alg,E$best)
      min(E$best)
       1
      E$alg[E$best==1]
      > table(E$best[E$alg=="noveltyp"])
       1  2
      84 16
      > table(E$best[E$alg=="novelty"])
       1  2
      70 30
      > table(E$best[E$alg=="adaptnoveltyp"])
       1  2
      46 54
      > table(E$best[E$alg=="sapsnr"])
       1  2  3  4  5  6
      34 35  5  9 12  5
      > table(E$best[E$alg=="gwsat"])
       1  2  3  4
      30 61  8  1
      > table(E$best[E$alg=="saps"])
       1  2  3  4  5  6  7
      29 29  1 19 19  2  1
      > table(E$best[E$alg=="gsat_tabu"])
       1  2  3  4  5
       7 18 52 21  2
      > table(E$best[E$alg=="samd"])
       1  2  3  4  5
       3 22 49 25  1
      > table(E$best[E$alg=="walksat_tabu"])
       1  2  3  4  5  6  7  8
       1  8 16 16 24 21 13  1
      > table(E$best[E$alg=="rnoveltyp"])
       1  2  3  4  5  6  7  8  9 10 11 12
       1  3  3 10  3  5  7 15 11 19 21  2
           
      so noveltyp seems clearly best.
    3. cutoff=10^6 (novelty+) finds in 5486 runs two solutions (seed=665936935, osteps=541019):
      > E = read_ubcsat("GreenTao_3-2-3-5_562.cnf_OUT")
         0    1    2    3
         2 4663  815    6
      5486
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         8586  157900  302600  362300  524300  999700
           
    4. The osteps-summary doesn't necessarily indicate that the cutoff should be increased?
  • n=563, cutoff=10^6 (novelty+):
    > E = read_ubcsat("GreenTao_3-2-3-5_563.cnf_OUT")
       0    1    2    3
       2 4893  822   13
    5730
    > summary(E$osteps)
       Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       8135  155800  300200  358900  523700 1000000
       
    (seed=3852946212,osteps=842014). And with cutoff=2*10^6
    > E2 = read_ubcsat("GreenTao_3-2-3-5_563.cnf_OUT2")
       0    1    2
       2 1734   45
    1781
    > summary(E2$osteps)
       Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
      11080  189400  358900  508400  710900 1996000
       
  • n=564, cutoff=2*10^6 (novelty+): a solution found in run 269 (seed=547643513, osteps=1980136).
  • n=565, cutoff=2*10^6 (novelty+): two solutions found in 3390 runs (seed=1584156557, osteps=555457).
  • n=566, cutoff=2*10^6 (novelty+): one solution found in 523 runs (seed=1418552292, osteps=1384572).
  • n=575
    1. adaptnovelty+ with cutoff=10^6:
      > E=read_ubcsat("GreenTao_3-2-3-5_575.cnf_OUT")
        1   2   3
      108  91   1
      200
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       130900  331500  452000  506100  677500  992900
           
    2. cutoff=2*10^6 (novelty+): one solution found in 1012 runs
      > E = read_ubcsat("GreenTao_3-2-3-5_575.cnf_OUT")
        0   1   2
        1 996  15
      1012
      > E[E$min==0,]
          sat min  osteps  msteps       seed
      151   1   0 1480941 1480941 1122654540
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        19260  177300  317000  416600  541600 1976000
           
  • n=580
    1. cutoff=2*10^6 (novelty+) found one solution in 2482 runs:
       E = read_ubcsat("GreenTao_3-2-3-5_580.cnf_OUT")
         0    1    2    3
         1  110 2145  226
      2482
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         8632  253800  545900  673000 1010000 2000000
      > E[E$min==0,]
           sat min osteps msteps       seed
      1934   1   0 715931 715931 2205549087
           
      We see quite a change: min=2 is now the overwhelming majority; one might need to check whether under these changed circumstances perhaps now adaptnovelty+ is better.
    2. Weak standard nested translation, sapsnr, cutoff=10^6:
       0  1  2  3
       1 33 53 13
      100
           
      So it seems clear that this translation with sapsnr is superior over the aloamo-translation.
  • n=581
    1. cutoff=2*10^6 (novelty+):
      > E = read_ubcsat("GreenTao_3-2-3-5_581.cnf_OUT")
         1    2    3    4
       508 8495  995    2
      10000
      > summary(E$osteps[E$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        17010  665400 1075000 1087000 1577000 1999000
      > summary(E$osteps[E$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        10870  284400  578000  697400 1031000 1998000
      > summary(E$osteps[E$min==3])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         7201  115200  259800  349500  467900 1975000
           
    2. cutoff=2*10^6 (adaptnovelty+):
      > E = read_ubcsat("GreenTao_3-2-3-5_581.cnf_OUT2")
         1    2    3
       244 9631  125
      10000
      > summary(E$osteps[E$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       181600  702500 1126000 1139000 1587000 1979000
      > summary(E$osteps[E$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       113000  351000  516700  612800  781300 1999000
      > summary(E$osteps[E$min==3])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       121300  237900  305300  342600  405900 1131000
           
      Apparently adaptnovelty+ is better than novelty+ in avoiding the worst cases, but worse in achieving the best cases (and this should be what counts).
    3. cutoff=4*10^6 (novelty+):
      > E = read_ubcsat("GreenTao_3-2-3-5_581.cnf_OUT3")
         1    2    3
      1013 8900   87
      10000
      > summary(E$osteps[E$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        66300 1097000 1981000 2026000 2981000 3990000
      > summary(E$osteps[E$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         9536  295200  634300  853200 1178000 3991000
      > summary(E$osteps[E$min==3])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        14180  104300  239200  270900  404300  904300
           
    4. cutoff=4*10^6 (adaptnovelty+):
      > E2 = read_ubcsat("GreenTao_3-2-3-5_581.cnf_OUT4")
         1    2    3
       516 9483    1
      10000
      > summary(E$osteps[E$min==1])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        66300 1097000 1981000 2026000 2981000 3990000
      > summary(E$osteps[E$min==2])
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         9536  295200  634300  853200 1178000 3991000
           
    5. Until now here only the aloamo-translation has been considered; now we consider the weak standard nested translation.
    6. Finding the best Ubcsat-algorithm:
      > E = run_ubcsat("GreenTao_N_3-2-3-5_581.cnf")
      > plot(E$alg,E$best)
      > eval_ubcsat_dataframe(E)
      
      sapsnr :
       1  2  3  4  5  6
       5  9 27 33 22  4
      gwsat :
       1  2  3  4  5  6
       1  9 23 34 28  5
      saps :
       1  2  3  4  5  6
       1  5 29 35 24  6
           
    7. Weak standard nested translation, sapsnr, cutoff=10^6:
       1  2  3
      33 40 27
      100
        1   2   3   4
      460 589 397   7
      1453
           
    8. minisat2 determines unsatisfiability:
      > minisat2 GreenTao_N_3-2-3-5_581.cnf
      | 194147745 |     988   150528   381538 |  1366664   312117     92 |  1.980 % |
      ===============================================================================
      restarts              : 35
      conflicts             : 205723929      (154 /sec)
      decisions             : 218415159      (1.18 % random) (164 /sec)
      propagations          : 13406735824    (10053 /sec)
      conflict literals     : 17789955664    (17.80 % deleted)
      Memory used           : 1129.76 MB
      CPU time              : 1.33355e+06 s
      UNSATISFIABLE
           
      (time = 22225.83 m = 370.4306 h = 15.43461 d).
    9. picosat913 aborted (by itself):
      s UNKNOWN
      c 0 iterations
      c 1204218 restarts
      c 0 failed literals
      c 1178199461 conflicts
      c 2147483647 decisions
      c 0 fixed variables
      c 2611033505 learned literals
      c 307.8% deleted literals
      c 486216418596 propagations
      c 93.6% variables used
      c 337685.6 seconds in library
      c 1.4 megaprops/second
      c 1 simplifications
      c 5953 reductions
      c 3731.2 MB recycled
      c 117.8 MB maximally allocated
      c 337685.6 seconds total run time
           
    10. picosat913 with minisat2-preprocessing aborted (by itself):
      s UNKNOWN
      c 0 iterations
      c 1195994 restarts
      c 0 failed literals
      c 1172783603 conflicts
      c 2147483647 decisions
      c 0 fixed variables
      c 2080170219 learned literals
      c 51.3% deleted literals
      c 444333049127 propagations
      c 87.0% variables used
      c 286041.0 seconds in library
      c 1.6 megaprops/second
      c 1 simplifications
      c 7140 reductions
      c 1601.8 MB recycled
      c 102.1 MB maximally allocated
      c 286041.0 seconds total run time
           
    11. precosat236 aborted (by itself) after 733478.4 seconds, though 279 variables have been fixed. We should disable this behaviour (also with picosat).
    12. OKsolver_2002 (without preprocessing):
      1. Progress is achieved, using monitoring-depth 20, but at the last monitoring node the solver felt into a hole:
        > OKsolver_2002-O3-DNDEBUG -M -D20 -F GreenTao_N_3-2-3-5_581.cnf
        
        >  tail GreenTao_N_3-2-3-5_581.cnf.mo
          1048566  32735    33.468   302.120     0.297      0     0    63     9.80
          1048567  67514    33.532   603.040     0.297      8     0    63     9.99
          1048568  38657    33.569   342.890     0.298      0     0    63    10.14
          1048569 763553    34.297  6611.470     0.304   8883     0    63    10.16
          1048570 1277518    35.515  8391.060     0.312  22593     0    63    10.05
          1048571 188987    35.695  1239.420     0.313      7     0    63     9.80
          1048572 109535    35.800   684.820     0.314     14     0    63    10.19
          1048573 2491404    38.176 16524.260     0.329  50479     0    64     9.88
          1048574 246079    38.410  1660.240     0.331     16     0    64     9.90
          1048575 1828763    40.154 12126.630     0.343  26943     0    64     9.98
        
        s UNKNOWN
        c sat_status                            2
        c initial_maximal_clause_length         10
        c initial_number_of_variables           1161
        c initial_number_of_clauses             183634
        c initial_number_of_literal_occurrences 429344
        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   168490
        c running_time(sec)                     1016841.0
        c number_of_nodes                       136369397
        c number_of_single_nodes                2445793
        c number_of_quasi_single_nodes          0
        c number_of_2-reductions                1359006383
        c number_of_pure_literals               47933615
        c number_of_autarkies                   0
        c number_of_missed_single_nodes         3394
        c max_tree_depth                        112
        c number_of_table_enlargements          0
        c number_of_1-autarkies                 6633673123
        c number_of_new_2-clauses               0
        c maximal_number_of_added_2-clauses     0
        c file_name                             GreenTao_N_3-2-3-5_581.cnf
               
      2. Single nodes seemed to play an important node, but no autarkies were found.
      3. Very peculiar the distribution of single-node-counts: a very strong tendency towards counts which are divisible by 7:
        > E=read_oksolver_mon("GreenTao_N_3-2-3-5_581.cnf.mo")
        488652
        > T=table(E$singles)
        > as.numeric(names(T)) %% 7
          [1] 0 1 2 3 4 5 6 0 1 0 1 0 0 1 0 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 1 0 1 0
         [38] 0 0 0 1 0 0 1 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0
         [75] 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        [112] 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        > table(as.numeric(as.vector(as.data.frame(T)$Var1)) %% 7)
          0   1   2   3   4   5   6
        119  17   2   1   1   1   1
               
      4. With m2-preprocessing the problem seems to get harder for OKsolver_2002.
  • n=585, cutoff=2*10^6 (novelty+):
    > E = read_ubcsat("GreenTao_3-2-3-5_585.cnf_OUT")
       2    3    4
    1026 2809  113
    3948
    > summary(E$osteps)
       Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       8295  251200  561200  690300 1041000 1999000
       
    Either this needs much higher cutoff/runs, or it is unsatisfiable.
  • n=600
    1. saps with cutoff=10^5:
      > ubcsat-okl -alg saps -runs 100 -cutoff 100000 -i GreenTao_3-2-3-5_600.cnf | tee GreenTao_3-2-3-5_600.cnf_OUT1
      > E=read_ubcsat("GreenTao_3-2-3-5_600.cnf_OUT1")
       8  9 10 11 12 13 14 15 16 17 18
       2  2  6 13 11 16 26 15  5  3  1
      100
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
         3693   19490   41420   45090   66360   98940
           
    2. Checking all ubcsat-algorithms via
      > E = run_ubcsat("GreenTao_3-2-3-5_600.cnf")
      plot(E$alg,E$best)
      > min(E$best)
      [1] 3
      > E$alg[E$best==3]
      [1] novelty  novelty  novelty  noveltyp
      > table(E$best[E$alg=="novelty"])
       3  4  5  6  7  8  9 10
       3  5 12 15 22 19 16  8
      > table(E$best[E$alg=="noveltyp"])
       3  4  5  6  7  8  9 10 11 12
       1  2 12 14 17 24 12 13  4  1
           
      shows novelty as best.
    3. novelty with cutoff=10^6:
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        37450  255200  485000  496100  746300  996700
      > E=read_ubcsat("GreenTao_3-2-3-5_600.cnf_OUT2")
       2  3  4  5  6
       2 22 44 25  7
      100
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        23310  215500  431000  464800  727800  996700
           
    4. Checking saps with cutoff=10^6: Seems worse.
    5. Checking adaptnovelty+ with cutoff=10^6:
      > E=read_ubcsat("GreenTao_3-2-3-5_600.cnf_OUT2")
       2  3  4
       5 58 37
      100
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
       167100  305900  432400  466300  606600  972000
           
      There seems to be a general tendency that adaptnovelty+ gets better than other algorithms with higher cutoffs (while it's not good with lower cutoffs).
    6. cutoff=2*10^6, novelty+:
      > E = read_ubcsat("GreenTao_3-2-3-5_600.cnf_OUT")
        2   3   4   5   6
       11 109 106  42   3
      271
      > summary(E$osteps)
         Min. 1st Qu.  Median    Mean 3rd Qu.    Max.
        32740  483000  907800  921700 1312000 1999000
           
    7. Let's consider n=600 for now as unsatisfiable.
Todo:
greentao_4(2,2,3,5) >= 582
  • The conjecture is greentao_4(2,2,3,5) = 582.
  • Using weak standard nested translation with sapsnr.
  • Created by output_greentao_standnest_stdname(append(create_list(2,i,1,2),[3,5]),n).
  • n=581:
    1. cutoff=10^5 in 100 runs didn't find a solution.
    2. cutoff=10^6 in 100 runs yields min=1 97 times and 3 times min=2.
    3. Finding the best Ubcsat-algorithm:
      > E = run_ubcsat("GreenTao_N_4-2-2-3-5_581.cnf", runs=100,cutoff=1000000)
      > plot(E$alg,E$best)
      > eval_ubcsat_dataframe(E)
      
      saps :
       0  1  2
       5 93  2
      gwsat
       0  1  2
       3 66 31
      walksat :
       0  1  2
       2 73 25
      sapsnr :
       0  1  2
       1 91  8
      walksat_tabu :
       0  1  2
       1 58 41
      hwsat :
       0  1  2  3  4  5
       1 23 40 28  4  4
           
      So here saps seems best.
    4. saps, cutoff=10^6:
        0   1   2
       52 942   6
      1000
           
  • n=582
    1. cutoff=10^6, saps: 100 runs yield all min=1. In 1000 runs 995 times min=1, and 5 times m=2. 75% of osteps for min=1 are below 233600. Another 2000 runs yield 1984 times min=1 and 16 times min=2.
    2. gwsat, cutoff=10^6: in 1000 runs 757 times min=1, and 243 times min=2.
    3. walksat, cutoff=10^6: in 1000 runs 815 times min=1, 183 times min=2, and 2 times min=2.
    4. Considering the logarithmic translation:
      1. Finding the best Ubcsat-algorithm:
        > E = run_ubcsat("GreenTao_L_4-2-2-3-5_582.cnf", runs=100,cutoff=1000000)
        > plot(E$alg,E$best)
        > eval_ubcsat_dataframe(E)
        
        saps :
          1
        100
        sapsnr :
          1
        100
        walksat_tabu :
         1  2
        96  4
        walksat_tabu_nonull :
         1  2
        95  5
        gwsat :
         1  2
        92  8
        rnoveltyp :
         1  2
        92  8
               
        One needs to remark here that saps is by far the slowest algorithm here, and that actually w.r.t. speed (flips per second) the order of the list above is exactly reversed (with rnoveltyp around 6 times faster than saps). Though one needed to repeat this experiment on a machine with fixed processor speed.
      2. rnovelty+, cutoff=10^5:
          1   2   3
        469 500  31
        1000
               
      3. walksat-tabu with cutoff=10^5 looks far weaker than rnovelty+.
      4. sapsnr with cutoff=10^5:
          1   2   3
        574 407  19
        1000
               
    5. OKsolver_2002:
      > OKsolver_2002-O3-DNDEBUG -M -D20 GreenTao_N_4-2-2-3-5_582.cnf
      
      524287:2000514     71.86  7.54E+07 20504.79s     0.63s     0y   3d 20h 18m 19s 48216     0   69
      
      s UNKNOWN
      c sat_status                            2
      c initial_maximal_clause_length         15
      c initial_number_of_variables           1745
      c initial_number_of_clauses             353339
      c initial_number_of_literal_occurrences 1153461
      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   169071
      c running_time(sec)                     1560686.8
      c number_of_nodes                       188207805
      c number_of_single_nodes                3194685
      c number_of_quasi_single_nodes          0
      c number_of_2-reductions                1866485094
      c number_of_pure_literals               65236419
      c number_of_autarkies                   0
      c number_of_missed_single_nodes         15526
      c max_tree_depth                        140
      c number_of_table_enlargements          0
      c number_of_1-autarkies                 9082462499
      c number_of_new_2-clauses               0
      c maximal_number_of_added_2-clauses     0
      c file_name                             GreenTao_N_4-2-2-3-5_582.cnf
           
      So at the node for the completion of the left subtree the solver felt into a hole (18 days spent). Also here a strong regularity w.r.t. the counts of single-nodes was observed (strong preference of multiples of 7).
Todo:
greentao_5(2,2,2,3,5) >= 610
  • The conjecture is greentao_5(2,2,2,3,5) = 610.
  • Using weak standard nested translation with saps.
  • n=582
    1. cutoff=10^5:
       1  2  3
      12 78 10
      100
           
    2. Finding the best Ubcsat-algorithm:
      > E = run_ubcsat("GreenTao_N_5-2-2-2-3-5_582.cnf")
      > plot(E$alg,E$best)
      > eval_ubcsat_dataframe(E)
      
      walksat :
       0  1  2  3  4
       1 19 51 21  8
      saps :
       1  2  3
      16 70 14
      gwsat :
       1  2  3  4  5
      12 31 40 13  4
      sapsnr :
       1  2  3
       9 70 21
      walksat_tabu :
       1  2  3  4
       5 27 47 21
      rnovelty :
       1  2  3  4
       2 42 48  8
      hwsat :
       1  2  3  4  5  6  7  8  9
       2 14 19 27 18 10  7  1  2
      rsaps :
       1  2  3  4  5  6  7  8
       2  3 20 39 14  9  7  6
      rnoveltyp :
       1  2  3  4
       1 37 49 13
      walksat_tabu_nonull :
       1  2  3  4  5
       1 31 43 24  1
      noveltyp :
       1  2  3  4  5
       1 12 48 35  4
      rots :
       1  2  3  4  5  6  7  8
       1  5 21 30 26 13  3  1
           
      So walksat looks like a clear winner.
  • n=583, walksat, cutoff=10^5: in 17 runs one solution was found (seed=3001400000, osteps=97947).
  • n=584
    1. walksat, cutoff=10^5:
       1  2  3  4  5
      24 66 87 20  3
      200
           
    2. walksat, cutoff=2*10^5: In 61 runs one solution was found (seed=3856782094, osteps=144523).
  • n=585, walksat, cutoff=2*10^5: Found a solution in 12 runs (seed=2413939155, osteps=134993).
  • n=586, walksat, cutoff=2*10^5: in run 44 a solution was found (seed=3886996291, osteps=136280).
  • n=587, walksat, cutoff=2*10^5: in run 90 a solution was found (seed=2632716927, osteps=54379).
  • n=588, walksat, cutoff=2*10^5: in run 39 a solution was found (seed=2347578362, osteps=90750).
  • n=589, walksat, cutoff=2*10^5: in run 40 a solution was found (seed=3563485142, osteps=143655).
  • n=590, walksat:
    1. cutoff=2*10^5:
       1  2  3  4  5
      25 98 56 18  3
      200
           
    2. cutoff=4*10^5:
        1   2   3
       66 104  30
      200
           
    3. cutoff=8*10^5: in run 21 a solution was found (seed=4185694717, osteps=520400).
  • n=591, walksat, cutoff=8*10^5: in run 108 a solution was found (seed=2891578849, osteps=134677).
  • n=592, walksat, cutoff=8*10^5: in run 115 a solution was found (seed=1172758495, osteps=245146).
  • n=593, walksat, cutoff=8*10^5: in run 37 a solution was found (seed=486754794, osteps=366951).
  • n=594, walksat, cutoff=8*10^5: in run 200 a solution was found (seed=945147507, osteps=415889).
  • n=595, walksat
    1. cutoff=8*10^5:
       1  2  3
      66 87 20
      173
           
    2. cutoff=10^6: In run 30 a solution was found (seed=3948629926, osteps=642601).
  • n=596, walksat, cutoff=10^6: In run 81 a solution was found (seed=841240642, osteps=348363).
  • n=597, walksat, cutoff=10^6: In run 38 a solution was found (seed=1493254021, osteps=155394).
  • n=598, walksat, cutoff=10^6: In run 48 a solution was found (seed=2759806596, osteps=288326).
  • n=599, walksat, cutoff=10^6: In run 107 a solution was found (seed=3466890966, osteps=476027).
  • n=600, walksat, cutoff=10^6: In run 120 a solution was found (seed=3925517125, osteps=820231).
  • n=601, walksat, cutoff=10^6: In run 6 a solution was found (seed=4169526379, osteps=735193).
  • n=602, walksat, cutoff=10^6: In run 46 a solution was found (seed=4270496857, osteps=105307).
  • n=603, walksat, cutoff=10^6: In run 155 a solution was found (seed=2616932593, osteps=144966).
  • n=604, walksat, cutoff=10^6: In run 7 a solution was found (seed=2000091215, osteps=41846).
  • n=605, walksat, cutoff=10^6: In run 21 a solution was found (seed=3901374280, osteps=332675).
  • n=606, walksat, cutoff=10^6: In run 38 a solution was found (seed=2868885090, osteps=699872).
  • n=607, walksat, cutoff=10^6:
      1   2   3
    105  92   3
    200
       
    In another 151 runs a solution was found (seed=3961377519, osteps=158435).
  • n=608, walksat
    1. cutoff=10^5: In run 2937 a solution was found (seed=3990638596, osteps=95877).
    2. cutoff=10^6:
        1   2   3
      209 179  12
      400
        1   2   3
      179 173   6
      358
           
  • n=609, walksat: cutoff=10^5 finds a solution in run 4561 (seed=886206866, osteps=78635), while cutoff=10^6 finds a solution in run 51 (seed=456485295, osteps=928598).
  • n=610, walksat
    1. cutoff=10^5:
         1    2    3    4    5    6    7    8    9
       191 1292 2864 3095 1818  617  110   10    3
      10000
           
      li> cutoff=2*10^5:
         1    2    3    4    5    6    7
       752 3053 3828 1966  367   32    2
      10000
           
    2. cutoff=10^6:
        1   2   3
      486 482  32
      1000
           
    3. cutoff=10^6:
        1   2
      794 206
      1000
           

Definition in file GreenTao_te_m-3-5.hpp.