OKlibrary  0.2.1.6
MinVarDegrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.4.2011 (Guangzhou) */
00002 /* Copyright 2011, 2012, 2013 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 
00025 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/PrimeNumbers.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00029 
00030 
00031 /* **************************
00032    * Number of full clauses *
00033    **************************
00034 */
00035 
00036 /* The lower bound on the maximal number of full clauses for deficiency k,
00037    using inverse 2-subsumption-resolution with a new variable:
00038 */
00039 fullclauses_dmu_lb1[k] := if k=1 then 2 else
00040   for i : 1 thru k-1 do
00041     if k-i+1<=fullclauses_dmu_lb1[i] then return(2 * (k-i+1))$
00042 
00043 /* For k >= 2 the index i in the recusion of fullclauses_dmu_lb1: */
00044 index_Sma_S2_rec(k) := for i : 1 do
00045   if k-i+1<=fullclauses_dmu_lb1[i] then return(i)$
00046 
00047 /* Analysing the recursion of fullclauses_dmu_lb1[k], we obtain the following
00048    algorithm for computing the list of the first k values (starting with k=1):
00049 */
00050 Sma_S2_replica(k) := block(
00051  [L, i:2,j,z:1, current:2,fin:0, rem],
00052   L : okl_make_array(fixnum,max(k,1)),
00053   L[z]:fin, z:z+1,
00054   while z <= k do (
00055     rem:k-z+1, thru min(rem, 2) do (fin:fin+2, L[z]:fin, z:z+1),
00056     if z <= k then (
00057       j:i+1,
00058       while j <= k and L[j] = current do j : j+1,
00059       rem:k-z+1, thru min(rem, j-i) do (L[z]:fin, z:z+1),
00060       i:j,
00061       current:current+2
00062     )
00063   ),
00064   return(take_l(k,ary2l(L))))$
00065 
00066 /* This function, for fixed d >= 2, seems to be equal to Sma_bydef(k,d) if
00067    and only if d is a prime number:
00068 */
00069 fullclauses_dmu_lb1_gen[k,d] := if k=1 then d else
00070   for i : 1 thru k-1 do
00071     if k-i+1<=fullclauses_dmu_lb1_gen[i,d] then return(d * (k-i+1))$
00072 /* And it seems always equal to the values produced by Sma_list(n,d). */
00073 
00074 /* The Smarandache Primitive Numbers for a natural number n >= 0,
00075    defined as the minimal natural number s >= 0 such that 2^n divides s!;
00076    this is http://oeis.org/A007843, except of that we start with 0, not with
00077    the faulty 1.
00078 */
00079 Sma_S2_bydef(n) := block([e:2^n, p:1, k:0],
00080  while mod(p,e)#0 do (k:k+1, p:p*k), k)$
00081 
00082 /* A different computation, yielding the list of the first n numbers (starting
00083    with index 0): */
00084 Sma_S2_list(n) := if n=0 then [] else block([res:[0], e : 2],
00085  n : n-1,
00086  while n>0 do block([count : expfact(e,2), t],
00087   t : min(n,count),
00088   n : n-t,
00089   res : append(res, create_list(e,i,1,t)),
00090   e : e+2
00091  ),
00092  res)$
00093 
00094 /* The general function S_d (Sma_S2_bydef is for d=2), for d >= 1 and n >= 0:
00095 */
00096 Sma_bydef(n,d) := block([e:d^n, p:1, k:0],
00097  while mod(p,e)#0 do (k:k+1, p:p*k), k)$
00098 
00099 /* A different computation for Sma_bydef(1,d): */
00100 Sma_start(d) := if primep(d) then d
00101 else lmax(create_list(Sma_bydef(p[2],p[1]), p,ifactors(d)))$
00102 
00103 /* A more efficient implementation, yielding the list of the first n numbers
00104    (starting with index 0), for arbitrary d >= 2: */
00105 Sma_list(n,d) := if n=0 then [] else block([res:[0], e : d],
00106  n : n-1,
00107  while n>0 do block([count : expfact(e,d), t],
00108   t : min(n,count),
00109   n : n-t,
00110   res : append(res, create_list(e,i,1,t)),
00111   e : e+d
00112  ),
00113  res)$
00114 
00115 /* Analysing the recursion of fullclauses_dmu_lb1_gen[k], we obtain the
00116    following algorithm for computing the list of the first k values (starting
00117    with k=1):
00118 */
00119 Sma_replica(k,d) := block(
00120  [L, i:2,j,z:1, current:d,fin:0, rem],
00121   L : okl_make_array(fixnum,max(k,1)),
00122   L[z]:fin, z:z+1,
00123   while z <= k do (
00124     rem:k-z+1, thru min(rem, d) do (fin:fin+d, L[z]:fin, z:z+1),
00125     if z <= k then (
00126       j:i+1,
00127       while j <= k and L[j] = current do j : j+1,
00128       rem:k-z+1, thru min(rem, j-i) do (L[z]:fin, z:z+1),
00129       i:j,
00130       current:current+d
00131     )
00132   ),
00133   return(take_l(k,ary2l(L))))$
00134 
00135 
00136 
00137 /* We have fullclauses_dmu_lb1[k] = Sma_S2_bydef(k). */
00138 
00139 /* Upper bound on the number of full clauses for deficiency k, using the
00140    known best upper bound on the min-var-degree:
00141 */
00142 fullclauses_dmu_ub1(k) := if k=1 then 2 else
00143  block([mvd : seconde(minvardegree_dmu(k)), ub],
00144   if oddp(mvd) then ub : mvd-1 else ub : mvd,
00145   if ub=mvd and 2*seconde(fullclauses_dmu[k-mvd/2+1]) < mvd then ub : mvd-1,
00146   ub)$
00147 
00148 /* Best lower and upper bounds: */
00149 fullclauses_dmu_lb(k) := fullclauses_dmu_lb1[k]$
00150 fullclauses_dmu_ub(k) := fullclauses_dmu_ub1(k)$
00151 
00152 /* Lower and upper bounds combined: */
00153 fullclauses_dmu(k) :=
00154  block([lb : fullclauses_dmu_lb(k), ub : fullclauses_dmu_ub(k)],
00155   if lb=ub then lb else [lb,ub])$
00156 
00157 
00158 /* ***************************
00159    * Maximal min-var-degrees *
00160    ***************************
00161 */
00162 
00163 /* For k in NN the smallest integer o with k <= 2^o-o: */
00164 order_deficiency(k) := if k=1 then 0 elseif k=2 then 2 else
00165  block([o : cld(k)], if k <= 2^o-o then o else o+1)$
00166 
00167 /* For deficiency k in NN the maximum minimal-variable-degree in minimally
00168    unsatisfiable clause-sets of deficiency k; if the precise value is not
00169    known, then an interval [lower-bound,upper-bound] is given.
00170    The "hitting-catalogue" is accessed via max_min_var_deg_uhit_def(k).
00171 */
00172 minvardegree_dmu(k) := block(
00173  [o : order_deficiency(k),
00174   l : nonmersenne_level(k), disto,distl],
00175   disto : (2^o-o) - k,
00176   distl : k - (2^l-l),
00177   if k=1 then 2
00178   elseif disto=0 then 2^o
00179   elseif disto<=o then 2^o-1-disto
00180   elseif distl=1 then 2^l
00181   elseif k=7 then 10 /* according to hitting-catalogue */
00182   elseif k=14 then 17 /* according to hitting-catalogue */
00183   elseif k=18 then 22 /* according to hitting-catalogue */
00184   elseif k=19 then 23 /* according to hitting-catalogue */
00185   elseif k=21 then 25 /* according to hitting-catalogue */
00186   else block(
00187    [lb : max(firste(minvardegree_dmu(k-1)), fullclauses_dmu_lb(k)),
00188     ub : nonmersenne_inf_law(k)],
00189     if lb=ub then lb else [lb,ub]))$
00190 
00191 
00192 /* **************************************
00193    * (Generalised) non-Mersenne numbers *
00194    **************************************
00195 */
00196 
00197 /* An upper bound on the maximal min-var-degree of a minimally unsatisfiable
00198    clause-set of deficiency k, according to [OK, XSZ, SAT 2011]. */
00199 /* This bound is sharp at least for 
00200  - k = 2^n-n (realised by full_fcs(n))
00201  - k=2 (realised by musatd2_fcs(n))
00202  - k=3 (realised by minvdegdef3(n))
00203  - k=4 (realised by minvdegdef4(n)). */
00204 /* I.e., min_unsat_bydef(F) and is(deficiency_cs(F) <= k) -> 
00205          min_variable_degree_cs(F) <= nonmersenne[k]. */
00206 /* First the recursive computation: */
00207 nonmersenne_rec[k] := 
00208  if k = 1 then 2 else
00209  lmax(create_list(min(2*i,nonmersenne_rec[k-i+1]+i),i,2,k))$
00210 /* This is sequence A062289 (http://www.research.att.com/~njas/sequences/),
00211    and accordingly we have 
00212    nonmersenne_rec[k] = nonmersenne_law(k). */
00213 nonmersenne_law(k) := k + fld(k+1 + fld(k+1))$
00214 /* A natural lower bound: */
00215 nonmersenne_lb(k) := k + fld(k+1)$
00216 /* A natural upper bound: */
00217 nonmersenne_ub(k) := k + 1 + fld(k)$
00218 
00219 /* The fastest computation: */
00220 nonmersenne(k) := nonmersenne_law(k)$
00221 
00222 /* Compare Lisp/ConflictCombinatorics/HittingClauseSets.mac
00223    for the treatmeant of hitting clause-sets.
00224 */
00225 
00226 /* Generalising the non-Mersenne numbers to "arity" d (for the ordinary numbers
00227    we have d=2), where now the values d^m-1, ..., d^m - (d-1) are jumped:
00228 */
00229 nonmersenne_dary_jump0(k,d) :=
00230  block([e : d^1, y : 0], while k > 0 do (
00231   k : k-1, y : y + 1,
00232   if y > e - d then (y : y+(d-1), e : e*d)
00233  ),
00234  y)$
00235 /* Remark: This function however does not seem to be relevant here. The
00236    following function nonmersenne_dary_rec[k,d] seems to be the right
00237    generalisation.
00238 */
00239 
00240 /* Generalising the recursion (k >= 1, d >= 2): */
00241 nonmersenne_dary_rec[k,d] :=
00242  if k = 1 then d else
00243  lmax(create_list(
00244    min(floor((1 + 1/(d-1))*i),nonmersenne_dary_rec[k-i+(d-1),d]+i),
00245    i,d,k+d-2))$
00246 nonmersenne_dary_jumpedpattern(L,d) :=
00247  not emptyp(L) and every_s(lambda([x], is(x=d-1)), rest(L))$
00248 nonmersenne_dary_jump_bydef(k,d) := block([res : 0],
00249  unless k=0 do (
00250    res : res+1,
00251    while nonmersenne_dary_jumpedpattern(int2polyadic(res,d),d) do
00252      res : res + 1,
00253    k : k-1
00254  ),
00255  res)$
00256 
00257 
00258 /* Analysis of the recurrence behaviour:
00259    Return [] iff k=1, else return the list of tuples T_i for 2 <= i <= k where
00260    min(2i,nonmersenne_rec[k-i+1]+i) = nonmersenne_rec[k],
00261    where the last component of T_i is
00262     - "a" if the first component is strictly less than the second,
00263     - "ab" if they are equal,
00264     - and "b" otherwise,
00265    where in the first case T_i has a leading i, and otherwise leading i, k-i+1.
00266 */
00267 analyse_nonmersenne_rec(k) := 
00268  if k=1 then []
00269  else block([res : [], maxv : minf],
00270   for i : 2 thru k do block(
00271    [a : 2 * i, b : nonmersenne_rec[k-i+1]+i, minv],
00272     minv : min(a,b),
00273     if minv >= maxv then (
00274       if minv > maxv then(maxv : minv,  res : []),
00275       if a < b then res : cons([i,"a"], res)
00276       elseif a = b then res : cons([i,k-i+1,"ab"], res)
00277       else res : cons([i,k-i+1,"b"], res)
00278     )
00279   ),
00280   return(reverse(res)))$
00281 
00282 /* Computation of the "primary recursion index", the smallest i in {2,...,k}
00283    with i >= nonmer(k-i+1) + i.
00284    Prerequisite: k >= 2.
00285 */
00286 index_nonmersenne_rec(k) :=
00287   block([i : 2],
00288     while i < nonmersenne_rec[k-i+1] do i : i + 1,
00289   return(i))$
00290 /* The alternative recursive formula for nonmersenne_rec[k]: */
00291 nonmersenne_rec2(k) := if k=1 then 2 else block(
00292  [i : index_nonmersenne_rec(k)],
00293   nonmersenne_rec[k-i+1]+i)$
00294 
00295 /* Analysis of the various steps, for k >= 2:
00296   [Delta nonmer(k),
00297    Delta (k -> nonmer(k-i(k)+1))(k),
00298    i(k+1)-i(k),
00299    i(k) - nonmer(k-i(k)+1)].
00300 */
00301 step_nonmersenne_rec(k) := block(
00302  [i : index_nonmersenne_rec(k),
00303   ip : index_nonmersenne_rec(k+1)],
00304   [
00305    nonmersenne_rec[k+1] - nonmersenne_rec[k],
00306    nonmersenne_rec[(k+1)-ip+1] - nonmersenne_rec[k-i+1],
00307    ip-i,
00308    i - nonmersenne_rec[k-i+1]
00309   ])$
00310 
00311 
00312 /* An alternative recursion for nonmersenne(k) for k >= 2:
00313    The maximal s in {4,...,2k} such that there exists (e_0,e_1) in {2,...,k}^2
00314    with e_0 + e_1 >= s and nonmersenne(k-e_i+1)+e_i >= s for both i in {0,1}.
00315 */
00316 nonmersenne_rec3[k] := if k=1 then 2 else last(
00317  sublist(create_list(i,i,4,2*k),
00318          lambda([s],
00319                 some_s(lambda([i], is(nonmersenne_rec3[k-i+1]+i >= s
00320                          and nonmersenne_rec3[k-(s-i)+1]+(s-i) >= s)),
00321                        create_list(i,i,max(s-k,2),min(s-2,k)))
00322    )))$
00323 
00324 
00325 /* For deficiency k and considered minimal variable degree m of a saturated
00326    non-singular minimally unsatisfiable F of deficiency k, the possible
00327    pairs [e0,e1] with e0+e1=m and e0 <= e1 of degrees of a variable v of F
00328    realising degree m, using the upper bound nonmersenne(k') on the degree
00329    of minimally unsatisfiable clause-sets of deficiency k', obtained by
00330    splitting on v (setting v first to 0, than to 1, accordingly e0 is the
00331    literal-degree of -v).
00332    Additionally to [e0,e1] the quadruple [k0,d0,k1,d1] is computed, with k0,k1
00333    the deficiencies after splitting, and d0, d1 the resulting upper bounds
00334    on the degree of v in F.
00335    The result is a list of pairs [[e0,e1], [k0,d0,k1,d1]], sorted by ascending
00336    e0.
00337    Prerequisites: k >= 2, 4 <= m.
00338 */
00339 possible_degree_pairs_nm(k,m) := block([res : []],
00340   for e0 : 2 thru min(k,m/2) do block(
00341    [e1 : m - e0, k0,k1, d0,d1],
00342     k0 : k-e0+1, k1 : k-e1+1,
00343     d0 : nonmersenne_rec[k0]+e0, d1 : nonmersenne_rec[k1]+e1,
00344     if d0 >= m and d1 >= m then res : cons([[e0,e1],[k0,d0,k1,d1]],res)),
00345   return(reverse(res)))$
00346 
00347 /* The general version of possible_degree_pairs_nm, now using function
00348    nmf_ instead of nonmersenne:
00349 */
00350 /* TODO: precisely specify the assumptions on the arguments. */
00351 possible_degree_pairs_gen(k,m,nmf_) := block([res : []],
00352   for e0 : max(2,m-k) thru min(k,m/2) do block(
00353    [e1 : m - e0, k0,k1, d0,d1],
00354     k0 : k-e0+1, k1 : k-e1+1,
00355     d0 : nmf_(k0)+e0, d1 : nmf_(k1)+e1,
00356     if d0 >= m and d1 >= m then res : cons([[e0,e1],[k0,d0,k1,d1]],res)),
00357   return(reverse(res)))$
00358 
00359 
00360 /* The "non-Mersenne operator", which performs the recursion on possible
00361    degree-pairs, with start-values (possibly to be improved) given by L.
00362    Prerequisites: L a non-empty list of natural numbers, L[1] = 2,
00363    increasing (not strict), and k >= 1.
00364 */
00365 nonmersenne_op[k,L] := if k=1 then 2 else block(
00366  [rec_ : buildq([L], lambda([x], nonmersenne_op[x,L])), m:4],
00367   while m <= 2*k and not emptyp(possible_degree_pairs_gen(k,m,rec_)) do
00368    m : m+1,
00369   if k <= length(L) then min(L[k],m-1) else m-1)$
00370 
00371 /* The generalised non-Mersenne numbers (according to [Kullmann, Zhao, 2011]),
00372    using the additional parameter r: These numbers are one less than
00373    non-Mersenne numbers for k = 2^(2+r')-2, 1 <= r' <= r, which triggers
00374    further reductions by one according to the recursions in
00375    possible_degree_pairs_nm.
00376    Prerequisites: k >= 1, r >= 0.
00377 */
00378 /* TODO: specify how this is a special case of nonmersenne_op. */
00379 nonmersenne_gen_rec[k,r] :=
00380  if r=0 then nonmersenne_rec[k]
00381  else block([nM : nonmersenne_gen_rec[k,r-1]],
00382    if k < 2^(2+r)-2 then nM
00383    elseif k=2^(2+r)-2 then nM-1
00384    else min(nM,lmax(create_list(min(nonmersenne_gen_rec[k-e+1,r]+e,
00385                                     nonmersenne_gen_rec[k-(nM-e)+1,r]+(nM-e)),
00386                                 e,nM-k,k))))$
00387 
00388 /* The "epoche" of k is the largest r which can have an influence on
00389    nonmersenne_gen_rec[k,r]:
00390 */
00391 epoche_nonmersenne_gen(k) := fld(k+2)-2$
00392 
00393 nonmersenne_inf_rec(k) := if k=1 then 2 else
00394  nonmersenne_gen_rec[k,epoche_nonmersenne_gen(k)]$
00395 
00396 /* The largest natural number l >= 0 such that 2^l-l <= k.
00397    Prerequisite k >= 1.
00398 */
00399 nonmersenne_level(k) := if k=1 then 1 elseif k=2 then 2 else
00400  block([l : cld(k)], if k >= 2^l-l then l else l-1)$
00401 
00402 nonmersenne_law2(k) := k + nonmersenne_level(k)$
00403 
00404 nonmersenne_inf_law(k) := block(
00405  [nM : nonmersenne_law(k),
00406   l : nonmersenne_level(k),
00407   e : epoche_nonmersenne_gen(k)],
00408   if k <= 2^l-l then nM
00409   elseif k <= 2^l-l+e then nM-1
00410   else nM)$
00411 
00412 
00413 possible_degree_pairs_nminf(k,m) :=
00414  possible_degree_pairs_gen(k,m,nonmersenne_inf_law)$
00415 
00416 possible_degree_pairs_genextr(k,nmf_) :=
00417  possible_degree_pairs_gen(k,nmf_(k),nmf_)$
00418 
00419 possible_degree_pairs_nminfextr(k) :=
00420  possible_degree_pairs_nminf(k,nonmersenne_inf_law(k))$
00421 
00422 /* A "sharpened non-Mersenne function" is a map f: NN -> NN with
00423    - f(1) = 2
00424    - f(2) = 4
00425    - f(k) in {nM(k),nM(k)-1} for all k in NN.
00426 
00427    f is furthermore called "consistent" if
00428      possible_degree_pairs_genextr(k,f) # {} for all k in NN.
00429 */
00430 sharpenednm_p(nmf_,K) := if nmf_(1)#2 or nmf_(2)#4 then false else
00431  is(done = block([nm],
00432    for k : 3 thru K do (
00433      nm : nonmersenne_law(k),
00434      if not elementp(nmf_(k), {nm,nm-1}) then return(false)
00435    )))$
00436 
00437 consistentsnm_p(nmf_,K) := sharpenednm_p(nmf_,K) and
00438  is (done = block([nm],
00439  for k : 3 thru K do
00440    if emptyp(possible_degree_pairs_genextr(k,nmf_)) then return(false)
00441  ))$
00442 
00443