OKlibrary  0.2.1.6
GreenTao_4-3.hpp File Reference

Investigations on greentao_4(3) More...

Go to the source code of this file.


Detailed Description

Investigations on greentao_4(3)

Generated by output_greentaod_stdname(4,3,n) or output_greentaod_sb_stdname(4,3,n) at Maxima-level, and by "GTdSat 4 3 n" at C++ level.

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

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

Todo:
Best local search algorithm
  • ubcsat-okl -runs 10 -cutoff 10000 -i GreenTao_4-3_400.cnf yields the following means for the different algorithms:
    gsat 36
    gsat -v simple 37.2
    gwsat 31.1
    gsat-tabu 21.7
    hsat 36.1
    hwsat 35.4
    walksat 84.3
    walksat-tabu 48.6
    walksat-tabu -v nonull 49.7
    novelty 51
    novelty+ 50.7
    adaptnovelty+ 22.2
    rnovelty 53.6
    rnovelty+ 49.7
    saps 41.6
    rsaps 37.8
    sapsnr 42.3
    rots 21.2
    irots 38.6
    samd 20.9
       
    The best algorithms here are samd, rots, gsat-tabu and adaptnovelty+ (in this order).
  • With runs=100:
    samd 20.950000 FlipsPerSecond = 100301
    gsat-tabu 21.1 FlipsPerSecond = 68634
    rots 21.17 FlipsPerSecond = 77399
    adaptnovelty+ 22.66 FlipsPerSecond = 473934
       
    So adaptnovelty+ is the weakest w.r.t. what is reached, but it is fastest by far.
  • Now with cutoff=100*10^3:
    adaptnovelty+ 13.24 min = 8 FlipsPerSecond = 457666
    samd 13.67 min = 10 FlipsPerSecond = 95157
    gsat-tabu 13.75 min = 10 FlipsPerSecond = 94661
    rots 18.34 min = 15 FlipsPerSecond = 79853
       
    So actually adaptnovelty+ seems best by far!
  • With cutoff=10^6:
    adaptnovelty+ 9.41 min = 7
    samd 11.37 min = 7
    gsat-tabu 11.35 min = 8
    rots 17.97 min = 15
       
    So adaptnovelty+ should be clearly the best.
  • One needs to investigate preprocessing (together with symmetry breaking), whether this changes the picture. Using n=400 as above.
    1. Just the minisat2-preprocessing alone makes things far worse:
      > ubcsat-okl -runs 10 -cutoff 1000000 -alg adaptnovelty+ -i GreenTao_4-3_400-m2pp.cnf
      Clauses = 30761
      Variables = 1600
      TotalLiterals = 135432
      FlipsPerSecond = 256674
      BestStep_Mean = 368355.300000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 15.200000
      BestSolution_Median = 14.500000
      BestSolution_Min = 14.000000
      BestSolution_Max = 18.000000
      > ubcsat-okl -runs 10 -cutoff 1000000 -alg adaptnovelty+ -i GreenTao_4-3_400.cnf
      Clauses = 32364
      Variables = 1600
      TotalLiterals = 95092
      FlipsPerSecond = 542299
      BestStep_Mean = 481813.900000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 9.800000
      BestSolution_Median = 10.000000
      BestSolution_Min = 6.000000
      BestSolution_Max = 11.000000
      
      adaptnovelty+ 15.2 min = 14
      samd 80.4 min = 74
      gsat-tabu 80.5 min = 71
      rots 76.0 min = 72
      
      walksat 116.5 min = 110
           
      Once we have the tools available, we need actually to reconsider all algorithms.
    2. Just symmetry-breaking alone:
      > ubcsat-okl -runs 10 -cutoff 1000000 -alg adaptnovelty+ -i GreenTao_sb_4-3_400.cnf
      Clauses = 32367
      Variables = 1600
      TotalLiterals = 95095
      FlipsPerSecond = 477555
      BestStep_Mean = 525055.500000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 9.700000
      BestSolution_Median = 10.000000
      BestSolution_Min = 9.000000
      BestSolution_Max = 11.000000
      
      adaptnovelty+ 9.7 min = 9
      samd 11.5 min = 9
      gsat-tabu 11.1 min = 9
      rots 17.8 min = 16
           
      So it doesn't seem to help (and perhaps it actually harms). Though one should definitely apply unit-clause propagation, and see whether this improves something. And again all algorithms need to be reexamined.
    3. Both together:
      > ubcsat-okl -runs 10 -cutoff 1000000 -alg adaptnovelty+ -i GreenTao_sb_4-3_400-m2pp.cnf
      Clauses = 30488
      Variables = 1600
      TotalLiterals = 133986
      FlipsPerSecond = 281532
      BestStep_Mean = 463622.700000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 15.300000
      BestSolution_Median = 15.500000
      BestSolution_Min = 12.000000
      BestSolution_Max = 17.000000
      
      adaptnovelty+ 15.3 min = 12
      samd 83.9  min = 73
      gsat-tabu  min = 
      rots 79.2 min = 64
           
    4. The first impression is that nothing can be achieved in this way. Perhaps there is a fundamental difference between DPLL-like SAT solvers and local-search SAT solvers: The former are strongest when some "structure" exists (in the form of "attackable points"), while the latter are strongest when the problems have a kind of "random" or "uniform" "(non-)structure".
