OKlibrary  0.2.1.6
Statistics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 4.4.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 
00026 
00027 /* ******************
00028    * Basic measures *
00029    ******************
00030 */
00031 
00032 /* Counting the number of variables: */
00033 
00034 nvar_cs(F) := length(var_cs(F))$
00035 nvar_ocs(F) := nvar_cl(F)$
00036 nvar_cl(F) := length(var_cl(F))$
00037 /* RENAME: nvar_fcs(FF) */
00038 nvar_f(FF) := length(FF[1])$
00039 nvar_fcs(FF) := length(FF[1])$
00040 nvar_fcl(FF) := length(FF[1])$
00041 nvar_ofcs(FF) := length(FF[1])$
00042 
00043 
00044 /* Number of clauses of a formal clause-set: */
00045 /* RENAME: ncl_fcs */
00046 ncl_f(FF) := length(clauses_f(FF))$
00047 ncl_fcs(FF) := length(FF[2])$
00048 ncl_fcl(FF) := length(FF[2])$
00049 /* Number of clauses of a clause-set: */
00050 ncl_cs(F) := length(F)$
00051 ncl_cl(F) := length(F)$
00052 
00053 /* Number of literal occurrences in a clause-set: */
00054 nlitocc_cl(F) := sum_l(map(length,listify(F)))$
00055 nlitocc_cs(F) := nlitocc_cl(F)$
00056 nlitocc_fcl(FF) := nlitocc_cl(FF[2])$
00057 nlitocc_fcs(FF) := nlitocc_cl(FF[2])$
00058 
00059 /* The list of pairs
00060    [occurring clause-lengths, number of clauses of this length],
00061    sorted by ascending clause-length.
00062 */
00063 ncl_list_fcl(FF) := block([n : nvar_fcl(FF), counts, res : []],
00064   counts : make_array(fixnum, n+1),
00065   for C in FF[2] do block([l : length(C)],
00066     counts[l] : counts[l] + 1),
00067   for i : 0 thru n do
00068     if counts[i] # 0 then res : cons([i, counts[i]], res),
00069   return(reverse(res)))$
00070 ncl_list_fcs(FF) := ncl_list_fcl(FF)$
00071 ncl_list_cl(F) := block(
00072  [n : nvar_cl(F), counts, res : []],
00073   counts : make_array(fixnum, n+1),
00074   for C in F do block([l : length(C)],
00075     counts[l] : counts[l] + 1),
00076   for i : 0 thru n do
00077     if counts[i] # 0 then res : cons([i, counts[i]], res),
00078   return(reverse(res)))$
00079 ncl_list_cs(F) := ncl_list_cl(F)$
00080 
00081 /* Maximal clause-length of a clause-set: */
00082 max_rank_cs(F) := block([m : -1],
00083   for C in F do if length(C) > m then m : length(C),
00084   return(m))$
00085 max_rank_fcs(FF) := max_rank_cs(FF[2])$
00086 /* Minimal clause-length of a clause-set: */
00087 min_rank_cs(F) := block([m : inf],
00088   for C in F do if length(C) < m then m : length(C),
00089   return(m))$
00090 min_rank_fcs(FF) := min_rank_cs(FF[2])$
00091 /* Tests whether a clause-set F is uniform: */
00092 uniformcsp(F) := is(max_rank_cs(F) <= min_rank_cs(F))$
00093 
00094 
00095 /* *******************
00096    * Literal degrees *
00097    *******************
00098 */
00099 
00100 /* The degree of a literal in a clause-set: */
00101 literal_degree_cs(F,l) := length(scls_l(F,l))$
00102 
00103 /* The literal-degrees of a clause-set, as hash-map, considering
00104    only occurring literals: */
00105 literal_degrees_cs(F) := block([h : sm2hm({})],
00106  for C in F do for x in C do enter_new_occurrence(h,x),
00107  return(h))$
00108 literal_degrees_cl(F) := block([h : sm2hm({})],
00109  for C in F do for x in C do enter_new_occurrence(h,x),
00110  return(h))$
00111 /* The literal-degrees of a formal clause-set, as hash-map, considering
00112    all literals (w.r.t. the variables given): */
00113 /* RENAME: literal_degrees_fcs */
00114 all_literal_degrees_fcs(FF) := block(
00115  [h : literal_degrees_cs(FF[2]), L : literals_v(FF[1])],
00116   for x in L do if ev_hm(h,x) = false then set_hm(h,x,0),
00117   return(h))$
00118 literal_degrees_fcs(FF) := all_literal_degrees_fcs(FF)$
00119 
00120 /* Returns the pairs of literal and literal degree of a clause-set F in
00121    descending order of the literal degree using the given order
00122    on literals  for equal counts. */
00123 ordered_literal_degrees_cs(F) :=
00124    sort(listify(hm2sm(literal_degrees_cs(F))),
00125         lambda([P1,P2], is(second(P1) > second(P2))))$
00126 ordered_literal_degrees_fcs(F) :=
00127    sort(listify(hm2sm(literal_degrees_fcs(F))),
00128         lambda([P1,P2], is(second(P1) > second(P2))))$
00129 
00130 /* Minimal literal-degree of a clause-set. */
00131 min_literal_degree_cs(F) :=
00132   lmin(map(second,hm2sm(literal_degrees_cs(F))))$
00133 min_literal_degree_fcs(FF) := min_literal_degree_cs(FF[2])$
00134 /* maximal literal-degree of a clause-set */
00135 max_literal_degree_cs(F) :=
00136   lmax(map(second,hm2sm(literal_degrees_cs(F))))$
00137 max_literal_degree_fcs(FF) := max_literal_degree_cs(FF[2])$
00138 /* Also returns a literal of minimal degree (if there is a literal);
00139    in case of ties, the return value is implementation-defined. */
00140 min_literal_degree_l_cs(F) := if F = {} or F = {{}} then [inf,0] else block(
00141   [D : hm2sm(literal_degrees_cs(F)),
00142    optl : 0, mind : inf],
00143   for m in D do block([d : m[2]],
00144     if d < mind then (mind : d, optl : m[1])),
00145   return([mind, optl]))$
00146 /* Also returns a literal of maximal degree (if there is a literal);
00147    in case of ties, the return value is implementation-defined. */
00148 max_literal_degree_l_cs(F) := if F = {} or F = {{}} then [minf,0] else block(
00149   [D : hm2sm(literal_degrees_cs(F)),
00150    optl : 0, maxd : minf],
00151   for m in D do block([d : m[2]],
00152     if d > maxd then (maxd : d, optl : m[1])),
00153   return([maxd, optl]))$
00154 max_literal_degree_l_cl(F) :=
00155  if emptyp(F) or F = [{}] then [minf,0] else block(
00156   [D : hm2sm(literal_degrees_cl(F)),
00157    optl : 0, maxd : minf],
00158   for m in D do block([d : m[2]],
00159     if d > maxd then (maxd : d, optl : m[1])),
00160   return([maxd, optl]))$
00161 
00162 /* Tests whether a clause-set is literal-regular (all literals have the same
00163    degree): */
00164 literalregularcsp(F) := is(min_literal_degree_cs(F) >= max_literal_degree_cs(F))$
00165 /* The average literal degree of a formal clause-set: */
00166 mean_literal_degree_fcs(FF) := nlitocc_fcs(FF) / (2 * nvar_f(FF))$
00167 /* Literal frequencies in various forms: */
00168 min_literal_frequency_cs(F) := min_literal_degree_cs(F) / ncl_cs(F)$
00169 max_literal_frequency_cs(F) := max_literal_degree_cs(F) / ncl_cs(F)$
00170 mean_literal_frequency_cs(FF) := mean_literal_degree_cs(FF) / ncl_f(FF)$
00171 
00172 /* The list of pairs
00173    [occurring literal-degree, number of literals of this degree],
00174    sorted by ascending literal_degree.
00175 */
00176 literal_degrees_list_fcs(FF) := block(
00177  [litdeg : hm2sm(all_literal_degrees_fcs(FF)), h : sm2hm({})],
00178   for p in litdeg do
00179     enter_new_occurrence(h,p[2]),
00180   get_distribution(h))$
00181 
00182 
00183 /* OK; ???? what is this doing ? What is "tb" ? */
00184 /* Would also need renaming: "_fcs". */
00185 max_literal_degree_tb(FF,l,d,n) := block([max_ld1, max_ld2, max_l1, max_l2],
00186       [max_l1, max_ld1] : max_literal_degree_tb_l_cs(apply_pa_f({l}, FF),d,n),
00187       [max_l2, max_ld2] : max_literal_degree_tb_l_cs(apply_pa_f({-l}, FF),d,n),
00188       [if max_ld1 > max_ld2 then max_l1 else max_l2, max_ld1 + max_ld2])$
00189 /* Returns the pair of literal and literal degree for the literal
00190    with the maximum degree in the given clause set, where look-aheads are made
00191    when a tie occurs for the maximum degree, looking up to d levels deeper
00192    and considering up to n tied literals. */
00193 /* OK: "look-ahead" ??? a definition is needed. */
00194 /* Would also need renaming: "_fcs". */
00195 max_literal_degree_tb_l_cs(FF,d,n) := block(
00196   [old : ordered_literal_degrees_cs(FF[2])],
00197   if emptyp(old) then [0,0]
00198   else if d < 1 then old[1]
00199   else
00200     xreduce(lambda([a,b], if second(a) > second(b) then a else b),
00201       map(lambda([c], max_literal_degree_tb(FF, first(c),d-1,n)),
00202         block([ml : sublist(rest(old),lambda([a],is(second(a)=second(first(old)))))],
00203           take_elements(min(n,length(ml)),ml))),
00204     first(old)))$
00205 
00206 
00207 /* ********************
00208    * Variable degrees *
00209    ********************
00210 */
00211 
00212 /* The degree of a variable in a clause-set: */
00213 variable_degree_cs(F,v) := length(scls_v(F,v))$
00214 
00215 /* The variable-degrees of a clause-set, as hash-map: */
00216 variable_degrees_cs(F) := block([h : sm2hm({})],
00217  for C in F do for v in var_c(C) do enter_new_occurrence(h,v),
00218  return(h))$
00219 
00220 /* The minimal variable-degree of a clause-set: */
00221 min_variable_degree_cs(F) := lmin(map(second,hm2sm(variable_degrees_cs(F))))$
00222 min_variable_degree_fcs(FF) := min_variable_degree_cs(FF[2])$
00223 /* Also returns a variable of minimal degree, i.e., returns a pair
00224    [min-degree, var], chosing the first in the internal order, while returning
00225    [inf,0] in case there is no variable:
00226 */
00227 min_variable_degree_v_cs(F) := if F = {} or F = {{}} then [inf,0] else block(
00228   [D : hm2sm(variable_degrees_cs(F)), optv : 0, mind : inf],
00229   for m in D do block([d : m[2]], if d < mind then (mind : d, optv : m[1])),
00230   return([mind, optv]))$
00231 
00232 /* The maximal min-var-degree of a set (or list) of clause-sets: */
00233 max_min_var_deg_cs(SF) := lmax(map(min_variable_degree_cs,SF))$
00234 max_variable_degree_fcs(FF) := max_variable_degree_cs(FF[2])$
00235 
00236 /* The maximal variable-degree of a clause-set: */
00237 max_variable_degree_cs(F) :=
00238   lmax(map(second,hm2sm(variable_degrees_cs(F))))$
00239 /* Also returns a variable of maximal degree (if there is a variable). */
00240 max_variable_degree_v_cs(F) := if F = {} or F = {{}} then [minf,0] else block(
00241   [D : hm2sm(variable_degrees_cs(F)),
00242    optv : 0, maxd : minf],
00243   for m in D do block([d : m[2]],
00244     if d > maxd then (maxd : d, optv : m[1])),
00245   return([maxd, optv]))$
00246 
00247 /* The minimal max-var-degree of a set (or list) of clause-sets. */
00248 min_max_var_deg_cs(SF) := lmin(map(max_variable_degree_cs,SF))$
00249 
00250 /* Tests whether a clause-set is variable-regular (all variables have the same
00251    degree). */
00252 variableregularcsp(F) := is(min_variable_degree_cs(F) >= max_variable_degree_cs(F))$
00253 
00254 /* The average variable-degree of a formal clause-set: */
00255 mean_variable_degree_cs(FF) := 2 * mean_literal_degree_fcs(FF)$
00256 /* literal frequencies in various forms: */
00257 min_variable_frequency_cs(F) := min_variable_degree_cs(F) / ncl_cs(F)$
00258 max_variable_frequency_cs(F) := max_variable_degree_cs(F) / ncl_cs(F)$
00259 mean_variable_frequency_cs(FF) := mean_variable_degree_fcs(FF) / ncl_f(FF)$
00260 
00261 /* The list of pairs
00262    [occurring variable-degree, number of variables of this degree],
00263    sorted by ascending variable_degree.
00264 */
00265 variable_degrees_list_cs(F) := block(
00266  [vardeg : hm2sm(variable_degrees_cs(F)), h : sm2hm({})],
00267   for p in vardeg do
00268     enter_new_occurrence(h,p[2]),
00269   get_distribution(h))$
00270 
00271 /* The set of full variables of a non-empty clause-set: */
00272 full_variables_cs(F) := lintersection(map(var_c,F))$
00273 /* The set of full variables of a formal clause-set: */
00274 full_variables_fcs(FF) := if emptyp(FF[2]) then FF[1] else
00275  full_variables_cs(FF[2])$
00276 /* Predicate for deciding whether a clause-set contains a full variable: */
00277 full_var_csp(F) := if emptyp(F) then false else
00278   not emptyp(full_variables_cs(F))$
00279 full_var_fcsp(FF) := not emptyp(full_variables_fcs(FF))$
00280 
00281 /* The set of singular or pure variables of a clause-set: */
00282 singularpure_variables_cs(F) :=
00283   setify(map(var_l,
00284       map(first,
00285           sublist(ordered_literal_degrees_fcs(cs2fcs(F)),
00286                   lambda([P], is(P[2]<=1))))))$
00287 /* Now just the singular variables (without pure variables): */
00288 singular_variables_cs(F) := singular_variables_fcs(cs2fcs(F))$
00289 singular_variables_fcs(FF) := block([h : literal_degrees_fcs(FF)],
00290   subset(FF[1],
00291          lambda([v], block([D : {ev_hm(h,v), ev_hm(h,-v)}],
00292                             elementp(1,D) and not elementp(0,D)))))$
00293 /* 1-singular variables: */
00294 onesingular_variables_fcs(FF) := block([h : literal_degrees_fcs(FF)],
00295   subset(FF[1], lambda([v], is(ev_hm(h,v)=1 and ev_hm(h,-v)=1))))$
00296 onesingular_variables_cs(F) := onesingular_variables_fcs(cs2fcs(F))$
00297 /* Non-1-singular variables: */
00298 nononesingular_variables_fcs(FF) := block([h : literal_degrees_fcs(FF)],
00299   subset(FF[1], lambda([v], block([D:{ev_hm(h,v),ev_hm(h,-v)}],
00300     not elementp(0,D) and elementp(1,D) and length(D)>=2))))$
00301 nononesingular_variables_cs(F) := nononesingular_variables_fcs(cs2fcs(F))$
00302 
00303 
00304 /* For a clause-set F, compute the list of variables sorted by ascending
00305    products pos-occurrences*neg-occurrences (for equal products use the
00306    built-in order of variables):
00307 */
00308 sortvar_prodocc_cs(F) := block([V : var_cs(F)],
00309  h : literal_degrees_fcs([V,F]),
00310  map(first,
00311      sort(map(lambda([v], [v,ev_hm(h,v)*ev_hm(h,-v)]), listify(V)),
00312           lambda([p1,p2], is(second(p1) < second(p2))))))$
00313 
00314 
00315 /* **********************
00316    * Numbers of clauses *
00317    **********************
00318 */
00319 
00320 /* The number of full clauses in a formal clause-list: */
00321 nfcl_fcl(FF) := block([n : length(FF[1])],
00322   length(sublist_indices(FF[2], lambda([C], is(length(C)=n)))))$
00323 /* The number of full clauses in a clause-set: */
00324 nfcl_cs(F) := nfcl_fcl(cs2fcl(F))$
00325 
00326 
00327 /* The weighted number of clauses, using weights 2^(-k) for clause-length k.
00328    This is also the expected number of falsified clauses, under a random
00329    assignment (with uniform distribution). And for a hitting clause-set,
00330    it is the probability that a random assignment falsifies the clause.
00331 */
00332 weighted_ncl_2n_cs(F) := block([L : listify(F)],
00333  return(sum(2^(-length(L[i])),i,1,length(L))))$
00334 weighted_ncl_2n_fcs(FF) := weighted_ncl_2n_cs(FF[2])$
00335 
00336 
00337 /* **************************
00338    * Summarising statistics *
00339    **************************
00340 */
00341 
00342 /* Gathers main statistics for a clause-set: */
00343 statistics_cs(F) := block([nl : 0, maxr : -1, minr : inf],
00344  for C in F do block([l : length(C)],
00345   nl : nl + l, if l > maxr then maxr : l, if l < minr then minr : l),
00346  return([nvar_cs(F), ncl_cs(F), nl, maxr, minr]))$
00347 /* We have statistics_cs(F) =
00348   [nvar_cs(F),ncl_cs(F),nlitocc_cs(F),max_rank_cs(F),min_rank_cs(F)]
00349 */
00350 /* Gathers main statistics for a formal clause-set: */
00351 statistics_fcs(FF) := block([nl : 0, maxr : -1, minr : inf],
00352  for C in FF[2] do block([l : length(C)],
00353   nl : nl + l, if l > maxr then maxr : l, if l < minr then minr : l),
00354  return([nvar_fcs(FF), ncl_fcs(FF), nl, maxr, minr]))$
00355 /* We have statistics_fcs(F) =
00356   [nvar_fcs(FF),ncl_fcs(FF),nlitocc_fcs(FF),max_rank_fcs(FF),min_rank_fcs(FF)]
00357 */
00358 
00359 extended_statistics_fcs(FF) := block(
00360  [nl : 0, minr : inf, maxr : -1, n : nvar_cs(FF[2]),
00361   cl_count, cl_list : [],
00362   v_count : sm2hm({}), l_count : sm2hm({})],
00363   cl_count : make_array(fixnum, n+1),
00364   for C in FF[2] do block([l : length(C)],
00365     nl : nl + l,
00366     if l > maxr then maxr : l, if l < minr then minr : l,
00367     cl_count[l] : cl_count[l] + 1,
00368     for x in C do (
00369       enter_new_occurrence(v_count, var_l(x)),
00370       enter_new_occurrence(l_count, x)
00371   )),
00372   for i : 0 thru n do
00373     if cl_count[i] # 0 then cl_list : cons([i, cl_count[i]], cl_list),
00374   return([
00375     length(FF[1]),length(FF[2]),nl,minr,maxr,reverse(cl_list),
00376     lmin(map(second,hm2sm(l_count))),
00377     lmax(map(second,hm2sm(l_count))),
00378     lmin(map(second,hm2sm(v_count))),
00379     lmax(map(second,hm2sm(v_count)))
00380   ]))$
00381 /* We have extended_statistics_fcs(FF) =
00382   [nvar_fcs(FF),ncl_fcs(FF),nlitocc_fcs(FF),min_rank_fcs(FF),max_rank_fcs(FF),
00383    ncl_list_fcs(FF),min_literal_degree_fcs(FF),max_literal_degree_fcs(FF),
00384    min_variable_degree_fcs(FF),max_variable_degree_fcs(FF)]
00385 */
00386