OKlibrary  0.2.1.6
GreenTaoProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 30.12.2009 (Swansea) */
00002 /* Copyright 2009, 2010, 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/Hypergraphs/Lisp/Generators/GreenTao.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00032 
00033 
00034 /* *****************************************
00035    * Arithmetic progressions in the primes *
00036    *****************************************
00037 */
00038 
00039 /* General remark: Generated formal clause-lists have multiple
00040    clause-occurrences iff there are multiple progression lengths zero;
00041    otherwise we have ordered clause-sets.
00042 */
00043 
00044 /* Boolean formal clause-sets, whose solutions are the partitionings of 
00045    the set of the first n prime numbers into two parts such that none of them 
00046    contains an arithmetic progression of size k.
00047    The variables are the first n prime numbers.
00048 */
00049 greentao2_fcl(k,n) := tcol2sat_stdohg2stdfcl(arithprog_primes_ohg(k,n))$
00050 greentao2_fcs(k,n) := fcl2fcs(greentao2_fcl(k,n))$
00051 
00052 /* More generally, create boolean formal clause-sets encoding the 
00053    partitionings of the first n prime numbers into two parts such that the
00054    first part (value 0) does not contain an arithmetic progression of size k1,
00055    whiel the second part (value 1) does not contain an arithmetic progression
00056    of size k2 ("nd" for "non-diagonal"):
00057 */
00058 greentao2nd_fcl(k1,k2,n) := block(
00059  [G1 : arithprog_primes_ohg(k1,n), G2 : arithprog_primes_ohg(k2,n)],
00060   [G1[1], append(G1[2], comp_cl(G2[2]))])$
00061 greentao2nd_fcs(k1,k2,n) := fcl2fcs(greentao2nd_fcl(k1,k2,n))$
00062 
00063 
00064 /* Now the general form, where L is an extended vdW-parameter-tuple: */
00065 greentao_nbfclud(L,n) := 
00066  if emptyp(L) then [primes_first(n),[],[]] else
00067  block([LG : [], old_k : -1, old_hg],
00068   for k in L do (
00069     if k > old_k then (
00070       old_hg : arithprog_primes_ohg(k,n),
00071       old_k : k
00072     ),
00073     LG : cons(old_hg,LG)
00074   ),
00075   return(
00076     gcol2sat_stdohg2stdnbfclud(reverse(LG),create_list(i,i,1,length(L)))))$
00077 
00078 greentao_nbfcsud(L,n) := nbfclud2nbfcsud(greentao_nbfclud(L,n))$
00079 
00080 /* Remarks: Validity of L is tested by extvanderwaerden_p(L) in
00081    ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/Numbers.mac.
00082 */
00083 
00084 
00085 /* The diagonal case (m parts, arithmetic progressions of size k): */
00086 greentaod_nbfclud(m,k,n) := 
00087  if m=0 then [primes_first(n),[],[]] else
00088  block([G : arithprog_primes_ohg(k,n)],
00089     gcol2sat_stdohg2stdnbfclud(create_list(G,i,1,m),create_list(i,i,1,m)))$
00090 
00091 greentaod_nbfcsud(m,k,n) := nbfclud2nbfcsud(greentaod_nbfclud(m,k,n))$
00092 
00093 
00094 /* ****************************************
00095    * Translation into boolean clause-sets *
00096    ****************************************
00097 */
00098 
00099 /* Translating the general forms into boolean clause-sets via the
00100    (strong) standard translation: */
00101 greentao_aloamo_fcl(L,n) :=
00102   nbfclud2fcl_aloamo(greentao_nbfclud(L,n))$
00103 greentao_aloamo_fcs(L,n) := fcl2fcs(greentao_aloamo_fcl(L,n))$
00104 
00105 
00106 /* Translating the general forms into boolean clause-sets via the
00107    standard nested translation; here L must be non-empty:
00108 */
00109 greentao_standnest_fcl(L,n) :=
00110   nbfclud2fcl_standnest(greentao_nbfclud(L,n))$
00111 greentao_standnest_fcs(L,n) := fcl2fcs(greentao_standnest_fcl(L,n))$
00112 
00113 greentao_standnest_strong_fcl(L,n) :=
00114   nbfclud2fcl_standnest_strong(greentao_nbfclud(L,n))$
00115 greentao_standnest_strong_fcs(L,n) := fcl2fcs(greentao_standnest_strong_fcl(L,n))$
00116 
00117 
00118 /* Translating the general forms into boolean clause-sets via the
00119    logarithmic translation; here L must be non-empty:
00120 */
00121 greentao_logarithmic_fcl(L,n) :=
00122   nbfclud2fcl_logarithmic(greentao_nbfclud(L,n))$
00123 greentao_logarithmic_fcs(L,n) := fcl2fcs(greentao_logarithmic_fcl(L,n))$
00124 
00125 
00126 /* Translating the general forms into boolean clause-sets via the
00127    standard reduced translation; here L must be non-empty:
00128 */
00129 greentao_reduced_fcl(L,n) :=
00130   nbfclud2fcl_reduced(greentao_nbfclud(L,n))$
00131 greentao_reduced_fcs(L,n) := fcl2fcs(greentao_reduced_fcl(L,n))$
00132 
00133 greentao_reduced_strong_fcl(L,n) :=
00134   nbfclud2fcl_reduced_strong(greentao_nbfclud(L,n))$
00135 greentao_reduced_strong_fcs(L,n) := fcl2fcs(greentao_reduced_strong_fcl(L,n))$
00136 
00137 
00138 /* *********************
00139    * Symmetry breaking *
00140    *********************
00141 */
00142 
00143 /* Symmetry breaking for n >= 2, forcing prime 3 into the first block: */
00144 greentao2_sb_fcs(k,n) := block([G : greentao2_fcs(k,n)],
00145  [G[1], adjoin({-3}, G[2])])$
00146 
00147 /* Symmetry breaking for n >= 2, forcing prime 3 into the first blocks
00148    of sections of equal progression lengths: */
00149 greentao_sb_aloamo_fcs(L,n) := block(
00150  [FF : greentao_aloamo_fcs(L,n), 
00151   sbC : {}, old_k : 0],
00152   for i : 1 thru length(L) do block([k : L[i]],
00153     if k > old_k then (
00154       sbC : adjoin(nbv_var(3,i), sbC),
00155       old_k : k
00156   )),
00157   return([FF[1], adjoin(sbC,FF[2])]))$
00158 
00159 /* Symmetry breaking for n >= 2, forcing prime 3 into the first block: */
00160 greentaod_sb_nbfcsud(m,k,n) := block([G : greentaod_nbfcsud(m,k,n)],
00161  [G[1], union(setify(create_list({[3,i]},i,2,m)), G[2]), G[3]])$
00162 
00163 
00164 /* ************************
00165    * Statistics functions *
00166    ************************
00167 */
00168 
00169 
00170 
00171 
00172 /* *******************
00173    * Standardisation *
00174    *******************
00175 */
00176 
00177 /* Standardising the standard translation */
00178 
00179 /* Computing translation functions for standardising resp. de-standardising
00180    terms resp. individual variables; P is here the list of the first
00181    n prime numbers (while [L,n] are the Green-Tao parameters):
00182 */
00183 standardise_greentao_aloamo(L,P) := block(
00184  [m : length(L),
00185   A : osm2ary_lt(l2osm_inv(P),last(P),fixnum)],
00186   buildq([m,A], lambda([t], ev(t, nbv(v,i):=(A[v]-1)*m+i, nbv))))$
00187 
00188 invstandardise_greentao_aloamo(L,P) := block(
00189  [m : length(L),
00190   A : osm2ary_lt(l2osm(P),length(P),fixnum)],
00191   buildq([m,A], lambda([i], block([d : divide(i-1,m)+1],
00192     nbv_var(A[d[1]], d[2])))))$
00193 
00194 /* Computing the pair [FF,V], where FF is the standardised form of
00195    greentao_aloamo_fcl(L,n), while V is the list of original variables:
00196 */
00197 greentao_aloamo_stdfcl(L,n) :=
00198  if n=0 then 
00199    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00200  else
00201  block([m : length(L), FF : greentao_nbfclud(L,n)],
00202   [block([s : standardise_greentao_aloamo(L,FF[1])],
00203      s(nbfclud2fcl_aloamo(FF))),
00204    block([invs : invstandardise_greentao_aloamo(L,FF[1])],
00205      create_list(invs(i), i,1,n*m))])$
00206 /* We have greentao_aloamo_stdfcl(L,n) =
00207    standardise_fcl(greentao_aloamo_fcl(L,n)).
00208 */
00209 
00210 
00211 /* Standardising the standard nested translation */
00212 
00213 /* Computing translation functions for standardising resp. de-standardising
00214    terms resp. individual variables; P is here the list of the first
00215    n prime numbers (while [L,n] are the Green-Tao parameters):
00216 */
00217 standardise_greentao_standnest(L,P) := block(
00218  [m : length(L),
00219   A : osm2ary_lt(l2osm_inv(P),last(P),fixnum)],
00220   buildq([m,A], lambda([t], ev(t, nbv(v,i):=(A[v]-1)*(m-1)+i, nbv))))$
00221 
00222 invstandardise_greentao_standnest(L,P) := block(
00223  [m : length(L),
00224   A : osm2ary_lt(l2osm(P),length(P),fixnum)],
00225   buildq([m,A], lambda([i], block([d : divide(i-1,m-1)+1],
00226     nbv_var(A[d[1]], d[2])))))$
00227 
00228 /* Computing the pair [FF,V], where FF is the standardised form of
00229    greentao_standnest_fcl, while V is the list of original variables:
00230 */
00231 greentao_standnest_stdfcl(L,n) :=
00232  if n=0 then 
00233    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00234  else
00235  block([m : length(L), FF : greentao_nbfclud(L,n)],
00236   [block([s : standardise_greentao_standnest(L,FF[1])],
00237      s(nbfclud2fcl_standnest(FF))),
00238    block([invs : invstandardise_greentao_standnest(L,FF[1])],
00239      create_list(invs(i), i,1,n*(m-1)))])$
00240 /* We have greentao_standnest_stdfcl(L,n) =
00241    standardise_fcl(greentao_standnest_fcl(L,n)).
00242 */
00243 
00244 greentao_standnest_strong_stdfcl(L,n) :=
00245  if n=0 then 
00246    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00247  else
00248  block([m : length(L), FF : greentao_nbfclud(L,n)],
00249   [block([s : standardise_greentao_standnest(L,FF[1])],
00250      s(nbfclud2fcl_standnest_strong(FF))),
00251    block([invs : invstandardise_greentao_standnest(L,FF[1])],
00252      create_list(invs(i), i,1,n*(m-1)))])$
00253 /* We have greentao_standnest_strong_stdfcl(L,n) =
00254    standardise_fcl(greentao_standnest_strong_fcl(L,n)).
00255 */
00256 
00257 
00258 /* Standardising the logarithmic translation */
00259 
00260 /* Computing translation functions for standardising resp. de-standardising
00261    terms resp. individual variables; P is here the list of the first
00262    n prime numbers (while [L,n] are the Green-Tao parameters):
00263 */
00264 standardise_greentao_logarithmic(L,P) := block(
00265  [m : cld(length(L)),
00266   A : osm2ary_lt(l2osm_inv(P),last(P),fixnum)],
00267   buildq([m,A], lambda([t], ev(t, nbv(v,i):=(A[v]-1)*m+i, nbv))))$
00268 
00269 invstandardise_greentao_logarithmic(L,P) := block(
00270  [m : cld(length(L)),
00271   A : osm2ary_lt(l2osm(P),length(P),fixnum)],
00272   buildq([m,A], lambda([i], block([d : divide(i-1,m)+1],
00273     nbv_var(A[d[1]], d[2])))))$
00274 
00275 /* Computing the pair [FF,V], where FF is the standardised form of
00276    greentao_logarithmic_fcl, while V is the list of original variables:
00277 */
00278 greentao_logarithmic_stdfcl(L,n) :=
00279  if n=0 then 
00280    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00281  else
00282  block([m : cld(length(L)), FF : greentao_nbfclud(L,n)],
00283   [block([s : standardise_greentao_logarithmic(L,FF[1])],
00284      s(nbfclud2fcl_logarithmic(FF))),
00285    block([invs : invstandardise_greentao_logarithmic(L,FF[1])],
00286      create_list(invs(i), i,1,n*m))])$
00287 /* We have greentao_logarithmic_stdfcl(L,n) =
00288    standardise_fcl(greentao_logarithmic_fcl(L,n)).
00289 */
00290 
00291 
00292 /* Standardising the reduced translation */
00293 
00294 /* Computing the pair [FF,V], where FF is the standardised form of
00295    greentao_reduced_fcl, while V is the list of original variables:
00296 */
00297 greentao_reduced_stdfcl(L,n) :=
00298  if n=0 then 
00299    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00300  else
00301  block([m : length(L), FF : greentao_nbfclud(L,n)],
00302   [block([s : standardise_greentao_standnest(L,FF[1])],
00303      s(nbfclud2fcl_reduced(FF))),
00304    block([invs : invstandardise_greentao_standnest(L,FF[1])],
00305      create_list(invs(i), i,1,n*(m-1)))])$
00306 /* We have greentao_reduced_stdfcl(L,n) =
00307    standardise_fcl(greentao_reduced_fcl(L,n)).
00308 */
00309 
00310 greentao_reduced_strong_stdfcl(L,n) :=
00311  if n=0 then 
00312    [[[],create_list({},i,1,length(sublist(L,lambda([x],is(x=0)))))],[]] 
00313  else
00314  block([m : length(L), FF : greentao_nbfclud(L,n)],
00315   [block([s : standardise_greentao_standnest(L,FF[1])],
00316      s(nbfclud2fcl_reduced_strong(FF))),
00317    block([invs : invstandardise_greentao_standnest(L,FF[1])],
00318      create_list(invs(i), i,1,n*(m-1)))])$
00319 /* We have greentao_reduced_strong_stdfcl(L,n) =
00320    standardise_fcl(greentao_reduced_strong_fcl(L,n)).
00321 */
00322 
00323 
00324 /* ********************
00325    * Output functions *
00326    ********************
00327 */
00328 
00329 /* The 2-colour diagonal version: */
00330 output_greentao2(k,n,filename) := block(
00331  [FFGT : standardise_fcl(greentao2_fcl(k,n))],
00332   output_fcl_v(
00333     sconcat("Green-Tao problem (diagonal form), 
00334 c created by the OKlibrary at ", timedate(),":
00335 c 2 parts, arithmetic progressions of size ", k, ", and ", n, " prime numbers.
00336 c Variables and associated prime numbers:"), 
00337     FFGT[1],
00338     filename,
00339     FFGT[2]))$
00340 /* Providing a standard name: "GreenTao_2-k_n.cnf": */
00341 output_greentao2_stdname(k,n) := output_greentao2(k,n,
00342   sconcat("GreenTao_2-",k,"_",n,".cnf"))$
00343 
00344 /* The 2-colour non-diagonal version: */
00345 output_greentao2nd(k1,k2,n,filename) := block(
00346  [FFGT : standardise_fcl(greentao2nd_fcl(k1,k2,n))],
00347   output_fcl_v(
00348     sconcat("Green-Tao problem (non-diagonal form),
00349 c created by the OKlibrary at ", timedate(),": 
00350 c 2 parts, arithmetic progressions of size ", k1, " and ", k2, ", and ", n, " prime numbers.
00351 c Variables and associated prime numbers:"), 
00352     FFGT[1],
00353     filename,
00354     FFGT[2]))$
00355 /* Providing a standard name: "GreenTao_2-k1-k2_n.cnf": */
00356 output_greentao2nd_stdname(k1,k2,n) := output_greentao2nd(k1,k2,n,
00357   sconcat("GreenTao_2-",k1,"-",k2,"_",n,".cnf"))$
00358 
00359 /* The general form, with aloamo-translation: */
00360 output_greentao(L,n,filename) := block(
00361  [FF : greentao_aloamo_stdfcl(L,n)],
00362   output_fcl_v(
00363     sconcat("Green-Tao problem (general form),
00364 c created by the OKlibrary at ", timedate(),": 
00365 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00366 c and ", n, " prime numbers.
00367 c Variables and associated prime numbers and \"colours\":"),
00368     FF[1],
00369     filename,
00370     FF[2]))$
00371 output_greentao_stdname(L,n) := output_greentao(L,n,
00372   sconcat("GreenTao_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00373 
00374 /* The general form, with standard-nested-translation: */
00375 output_greentao_standnest(L,n,filename) := block(
00376  [FF : greentao_standnest_stdfcl(L,n)],
00377   output_fcl_v(
00378     sconcat("Green-Tao problem, translated via standard nested translation to the boolean form,
00379 c created by the OKlibrary at ", timedate(),": 
00380 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00381 c and ", n, " prime numbers.
00382 c Variables and associated prime numbers and \"colours\":"),
00383     FF[1],
00384     filename,
00385     FF[2]))$
00386 output_greentao_standnest_stdname(L,n) := output_greentao_standnest(L,n,
00387   sconcat("GreenTao_N_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00388 
00389 output_greentao_standnest_strong(L,n,filename) := block(
00390  [FF : greentao_standnest_strong_stdfcl(L,n)],
00391   output_fcl_v(
00392     sconcat("Green-Tao problem, translated via strong standard nested translation to the boolean form,
00393 c created by the OKlibrary at ", timedate(),": 
00394 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00395 c and ", n, " prime numbers.
00396 c Variables and associated prime numbers and \"colours\":"),
00397     FF[1],
00398     filename,
00399     FF[2]))$
00400 output_greentao_standnest_strong_stdname(L,n) := output_greentao_standnest_strong(L,n,
00401   sconcat("GreenTao_SN_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00402 
00403 /* The general form, logarithmic translation: */
00404 output_greentao_logarithmic(L,n,filename) := block(
00405  [FF : greentao_logarithmic_stdfcl(L,n)],
00406   output_fcl_v(
00407     sconcat("Green-Tao problem, translated via logarithmic translation to the boolean form,
00408 c created by the OKlibrary at ", timedate(),": 
00409 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00410 c and ", n, " prime numbers.
00411 c Variables and associated prime numbers and \"colours\":"),
00412     FF[1],
00413     filename,
00414     FF[2]))$
00415 output_greentao_logarithmic_stdname(L,n) := output_greentao_logarithmic(L,n,
00416   sconcat("GreenTao_L_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00417 
00418 
00419 /* The general form, with standard reduced translation: */
00420 output_greentao_reduced(L,n,filename) := block(
00421  [FF : greentao_reduced_stdfcl(L,n)],
00422   output_fcl_v(
00423     sconcat("Green-Tao problem, translated via standard reduced translation to the boolean form,
00424 c created by the OKlibrary at ", timedate(),": 
00425 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00426 c and ", n, " prime numbers.
00427 c Variables and associated prime numbers and \"colours\":"),
00428     FF[1],
00429     filename,
00430     FF[2]))$
00431 output_greentao_reduced_stdname(L,n) := output_greentao_reduced(L,n,
00432   sconcat("GreenTao_R_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00433 
00434 output_greentao_reduced_strong(L,n,filename) := block(
00435  [FF : greentao_reduced_strong_stdfcl(L,n)],
00436   output_fcl_v(
00437     sconcat("Green-Tao problem, translated via strong standard reduced translation to the boolean form,
00438 c created by the OKlibrary at ", timedate(),": 
00439 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00440 c and ", n, " prime numbers.
00441 c Variables and associated prime numbers and \"colours\":"),
00442     FF[1],
00443     filename,
00444     FF[2]))$
00445 output_greentao_reduced_strong_stdname(L,n) := output_greentao_reduced_strong(L,n,
00446   sconcat("GreenTao_SR_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00447 
00448 
00449 /* The general form with aloamo-translation and with symmetry breaking: */
00450 output_greentao_sb(L,n,filename) := block(
00451  [FF : standardise_fcs(greentao_sb_aloamo_fcs(L,n))],
00452   output_fcs_v(
00453     sconcat("Green-Tao problem (general form),
00454 c created by the OKlibrary at ", timedate(),": 
00455 c ", length(L), " parts with arithmetic progressions of sizes ", L, "
00456 c and ", n, " prime numbers.
00457 c Symmetry breaking by putting prime 3 into the first parts
00458 c   of constant segments of progression lengths.
00459 c Variables and associated prime numbers and \"colours\":"),
00460     FF[1],
00461     filename,
00462     FF[2]))$
00463 output_greentao_sb_stdname(L,n) := output_greentao_sb(L,n,
00464   sconcat("GreenTao_sb_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))$
00465 
00466 
00467 /* The diagonal case, with aloamo-translation (m is the number of parts, 
00468    k the length or arithmetic progressions): */
00469 output_greentaod(m,k,n,filename) := block(
00470  [FF : standardise_fcs(nbfcsfd2fcs_aloamo(nbfcsud2nbfcsfd(greentaod_nbfcsud(m,k,n))))],
00471   output_fcs_v(
00472     sconcat("Green-Tao problem (diagonal form),
00473 c created by the OKlibrary at ", timedate(),": 
00474 c ", m, " parts with arithmetic progressions of sizes ", k, "
00475 c and ", n, " prime numbers.
00476 c Variables and associated prime numbers and \"colours\":"),
00477     FF[1],
00478     filename,
00479     FF[2]))$
00480 output_greentaod_stdname(m,k,n) := output_greentaod(m,k,n,
00481   sconcat("GreenTao_",m,"-",k,"_",n,".cnf"))$
00482 
00483 output_greentaod_sb(m,k,n,filename) := block(
00484  [FF : standardise_fcs(nbfcsfd2fcs_aloamo(nbfcsud2nbfcsfd(greentaod_sb_nbfcsud(m,k,n))))],
00485   output_fcs_v(
00486     sconcat("Green-Tao problem (diagonal form),
00487 c created by the OKlibrary at ", timedate(),": 
00488 c ", m, " parts with arithmetic progressions of sizes ", k, "
00489 c and ", n, " prime numbers. Symmetry breaking by putting prime 3 into part 1.
00490 c Variables and associated prime numbers and \"colours\":"),
00491     FF[1],
00492     filename,
00493     FF[2]))$
00494 output_greentaod_sb_stdname(m,k,n) := output_greentaod_sb(m,k,n,
00495   sconcat("GreenTao_sb_",m,"-",k,"_",n,".cnf"))$
00496 
00497