Todo:
Lower bounds: greentao_4(3) > 384
  • Best we see first where adaptnovelty+ finds easily solutions.
  • n=300 very easily satisfiable.
  • n=338 easily satisfiable.
  • n=348 found satisfiable (cutoff=10^6, seed=1463613527).
  • n=352 found satisfiable (cutoff=10^6, seed=3476207011).
  • n=355 found satisfiable (cutoff=10^6, seed=3865650519).
  • n=356 found satisfiable (cutoff=10^6, seed=1266825813).
  • n=357
    1. > ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 1000000 -i GreenTao_4-3_357.cnf
      clauses = 26471
      Variables = 1428
      TotalLiterals = 77628
      FlipsPerSecond = 659761
      BestStep_Mean = 447147.770000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 2.330000
      BestSolution_Median = 2.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 4.000000
           
      seems unsatisfiable.
    2. > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_357.cnf
      Clauses = 26471
      Variables = 1428
      TotalLiterals = 77628
      FlipsPerSecond = 628361
      BestStep_Mean = 3492205.863000
      Steps_Mean = 9675267.971000
      Steps_Max = 10000000.000000
      PercentSuccess = 5.90
      BestSolution_Mean = 1.236000
      BestSolution_Median = 1.000000
      BestSolution_Min = 0.000000
      BestSolution_Max = 2.000000
           
      A solution was found e.g. with seed=876327096.
  • n=358 found satisfiable with cutoff=10*10^6 and seed=1641133745.
  • n=359 found satisfiable with cutoff=10*10^6 and seed=2108885839.
  • n=360 found satisfiable with cutoff=10*10^6 and seed=1802549929.
  • n=361 found satisfiable with cutoff=10*10^6 and seed=1427782088 (140 runs needed).
  • n=362 found satisfiable with cutoff=10*10^6 and seed=2256326590.
  • n=363 found satisfiable with cutoff=10*10^6 and seed=342405381.
  • n=364 found satisfiable (seed=373433483)
    > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_364.cnf
    Clauses = 27420
    Variables = 1456
    TotalLiterals = 80440
    FlipsPerSecond = 602655
    BestStep_Mean = 3488853.231000
    Steps_Mean = 9993570.374000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.10
    BestSolution_Mean = 2.195000
    BestSolution_Median = 2.000000
    BestSolution_Min = 0.000000
    BestSolution_Max = 4.000000
       
  • n=365 found satisfiable (seed=2430690635)
    > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_365.cnf
    Clauses = 27543
    Variables = 1460
    TotalLiterals = 80804
    FlipsPerSecond = 598431
    BestStep_Mean = 3608383.766000
    Steps_Mean = 9990625.610000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.10
    BestSolution_Mean = 2.248000
    BestSolution_Median = 2.000000
    BestSolution_Min = 0.000000
    BestSolution_Max = 4.000000
       
  • n=366 found satisfiable (seed=3191925315).
  • n=367 found satisfiable (seed=1210488827).
    > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_367.cnf
    Clauses = 27805
    Variables = 1468
    TotalLiterals = 81580
    FlipsPerSecond = 597684
    BestStep_Mean = 3695380.296000
    Steps_Mean = 9999170.437000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.10
    BestSolution_Mean = 2.468000
    BestSolution_Median = 2.000000
    BestSolution_Min = 0.000000
    BestSolution_Max = 4.000000
       
  • n=368 found satisfiable:
    > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_368.cnf
    Clauses = 27936
    Variables = 1472
    TotalLiterals = 81968
    FlipsPerSecond = 601632
    BestStep_Mean = 3627492.165000
    Steps_Mean = 9984052.649000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.30
    BestSolution_Mean = 2.580000
    BestSolution_Median = 3.000000
    BestSolution_Min = 0.000000
    BestSolution_Max = 4.000000
       
    for example seed=1454356055.
  • n=369 found satisfiable (2 solutions in 807 runs with cutoff=10000000=10*10^6, for example seed=191448713).
  • n=370
    1. > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 10000000 -i GreenTao_4-3_370.cnf
      Clauses = 28202
      Variables = 1480
      TotalLiterals = 82756
      FlipsPerSecond = 612643
      BestStep_Mean = 3801288.200000
      Steps_Mean = 10000000.000000
      Steps_Max = 10000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 2.821000
      BestSolution_Median = 3.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 4.000000
           
    2. With cutoff=20000000 in 1295 runs one solution was found
           (seed=406385002). </li>
          </ol>
         </li>
         <li> n=375:
          <ol>
           <li>
           \verbatim
      > ubcsat-okl -alg adaptnovelty+ -runs 3000 -cutoff 10000000 -i GreenTao_4-3_375.cnf
      Clauses = 28901
      Variables = 1500
      TotalLiterals = 84828
      FlipsPerSecond = 587133
      BestStep_Mean = 3945694.062333
      Steps_Mean = 10000000.000000
      Steps_Max = 10000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 3.491667
      BestSolution_Median = 4.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 5.000000
      ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 20000000 -i GreenTao_4-3_375.cnf
      Clauses = 28901
      Variables = 1500
      TotalLiterals = 84828
      FlipsPerSecond = 577930
      BestStep_Mean = 7458479.743000
      Steps_Mean = 20000000.000000
      Steps_Max = 20000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 3.156000
      BestSolution_Median = 3.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 5.000000
      > ubcsat-okl -alg adaptnovelty+ -runs 1000 -cutoff 100000000 -i GreenTao_4-3_375.cnf
      Clauses = 28901
      Variables = 1500
      TotalLiterals = 84828
      FlipsPerSecond = 601664
      BestStep_Mean = 31289071.326000
      Steps_Mean = 100000000.000000
      Steps_Max = 100000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 2.463000
      BestSolution_Median = 2.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 4.000000
           
    3. Finally using cutoff=10^9 in 31 runs a solution (seed=1958151049, osteps=765212681) was found.
  • n=376
    1. cutoff=10^9: In 200 runs no solution was found (average-min=1.81)
    2. cutoff=2*10^9: In 200 runs 1 solution found (seed=3617483568; average-min=1.725). Perhaps still cutoff=10^9 is sufficient, but more runs are needed.
  • n=377
    1. cutoff=10^9: 200 runs yield no solution (and an average-min=1.98). Another 900 runs yield an average-min=1.951111:
      > E = read_ubcsat("GreenTao_4-3_377.OUT2")
        1   2   3
       84 776  40
      900
           
    2. cutoff=4*10^9: 100 runs yield no solution (and an average-min=1.73).
    3. Further 68 runs (cutoff=4*10^9):
       1  2
      22 46
      68
           
    4. Finally one solution was found (cutoff=4*10^9):
       0  1  2
       1 34 79
      114
           
      with osteps=878382160 and seed=296462353.
  • n=378
    1. cutoff=10^9 yields in 15 runs 14 times min=2 and once min=1. More runs:
        1   2   3
       25 281  21
      327
           
    2. cutoff=4*10^9:
      > ubcsat-okl -alg adaptnovelty+ -runs 100 -cutoff 4000000000 -i GreenTao_4-3_378.cnf
             sat  min     osteps     msteps       seed
            1 0     1 3247511031 4000000000  969465860
            2 0     2   26424461 4000000000 3292184256
            3 0     2   41342213 4000000000 2086282835
            4 0     1 2670401695 4000000000 3600327435
           
      Possibly this is satisfiable, but according to the general strategy outlined in ExperimentSystem/ControllingLocalSearch/plans/PointOfUnsatisfiability.hpp we first investigate n=376.
    3. New run with cutoff=4*10^9: 55 runs yield 7 times min=1 (rest min=2). Then with 19 runs one was successfull: osteps=3189951424, seed=4157450661.
  • n=379, cutoff=4*10^9:
    > E = read_ubcsat("GreenTao_4-3_379.cnf_OUT")
      1   2
     34 190
    224
    > E = read_ubcsat("GreenTao_4-3_379.cnf_OUT2")
     1  2
     7 45
    52
       
    finally in another 345 runs one solution was found: seed=3835287522, osteps=2675973906.
  • n=380:
    1. Aloamo, adaptnovelty+, cutoff=4*10^9: One solution was found in 110 runs: osteps=2056704946, seed=285602449.
    2. Logarithmic translation: OKsolver_2002 didn't complete a monitoring node at depth 30 (86341.6 s), unclear whether minisat2 after 32 restarts (85416 s) or precosat236 (85414.4 s) made any progress.
  • n=381:
    1. Aloamo: cutoff=2*10^9 yields in 8 runs constantly min=2 with the maximal osteps ~ 500*10^6, so it looks unsatisfiable.
    2. cutoff=4*10^9:
      > nohup ubcsat-okl -runs 1000 -cutoff 4000000000 -alg adaptnovelty+ -i GreenTao_4-3_381.cnf | tee GreenTao_4-3_381.cnf_OUT &
      > E = read_ubcsat("GreenTao_4-3_381.cnf_OUT")
        1   2   3
       49 624  28
      701
      > summary(E$osteps)
           Min.   1st Qu.    Median      Mean   3rd Qu.      Max.
      3.368e+06 2.945e+08 7.322e+08 1.041e+09 1.482e+09 3.955e+09
           
    3. Logarithmic translation: Finding best ubcsat-solver by
      E = run_ubcsat("GreenTao_L_4-3-3-3-3_380.cnf", runs=200,cutoff=1000000)
           
      evaluating it by plot(E$alg,E$best):
      > table(E$best[E$alg=="adaptnoveltyp"])
       2  3  4  5  6  7  8  9
       1  4 14 54 65 46 15  1
      > table(E$best[E$alg=="gwsat"])
       4  5  6  7  8  9 10 11
       3 15 36 36 50 40 16  4
      > table(E$best[E$alg=="rnoveltyp"])
       4  6  8  9 10 11 12 13 14 15 16 17 18 19 20
       1  1  4  4  6 10 19 25 27 42 26 17 13  4  1
           
    4. Logarithmic translation, adaptnovelty+, cutoff=10^7:
        1   2   3   4   5   6
        1  26 168 490 285  30
      1000
           
      and cutoff=2*10^7:
        1   2   3   4   5   6
        2  20 143 281  53   1
      500
           
      cutoff=4*10^7:
        1   2   3   4   5
        4  47 229 219   4
      503
           
      cutoff=8*10^7:
        1   2   3   4
       13  82 314  91
      500
           
    5. Weak nested translation, rnovelty, cutoff=2*10^7:
        1   2   3   4   5
       20 157 431 355  37
      1000
           
    6. Weak nested translation, rnovelty+, cutoff=2*10^7:
        1   2   3   4   5
       20 146 404 390  40
      1000
           
    7. Weak nested translation, rnovelty, cutoff=8*10^7:
       1  2  3  4
      12 44 54  2
      112
        0   1   2   3   4
        1  25  97 131   4
      258
           
      (seed=4041962787, osteps=14325801), while with rnovelty+:
        0   1   2   3   4
        2  35 164 222   9
      432
      > E[E$min==0,]
         sat min   osteps   msteps       seed
      56   1   0 62431299 62431299 3732998098
      70   1   0 18376184 18376184 2048479337
           
  • n=382, weak nested translation, rnovelty, cutoff=8*10^7:
      1   2   3   4
     48 238 434  64
    784
       
    while with rnovelty+:
      0   1   2   3   4   5
      4  76 430 750 155   1
    1416
       
    (best seed=517603456, osteps=28119845). So rnovelty+ seems better (and also faster).
  • n=383: weak nested standard translation, rnovelty+, cutoff=8*10^7 found two solutions in 577 runs (seed=3954065297, osteps=694138).
  • n=384: weak nested standard translation, rnovelty+,
    1. cutoff=4*10^7:
        1   2   3   4   5   6
       30 239 786 848  96   1
      2000
           
    2. cutoff=8*10^7:
        1   2   3   4
       36 277 661 252
      1226
           
    3. cutoff=32*10^7:
        1   2   3   4
       40 222 244  19
      525
        1   2   3
       24 106  60
      190
           
    4. cutoff=64*10^7: In 127 runs one solution was found (seed=2964481864, osteps=112033518).
  • n=385: weak nested standard translation, rnovelty+
    1. cutoff=32*10^7:
        1   2   3   4
       96 538 431   5
      1070
           
    2. cutoff=64*10^7:
        1   2   3
      135 338  86
      559
           
  • n=387, cutoff=10^9 yields in 22 runs only min=2,3,4; if this is to be re-examined, then cutoff=4*10^9 should be used.
  • n=400, cutoff=10^9 yields in 12 runs a minimum=4, and this only once, so this looks very tough.
  • n=450: using cutoff=10^9, one run reaches a minimum of 14, which seems hopeless.
  • n=600
    1. The instance-generation by Maxima takes far too long.
      • nbfcsfd2fcs_aloamo is rather slow, but a worse bottleneck is standardise_fcs.
      • And worst is standard_statistics_fcs!
      • Where actually these statistics are not so informative anymore, since they mix three different types of clauses. So we better should have separate statistics on the hypergraphs, on the alo- and alo-clauses, and for everything together.
    2. adaptnovelty+ reaches only values in the sixties.
