OKlibrary  0.2.1.6
GreenTao_2-3-7.hpp File Reference

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

Go to the source code of this file.


Detailed Description

Investigations on greentao_2(3,7)

Problems are generated by output_greentao2nd_stdname(3,7,n) at Maxima level, or by "GTSat 3 7 n" at C++ level.

Todo:
Finding the best algorithm from ubcsat
  • Is adaptnovelty+ still best?
Todo:
Survey propagation
  • For n=5000, 7500, 10000, 12500 survey propagation apparently thinks the problem is unsatisfiable, i.e., we always get
    > survey_propagation -l GreenTao_2-3-7_XX000.cnf
    <bias>:nan
    fixed 1 biased var (+0 ucp)
    .:-)
    <bias>:nan
    contradiction
       
    However these problems are all satisfiable.
  • the same behaviour for n=15000 (but here we don't know whether it's satisfiable).
Todo:
greentao_2(3,7) > 13800
  • n=5000: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=10000.
  • n=7500: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=100000.
  • n=10000: ubcsat::adaptnovelty+ finds it satisfiable with just a cutoff=1000000 (seed=3610283050).
  • n=12500
    1. > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000 -i GreenTao_2-3-7_12500.cnf
      Clauses = 4722593
      Variables = 12500
      TotalLiterals = 14173471
      FlipsPerSecond = 6550
      BestStep_Mean = 779318.300000
      Steps_Mean = 1000000.000000
      Steps_Max = 1000000.000000
      PercentSuccess = 0.00
      BestSolution_Mean = 14.200000
      BestSolution_Median = 14.000000
      BestSolution_Min = 8.000000
      BestSolution_Max = 19.000000
           
    2. Found satisfiable (first run) with cutoff=10*10^6 (seed=348690330).
  • n=13750
    1. A cutoff=100*10^6 yields in 10 runs a minimum of 2 and a maximum of 4.
    2. cutoff=10^9:
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_2-3-7_13750.cnf
             sat  min     osteps     msteps       seed
            1 0     2  162139042 1000000000 1446773825
            2 0     1  481815784 1000000000 3328367368
            3 1     0  569156743  569156743 1397463094
           
  • n=13800
    1. cutoff=10^8: In 36 runs one solution was found:
      > E = read_ubcsat("GreenTao_2-3-7_13800.cnf_OUT2")
       0  1  2  3  4
       1  3 10 17  5
      36
      > E[E$min==0,]
         sat min   osteps   msteps      seed
      21   1   0 77868065 77868065 793605254
           
    2. cutoff=10^9: three runs yield twice min=1 and once min=2.
    3. cutoff=2*10^9: one run yields min=2.
    4. So perhaps a cutoff=10^8 is more appropriate here.
  • n=13825
    1. cutoff=10^8, adaptnovelty+
       1  2  3  4  5
       2 24 56 37  8
      127
       1  2  3  4  5
       1 25 51 47  3
      127
           \endverbartim
           </li>
          </ol>
         </li>
         <li> n=13850
          <ol>
           <li> cutoff=10^7 (adaptnovelty+):
           \verbatim
       5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 27
       1  2  4 27 27 36 48 46 38 41 37 16 14 15 10  4  1  2  1
      370
           
    2. cutoff=2*10^7 (adaptnovelty+):
       3  4  5  6  7  8  9 10 12 13
       5 15 24 17 15 22 16 11  3  1
      129
           
    3. cutoff=4*10^7 (adaptnovelty+):
       1  2  3  4  5  6  7  8  9
       1 10 38 64 54 22 11  1  1
      202
           
    4. cutoff=10^8 (adaptnovelty+):
       1  2  3  4  5
       1  2 10  5  3
      21
      2 3 4
      5 8 7
      20
       2  3  4  5  6
      15 49 31  2  3
      100
           
    5. cutoff=2*10^8 (adaptnovelty+):
       1  2  3
       1  3 10
      14
           
    6. So lets consider this for now as unsatisfiable.
  • n=14000
    1. cutoff=10^9: 4 runs yield min=3.
    2. cutoff=2*10^9: 1 run yields min=3.
    3. So let's consider this for now as unsatisfiable.
  • n=14375
    1. cutoff=10^9: three times min=6. So let's consider this unsatisfiable for now.
  • n=15000
    1. > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 10000000 -i GreenTao_2-3-7_15000.cnf
             sat  min     osteps     msteps       seed
            1 0    36    9340701   10000000 1782442807
            2 0    39    5704494   10000000  470832140
            3 0    37    8891559   10000000 3612813694
            4 0    33    9055929   10000000 1719584600
            5 0    41    9854280   10000000  433897223
           
    2. cutoff multiplied with 10:
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 100000000 -i GreenTao_2-3-7_15000.cnf
             sat  min     osteps     msteps       seed
            1 0    17   43895806  100000000 1613156495
            2 0    23   98468694  100000000 3089531980
            3 0    25   57245388  100000000  293693136
           
      If this should be satisfiable then it's tough.
    3. cutoff=10^9 yields
      > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 1000000000 -i GreenTao_2-3-7_15000.cnf
             sat  min     osteps     msteps       seed
            1 0    19  760636579 1000000000 1303145336
            2 0    19  960310544 1000000000 1126725316
           
      One would need cutoff=4*10^9, but perhaps it's unsatisfiable.
    4. > ubcsat-okl -alg adaptnovelty+ -runs 10 -cutoff 4000000000 -i GreenTao_2-3-7_15000.cnf
             sat  min     osteps     msteps       seed
            1 0    15 3386525961 4000000000 1699695039
           
      So if it's still satisfiable, then it's a rather hard problem.

Definition in file GreenTao_2-3-7.hpp.