OKlibrary  0.2.1.6
Certificates.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.11.2010 (Swansea) */
00002 /* Copyright 2010, 2011, 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/VanderWaerden.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00026 
00027 
00028 /* *****************
00029    * Basic notions *
00030    *****************
00031 */
00032 
00033 /*
00034    A "vdw-certificate" P for a pair [L,n], where L is a parameter tuple of
00035    length m and n is a natural number, corresponds to a solution of
00036    vanderwaerden_nbfclud(L,n), that is, certifies that vanderwaerden(L) > n.
00037 
00038    P is a block partition of {1,...,n} into m blocks, that is, a list of
00039    m disjoint subsets of {1,...,n} whose union is the whole set.
00040 */
00041 
00042 /* Tests whether P is a vdW-certificate for parameter tuple L and n vertices.
00043    It is assumed that L is an extended vdW-parameter-tuple, n a natural
00044    number, and P a list of sets. A valid certificate can have empty parts, but
00045    overlaps between the parts and additional elements are not allowed.
00046 */
00047 certificate_vdw_p(L,n,P) :=
00048   is(length(L) = length(P)) and blockpartitionp(P,setn(n)) and
00049     every(lambda([k,b], not has_arithprog(b,k)), L, P)$
00050 /* See "The notion of a certificate" in 
00051    ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/plans/Certificates.hpp.
00052 */
00053 
00054 /* For a list of subsets of {1,...,n} check whether P is "palindromic",
00055    that is, whether for every element (subset) p of P it is true that
00056    v is in p iff n+1-v is in p:
00057 */
00058 palindromic_subsets_p(n,P) := if n <= 1 then true else
00059  block([palin : true],
00060   for p in P while palin do
00061     for x in p while palin do
00062       if not elementp(n+1-x,p) then palin : false,
00063   return(palin))$
00064 
00065 /* Check whether P is a palindromic vdW-certificate for L and n: */
00066 certificate_pdvdw_p(L,n,P) := palindromic_subsets_p(n,P) and
00067  certificate_vdw_p(L,n,P)$
00068 
00069 
00070 /* *******************
00071    * Transformations *
00072    *******************
00073 */
00074 
00075 /* Creates a certificate from a list of elements constituting one part
00076    of a binary partitioning:
00077 */
00078 create_certificate2_vdw(S,n) := block([s : setify(S)],
00079   [s, setdifference(setn(n),s)])$
00080 
00081 
00082 /* Certificates as partitions versus certificates as lists */
00083 
00084 /* The "list-presentation" of a certificate represents the partition
00085    as a list of pairs [i,p], where 0 <= i < m represents the block,
00086    and p >= 1 says how many consecutive elements are there;
00087    The whole list-representation has to be read from left to right.
00088    Accordingly we have "list-certificates".
00089 */
00090 
00091 /* First the "uncompressed list", here denoted as "sequence":
00092    Translates a vdw-certificate P (as a block-partitioning of {1,...,n})
00093    into a sequence of i elements of 0,...,length(P)-1 representing
00094    the colour:
00095 */
00096 certificatevdw2seq(P) := block([N : lunion(P)],
00097  if emptyp(N) then return([]),
00098  create_list(
00099   block([j:0], for b in P do if elementp(i,b) then return(j) else j:j+1),
00100   i,1,lmax(N)))$
00101 
00102 /* Now the "compressed list":
00103    Translates a vdw-certificate P (as a block-partitioning of {1,...,n})
00104    into a sequence "i^k", where i = 0,...,length(P)-1 is the colour,
00105    and k is the occurrence numbers, representing "i^k" as [i,k] for the
00106    list-form, while using "i" for "i^1" in the string-form:
00107 */
00108 certificatevdw2list(P) := block([seq : certificatevdw2seq(P)],
00109  if emptyp(seq) then return(seq),
00110  block([current:first(seq), compressed:[], count:1],
00111    for x in rest(seq) do
00112      if x=current then count:count+1
00113      else (compressed:cons([current,count],compressed), count:1, current:x),
00114    if count>0 then compressed:cons([current,count],compressed),
00115    return(reverse(compressed))))$
00116 certificatevdw2string(P) := block([distribute_over:false, x,y], 
00117   ssubst("1","y",ssubst("0","x", apply(sconcat,
00118     map(lambda([p], block([a,b], [a,b]:p, if a=0 then a:x elseif a=1 then a:y, 
00119                           if b=1 then a else a^{b})),
00120         certificatevdw2list(P))))))$
00121 
00122 /* The reverse direction, translates a (compressed) list-representation of a
00123    partition into a partition:
00124 */
00125 list2certificatevdw(L) := if emptyp(L) then [] else
00126  block([m : lmax(map(first,L))+1, i : 1, res],
00127   res : create_list({},i,1,m),
00128   for p in L do (
00129     res[first(p)+1] : union(res[first(p)+1], setmn(i, i+second(p)-1)),
00130     i : i + second(p)
00131   ),
00132   res)$
00133 /* And translating an "uncompressed list-representation" into a partition: */
00134 seq2certificatevdw(L) := if emptyp(L) then [] else
00135  block([m : lmax(L)+1, i : 1, res],
00136   res : create_list({},i,1,m),
00137   for p in L do (
00138     res[p+1] : adjoin(i,res[p+1]),
00139     i : i + 1
00140   ),
00141   res)$
00142 
00143 
00144 
00145 /* Palindromic certificates */
00146 
00147 /* The compression of a palindromic partition of {1,...,n}, restricting to
00148    the elements <= (n+1)/2:
00149 */
00150 compress_palindromic_subsets(P) := 
00151 block([n : lmax(map(lmax,P)), H],
00152   if n = minf then return(P),
00153   H : setn(ceiling(n/2)),
00154   map(lambda([p], intersection(p,H)), P))$
00155 
00156 /* Unfolding a compressed palindromic partition (creating an ordinary
00157    (palindromic) vdW-certificate):
00158 */
00159 uncompresss_palindromic_subsets(n,P) := block([m : lambda([v], {v,n+1-v})],
00160   map(lambda([p], lunion(map(m,listify(p)))), P))$
00161 
00162 /* For a "half compressed palindromic certificate" S, that is, a sublist of
00163    {1,...,m} with m = ceiling(n/2), which specifies the elements of the
00164    first part of the partition, create a (full, palindromic) certificate:
00165 */
00166 create_certificate2c_pdvdw(S,n) := block([m : ceiling(n/2), P],
00167   P : create_certificate2_vdw(S,m),
00168   uncompresss_palindromic_subsets(n,P))$
00169 
00170 
00171 /* Output */
00172 
00173 /* Output a certificate with two blocks in simple partial-assignment-format,
00174    i.e., first the elements of the first block, then negated the element
00175    of the second block, space-separated:
00176 */
00177 output_certificate2_vdw(C,filename) := with_stdout(filename,
00178  print_nlb(apply(sconcat, map(dimacs_c_string,[C[1],comp_sl(C[2])]))))$
00179 
00180 
00181 /* **************************
00182    * Analysing certificates *
00183    **************************
00184 */
00185 
00186 /* For a block partition P of {1,...,n} with m blocks compute for each block:
00187  - the size
00188  - the count of (maximal) intervals
00189  - the count of (maxima) non-trivial (more than one element) intervals
00190  - the number of extremal plateaus for the list representation
00191  - the maximal number of equal consecutive elements in the list representation.
00192    Returned is a 5-tuple of tuples of natural numbers (of size m).
00193 */
00194 analyse_certificate(P) := block(
00195  [m : length(P), L : certificatevdw2list(P), N, ci, cnti, ce, mi],
00196   N : map(length, P),
00197   ci : create_list(
00198         countpred_l(lambda([p], is(first(p)=i)), L),
00199         i,0,m-1),
00200   cnti : create_list(
00201           countpred_l(lambda([p], is(first(p)=i and second(p)#1)), L),
00202           i,0,m-1),
00203   ce : create_list(
00204         count_extremals_l(map(second, sublist(L, lambda([p], is(first(p)=i))))),
00205         i,0,m-1),
00206   mi : create_list(
00207         lmax(size_constintervals_l(map(second, sublist(L, lambda([p], is(first(p)=i)))))),
00208         i,0,m-1),
00209   [N,ci,cnti,ce,mi])$
00210 
00211