Todo:
Upper bounds
Todo:
Minisat2 for n=377
  • Running minisat2 on GreenTao_sb_4-3_376.cnf for a day (32 restarts) doesn't seem to make progress.
Todo:
Picosat913 for n=377
  • Without preprocessing: Stopped after 2 days; the problem is that apparently there are no progress-indicators (or could one interprete "level" as such?), and so it's not possible to say whether any progress has been achieved.
  • With minisat2 preprocessing: Stopped after 10 hours --- hard to tell the difference (and hard to see any progress due to the confusing output).

Precosat236 for n=377

  • Stopped after 5 hours; same problem as with picosat, that there is no progress visible, and perhaps not even any such measurement (in the absence of fixed variables --- once one gets one fixed variables, then at least for these problems the solution is near).
  • If there would be at least some documentation on those various outputs, then perhaps one could try to use this for some form of classification of problem types.
Todo:
OKsolver for n=377
  • Without symmetry breaking and without preprocessing:
    > OKsolver_2002-O3-DNDEBUG -D30 -M -F GreenTao_4-3_377.cnf
    Name of file, monitoring depth and number of monitoring nodes:
     GreenTao_4-3_377.cnf,   30, 1073741824
    level: nodes processed, average nodes, predicted total nodes, time for monitoring node, average time, predicted remaining time
    s UNKNOWN
    c sat_status=2 initial_maximal_clause_length=4 initial_number_of_variables=1508 initial_number_of_clauses=29195 initial_number_of_literal_occurrences=85700 running_time(s)=96556.5 number_of_nodes=5442104 number_of_single_nodes=29075 number_of_quasi_single_nodes=0 number_of_2-reductions=77078983 number_of_pure_literals=0 number_of_autarkies=32 number_of_missed_single_nodes=55540 max_tree_depth=140 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=2218981570 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=2262 file_name=GreenTao_4-3_377.cnf
       
    No observation node at level 30 reached: From time to time an autarky is found, and also single-nodes are found (quite a few), but likely the depth is just too big.
  • Without symmetry breaking and with preprocessing:
    > OKsolver_2002-m2pp -D30 -M -F GreenTao_4-3_377.cnf
    s UNKNOWN
    c sat_status=2 initial_maximal_clause_length=9 initial_number_of_variables=1128 initial_number_of_clauses=27684 initial_number_of_literal_occurrences=121758 running_time(s)=251956.6 number_of_nodes=6807637 number_of_single_nodes=1004 number_of_quasi_single_nodes=0 number_of_2-reductions=88887630 number_of_pure_literals=3 number_of_autarkies=10 number_of_missed_single_nodes=1529 max_tree_depth=179 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=84 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=1128 file_name=GreenTao_4-3_377.cnf_m2pp_582
       
    (without completing any monitor node at level 30; regarding the tree depth it looks even worse than without reprocessing, however this might be accidental, given the large search space).
  • Interesting to note here that the number of variables and the number of 2-clauses coincide: it might be that the reduction actually establishes some new structure.
  • With symmetry breaking and without preprocessing:
    > OKsolver_2002-O3-DNDEBUG -D30 -M -F GreenTao_sb_4-3_377.cnf
    s UNKNOWN
    c sat_status=2 initial_maximal_clause_length=4 initial_number_of_variables=1508 initial_number_of_clauses=29198 initial_number_of_literal_occurrences=85703 running_time(s)=152404.7 number_of_nodes=10367390 number_of_single_nodes=81451 number_of_quasi_single_nodes=0 number_of_2-reductions=148752374 number_of_pure_literals=0 number_of_autarkies=23 number_of_missed_single_nodes=165112 max_tree_depth=136 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=4 reduced_number_of_clauses=274 reduced_number_of_literal_occurrences=899 number_of_1-autarkies=4253877291 number_of_initial_unit-eliminations=4 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=2344 file_name=GreenTao_sb_4-3_377.cnf
       
    As usual, it seems a bit improved, but not much (still no monitoring node completed).
  • With symmetry breaking and with preprocessing:
    > OKsolver_2002-m2pp -M -D30 -F GreenTao_sb_4-3_377.cnf
    s UNKNOWN
    c sat_status=2 initial_maximal_clause_length=9 initial_number_of_variables=1125 initial_number_of_clauses=27417 initial_number_of_literal_occurrences=120344 running_time(s)=419516.6 number_of_nodes=10894679 number_of_single_nodes=4 number_of_quasi_single_nodes=0 number_of_2-reductions=138939484 number_of_pure_literals=0 number_of_autarkies=20 number_of_missed_single_nodes=508 max_tree_depth=84 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=278 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=1213 file_name=GreenTao_sb_4-3_377.cnf_m2pp_16337
       
    without reaching any node at level 30; as with greentao_3(3), it looks much better when preprocessing and symmetry breaking are combined, which is strange. Also strange that suddenly there are nearly no single-nodes anymore?
  • The above "symmetry breaking" is "simple symmetry breaking", which should be the right form since we have k=3 here throughout.

Definition in file GreenTao_4-3.hpp.