OKlibrary  0.2.1.6
GreenTao_2-3-k.hpp File Reference

On investigations into Green-Tao numbers greentao_2(3,k) More...

Go to the source code of this file.


Detailed Description

On investigations into Green-Tao numbers greentao_2(3,k)

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

Todo:
Investigate greentao_2(3,k)
  • Here we get into combinatorial area ("Ramsey-like").
  • greentao_2(3,0)=0, greentao_2(3,1)=4, greentao(3,2)=7, greentao(3,3)=23.
  • greentao_2(3,4) = 79 (see below).
  • greentao_2(3,5) = 528
    1. greentao_2(3,5) > 450 (easy for OKsolver-2002)
    2. greentao_2(3,5) > 527 (trivial for ubcsat-rnovelty+).
    3. n=528 looks unsatisfiable by ubcsat-rnovelty+.
    4. OKsolver-2002 proves unsatisfiability:
      > OKsolver_2002-O3-DNDEBUG -M -D10 GreenTao_2_3_5_528.cnf
      s UNSATISFIABLE
      c sat_status=0 initial_maximal_clause_length=5 initial_number_of_variables=527 initial_number_of_clauses=12692 initial_number_of_literal_occurrences=38748 running_time(s)=-364.7 number_of_nodes=1139193 number_of_single_nodes=22186 number_of_quasi_single_nodes=0 number_of_2-reductions=11956251 number_of_pure_literals=420178 number_of_autarkies=0 number_of_missed_single_nodes=6 max_tree_depth=43 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=47664479 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=0 file_name=GreenTao_2_3_5_528.cnf
           
      (about one hour).
    5. minisat solves it even faster:
      > minisat GreenTao_2_3_5_528.cnf
      restarts              : 25
      conflicts             : 3518551        (2170 /sec)
      decisions             : 3840063        (2369 /sec)
      propagations          : 146037825      (90078 /sec)
      conflict literals     : 48001533       (41.34 % deleted)
      Memory used           : 11.35 MB
      CPU time              : 1621.24 s
           
    6. march_pl is also faster:
      > march_pl GreenTao_2_3_5_528.cnf
      c main():: nodeCount: 328459
      c main():: dead ends in main: 548
      c main():: lookAheadCount: 134392690
      c main():: unitResolveCount: 2031542
      c main():: time=1729.920000
      c main():: necessary_assignments: 51674
      c main():: bin_sat: 0, bin_unsat 0
      c main():: doublelook: #: 3653456, succes #: 3159644
      c main():: doublelook: overall 2.760 of all possible doublelooks executed
      c main():: doublelook: succesrate: 86.484, average DL_trigger: 153.978
      s UNSATISFIABLE
           
  • See Experimentation/Investigations/RamseyTheory/GreenTaoProblems/plans/GreenTao_2-3-6.hpp for greentao_2(3,6).
  • Also this sequence (starting with 4,7,23,79,528) is apparently not in that "online encyclopedia".
Todo:
SAT 2011 competition
Todo:
greentao_2(3,4) = 79
  • Easy for OKsolver:
    > OKsolver_2002-O3-DNDEBUG GreenTao_2-3-4_78.cnf
    s SATISFIABLE
    c sat_status                            1
    c initial_maximal_clause_length         4
    c initial_number_of_variables           77
    c initial_number_of_clauses             450
    c initial_number_of_literal_occurrences 1439
    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)                     0.0
    c number_of_nodes                       25
    c number_of_single_nodes                0
    c number_of_quasi_single_nodes          1
    c number_of_2-reductions                49
    c number_of_pure_literals               11
    c number_of_autarkies                   1
    c number_of_missed_single_nodes         0
    c max_tree_depth                        10
    c number_of_table_enlargements          0
    c number_of_1-autarkies                 25
    c number_of_new_2-clauses               0
    c maximal_number_of_added_2-clauses     0
    c file_name                             GreenTao_2-3-4_78.cnf
       
    and
    > OKsolver_2002-O3-DNDEBUG GreenTao_2-3-4_79.cnf
    s UNSATISFIABLE
    c sat_status                            0
    c initial_maximal_clause_length         4
    c initial_number_of_variables           78
    c initial_number_of_clauses             460
    c initial_number_of_literal_occurrences 1472
    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)                     0.0
    c number_of_nodes                       41
    c number_of_single_nodes                0
    c number_of_quasi_single_nodes          0
    c number_of_2-reductions                111
    c number_of_pure_literals               3
    c number_of_autarkies                   0
    c number_of_missed_single_nodes         0
    c max_tree_depth                        6
    c number_of_table_enlargements          0
    c number_of_1-autarkies                 37
    c number_of_new_2-clauses               0
    c maximal_number_of_added_2-clauses     0
    c file_name                             GreenTao_2-3-4_79.cnf
       
Todo:
Predicting greentao_2(3,k)
  • Analysing the sequence 4,7,23,79,528,2072 (in R):
    d = c(4,7,23,79,528,2072)
    plot(log(log(d)))
       
    it looks linear in the log-log, but the sixth value is definitely below that (one might see some oscillation).
  • Perhaps k -> exp(k^c) for some constant c, since
    plot(log(c(1,2,3,4,5,6)[-1]),log(log(d)[-1]))
       
    looks linear:
    x = log(c(1,2,3,4,5,6)[-1])
    y = log(log(d)[-1])
    plot(x,y)
    L = lm(y ~ x)
    summary(L)
     Coefficients:
                Estimate Std. Error t value Pr(>|t|)
    (Intercept) -0.22623    0.05648  -4.005   0.0279 *
    x            1.25893    0.04117  30.578 7.68e-05 ***
    lines(x,predict(L))
    C = coefficients(L)
    -0.2262296   1.2589339
       
  • So y = -0.22623 + 1.25893 * x, that is, f(k) = exp(exp(C[1]) * k^C[2]) = exp(0.797535 * k^1.2589339):
    f = function(k){exp(exp(C[1]) * k^C[2])}
    f(c(2,3,4,5,6,7,8))
     6.743988 24.044422 96.328312 423.826146 2018.493830 10301.119863 55910.95
       
  • We see that the value for f(7) underestimates the correct value --- perhaps that oscillation.

Definition in file GreenTao_2-3-k.hpp.