OKlibrary  0.2.1.6
Numbers.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 15.7.2012 (Swansea) */
00002 /* Copyright 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/RamseyTheory/Lisp/Ramsey/Numbers.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lambda.mac")$
00025 
00026 
00027 /* *****************
00028    * Schur numbers *
00029    *****************
00030 */
00031 
00032 /* r is natural numbers >= 0: */
00033 schur(r) := if r <= 4 then [1,2,5,14,45][r+1]
00034  elseif r=5 then [161,306]
00035  elseif r=6 then [537,1837]
00036  elseif r=7 then [1681,12860]
00037  else block([lb : max(3^(r-7)*(1681-1/2)+1/2,ceiling(44/89*89^(r/4))),
00038              ub : floor(r!*%e),
00039              rub : ramsey([2,create_list(3,i,1,r)])],
00040    if rub#unknown then ub : min(ub, rub-1),
00041    [lb, ub])$
00042 /* Remarks:
00043  - This is A030126 in the OEIS (http://oeis.org/A030126).
00044  - For the general bounds see Theorems 8.8, 8.9 and Corollary 8.6 in
00045    [Ramsey Theory on the Integers; Landman, Robertson].
00046  - Schur showed that schur(r) >= 3*schur(r-1)-1 for r >= 1.
00047    The sequence s(r) := 3*s(r-1)-1 has the law s(r) = 3^r*(s(0)-1/2)+1/2.
00048    Since for r=7 we have the last concrete bound, we set s(0) = 1681.
00049  - For r = 5:
00050     - For the lower bound see certificates in
00051       Investigations/RamseyTheory/SchurProblems/plans/general.hpp.
00052     - The upper bound comes from ramsey([2,[3,3,3,3,3]]) <= 307
00053       ([Small Ramsey Numbers; Radziszowski, The Electronic Journal of
00054       Combinatorics, August 22, 2011], Page 34
00055       http://www.combinatorics.org/ojs/index.php/eljc/article/view/ds1/html).
00056  - For r = 6:
00057     - The upper bound comes from ramsey([2,[3,3,3,3,3,3]]) <= 1838
00058       ([Small Ramsey Numbers; Radziszowski, The Electronic Journal of
00059       Combinatorics, August 22, 2011]).
00060  - For r = 7:
00061     - The upper bound comes from ramsey([2,[3,3,3,3,3,3,3]]) <= 12861
00062       ([Small Ramsey Numbers; Radziszowski, The Electronic Journal of
00063       Combinatorics, August 22, 2011]).
00064 
00065 */
00066 
00067 
00068 /* **********************
00069    * Weak Schur numbers *
00070    **********************
00071 */
00072 
00073 /* r is natural numbers >= 0: */
00074 wschur(r) := if r <= 4 then [1,3,9,24,67][r+1]
00075  elseif r=5 then [190,1631]
00076  elseif r=6 then [573,11743]
00077  else block([lb : firste(schur(r)), ub : floor(r!*r*%e)+1,
00078              rub : ramsey([2,create_list(4,i,1,r)])],
00079    if rub#unknown then ub : min(ub, rub-1),
00080    rub : ramsey([2,create_list(3,i,1,2*r)]),
00081    if rub#unknown then ub : min(ub, rub-1),
00082    [lb, ub])$
00083 
00084 
00085 /* *****************************
00086    * Palindromic Schur numbers *
00087    *****************************
00088 */
00089 
00090 /* Instead of "numbers" we have "number predicates", which are true for n
00091    iff the corresponding satisfiability-problem for n is satisfiable.
00092 */
00093 
00094 /* r is natural numbers >= 0: */
00095 pdschur(r) := if r <= 4 then [ltlb(1),ltlb(2),ltlb(5),ltlb(14),ltlb(45)][r+1]
00096  elseif r=5 then lambda([n], if n>306 then false elseif n=158 or n>=161 then unknown else true)
00097  else unknown$
00098 
00099 
00100 /* r is natural numbers >= 0: */
00101 pdwschur(r) := if r <= 4 then [ltlb(1),ltlb(3),ltlb(6),ltlb(15),lambda([n], if n >= 48 or n=45 or n=46 then false else true)][r+1]
00102  elseif r=5 then lambda([n], if n>1631 then false elseif n>=161 then unknown else true)
00103  else unknown$
00104 /* Note that if a palindromic (ordinary) Schur-instance is known to be
00105    satisfiable for n mod 3 # 2, then also the weak palindromic Schur-instance
00106    for that n is satisfiable.
00107 */
00108 
00109 
00110 /* **************************
00111    * Full symmetry-breaking *
00112    **************************
00113 */
00114 
00115 /* r is natural numbers >= 0: */
00116 
00117 schurfsb(r) := if r <= 4 then [1,2,5,14,45][r+1]
00118  elseif r=5 then [161,seconde(schur(5))]
00119  elseif r=6 then unknown
00120  elseif r=7 then unknown
00121  else unknown$
00122 
00123 pdschurfsb(r) := if r <= 4 then [ltlb(1),ltlb(2),ltlb(5),ltlb(14),ltlb(45)][r+1]
00124  elseif r=5 then lambda([n], if n>seconde(schur(5)) then false elseif n<=157 or n=159 or n=160 then true else unknown)
00125  elseif r=6 then unknown
00126  elseif r=7 then unknown
00127  else unknown$
00128 
00129 
00130 wschurfsb(r) := if r <= 4 then [1,3,9,24,67][r+1]
00131  elseif r=5 then [161,seconde(wschur(5))]
00132  else unknown$
00133 
00134 pdwschurfsb(r) := if r <= 4 then [ltlb(1),ltlb(3),ltlb(6),ltlb(15),lambda([n], if n >= 48 or n=45 or n=46 then false else true)][r+1]
00135  elseif r=5 then lambda([n], if n>1631 then false elseif n<=160 then true else unknown)
00136  else unknown$
00137 
00138 /* Note that schurfsb(r) and wschurfsb(r) do not need predicates, since these
00139    problems are monotone.
00140    Satisfiability of a palindromic problem means satisfiability of the
00141    corresponding non-palindromic problem.
00142    And satisfiability of an ordinary problem means satisfiability of the
00143    corresponding weak problem, except for palindromic problems in case of
00144    n+1 divisible by 3, and also not not regarding full symmetry-breaking,
00145    since the weak form uses a different full symmetry-breaking.
00146 */
00147 
00148 
00149 /* *****************
00150    * Modular forms *
00151    *****************
00152 */
00153 
00154 /* Instead of "numbers" we have "number predicates", which are true for n
00155    iff the corresponding satisfiability-problem for n is satisfiable.
00156 */
00157 
00158 /* r is natural numbers >= 0: */
00159 mschur(r) := if r <= 4 then [ltlb(1),ltlb(2),ltlb(5),ltlb(14),ltlb(45)][r+1]
00160  elseif r=5 then unknown
00161  else unknown$
00162 /* Consider a fixed n:
00163    If the modular problem for n is satisfiable, then also the ordinary problem.
00164    And if the palindromic (ordinary) problem is satisfiable, then so is the
00165    modular problem.
00166 */
00167 
00168 /* r is natural numbers >= 0: */
00169 wmschur(r) := if r <= 4 then [ltlb(1),ltlb(3),ltlb(7),ltlb(15),
00170    lambda([n], if n<45 or n=47 then true else false)][r+1]
00171  elseif r=5 then unknown
00172  else unknown$
00173 /* Consider a fixed n:
00174    If the modular problem for n is satisfiable, then also the ordinary problem.
00175    And if the palindromic (ordinary) problem is satisfiable, then so is the
00176    modular problem.
00177 */
00178 /* Note that if a modular (ordinary) Schur-instance is satisfiable, then also
00179    the weak modular Schur-instance for that n.
00180 */
00181 
00182