OKlibrary  0.2.1.6
BasicOperations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.11.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 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 
00022 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 
00026 /* Guaranteed to be included: */
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Strings.mac")$
00031 
00032 
00033 /* **************************
00034    * Variables and literals *
00035    **************************
00036 */
00037 
00038 /*
00039  A "boolean variable" might be any expression x, such that "- x" is defined
00040  and yields a different object, and such that abs(x) = x.
00041 */
00042 
00043 v_p(v) :=
00044  not stringp(v) and
00045  is(is(v>0)=true) and
00046  is(is(-v<0)=true) and
00047  is(is(-v#v)=true) and
00048  is(is(abs(v)=v)=true) and
00049  is(is(abs(-v)=v)=true) and
00050  is(is(--v=v)=true)$
00051 
00052 /*
00053  A "boolean literal" might be a boolean variable "v" or a negated boolean
00054  variable "-v".
00055 */
00056 
00057 l_p(x) :=
00058  is(is(--x=x)=true) and
00059  if is(x>0)=true then
00060    is(is(abs(x)=x)=true) and v_p(x)
00061  elseif is(x<0)=true then
00062    is(is(abs(x)=-x)=true) and v_p(-x)
00063  else false$
00064 
00065 /* The underlying variable of a literal: */
00066 var_l(x) := abs(x)$
00067 
00068 /* The sign of a literal in {-1,+1}: */
00069 sign_l(x) := if sign(x)=pos then 1 else -1$
00070 pos_l(x) := is(sign(x)=pos)$
00071 neg_l(x) := is(sign(x)=neg)$
00072 
00073 /* The set of literals for a set/list V of literals, that is, the closure under
00074    complementation: */
00075 literals_v(V) := block([L : listify(V)], setify(append(L,-L)))$
00076 
00077 /* A generic function for creating variables, e.g.,
00078      gv("h"), gv(1,2,[33])
00079    etc. For equality-checking use (as usual in this context) just "=".
00080 */
00081 kill(gv)$
00082 declare(gv, noun)$
00083 declare(gv, posfun)$
00084 gv_var([x]) := apply(nounify(gv),x)$
00085 
00086 
00087 /* ***********
00088    * Clauses *
00089    ***********
00090 */
00091 
00092 /* Complementation of a set or list of literals: */
00093 comp_sl(L) := map("-", L)$
00094 
00095 /*
00096  A "boolean clause" is a set C of boolean literals such that
00097  C and comp_sl(C) have empty intersection.
00098 */
00099 
00100 c_p(C) := setp(C) and every_s(l_p,C) and emptyp(intersection(C,comp_sl(C)))$
00101 
00102 /* Tests whether two literal sets contain a clashing literal. */
00103 clashp(A,B) := not emptyp(intersection(A,comp_sl(B)))$
00104 
00105 /* The set of variables in a clause: */
00106 var_c(C) := map(var_l, C)$
00107 /* The set of variables in a set of literals: */
00108 var_sl(C) := map(var_l, C)$
00109 
00110 /* The positive resp. negative literals in a clause (can also be applied to
00111    a set of literals): */
00112 pospart_c(C) := subset(C, lambda([x], is(x>0)))$
00113 negpart_c(C) := subset(C, lambda([x], is(x<0)))$
00114 /* Testing whether clause C is positive resp. negative: */
00115 posp_c(C) := emptyp(negpart_c(C))$
00116 negp_c(C) := emptyp(pospart_c(C))$
00117 
00118 /* The set of all full clauses over a set or list V of variables is computed by
00119      full_cs_v(V) (resp. full_cs(n) for V = {1,...,n})
00120    in ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac.
00121 */
00122 
00123 
00124 /* ***************
00125    * Clause-sets *
00126    ***************
00127 */
00128 
00129 /*
00130  A "boolean clause-set" (cs) is a set of boolean clauses.
00131 */
00132 cs_p(F) := setp(F) and every_s(c_p,F)$
00133 /*
00134  An "ordered boolean clause-set" (ocs) is a repetition-free list
00135  of boolean clauses.
00136 */
00137 ocs_p(F) := listnorep_p(F) and every_s(c_p,F)$
00138 /*
00139  A "boolean clause-list" (cl) is a list of boolean clauses.
00140 */
00141 cl_p(F) := listp(F) and every_s(c_p,F)$
00142 
00143 /*
00144  A "formal boolean clause-set" is a pair [V, F], where V is a set of
00145  variables, while F is a clause-set using only variables from V
00146  (that is, with var_cs(F) <= V).
00147 */
00148 fcs_p(FF) := listp(FF) and is(length(FF) = 2) and setp(FF[1]) and
00149   every_s(v_p,FF[1]) and cs_p(FF[2]) and subsetp(var_cs(FF[2]),FF[1])$
00150 /*
00151  An "ordered formal boolean clause-set" is a pair [V,F], where V is
00152  a repetition-free list of variables, while F is an ordered clause-set
00153  using only variables from V.
00154 */
00155 ofcs_p(FF) := listp(FF) and is(length(FF) = 2) and listnorep_p(FF[1])
00156   and every_s(v_p,FF[1]) and ocs_p(FF[2]) and subsetp(var_ocs(FF[2]),setify(FF[1]))$
00157 /*
00158  An "formal boolean clause-list" is a pair [V,F], where V is
00159  a repetition-free list of variables, while F is a clause-list
00160  using only variables from V.
00161 */
00162 fcl_p(FF) := listp(FF) and is(length(FF) = 2) and listnorep_p(FF[1])
00163   and every_s(v_p,FF[1]) and cl_p(FF[2]) and subsetp(var_cl(FF[2]),setify(FF[1]))$
00164 
00165 /* Extracting the set of variables: */
00166 
00167 var_cs(F) := var_sl(lunion(F))$
00168 var_cl(F) := var_sl(lunion(F))$
00169 var_ocs(F) := var_cl(F)$
00170 /* RENAME: var_fcs */
00171 var_cs_f(FF) := FF[1]$
00172 var_fcs(FF) := FF[1]$
00173 var_fcl(FF) := setify(FF[1])$
00174 var_ofcs(FF) := var_fcl(FF)$
00175 
00176 /* Extracting the repetition-free list of variables in a clause-list
00177    (in the order as they occur): */
00178 ovar_cl(F) := block([L : [], V : {}],
00179   for C in F do block([vc : var_c(C), nv],
00180     nv : setdifference(vc, V),
00181     L : append(L,listify(nv)),
00182     V : union(V,nv)
00183   ),
00184   return(L))$
00185 ovar_ocs(F) := ovar_cl(F)$
00186 
00187 /* The set of occurring literals in clause-set F: */
00188 olit_cs(F) := lunion(F)$
00189 /* The "formal" literals in F: */
00190 flit_cs(F) := block([L : olit_cs(F)], union(L,comp_sl(L)))$
00191 
00192 
00193 /* Promotions: */
00194 
00195 /* RENAME: cs2fcs */
00196 cs_to_fcs(F) := [var_cs(F), F]$
00197 cs2fcs(F) := [var_cs(F), F]$
00198 cl2fcl(F) := [listify(var_cl(F)), F]$
00199 ocs2fcl(F) := [listify(var_ocs(F)), F]$
00200 ocs2ofcs(F) := [ovar_cl(F), F]$
00201 /* So a clause-list is promoted to a formal clause-list by taking the
00202    order of variables as given by the given (Maxima) order on the variables,
00203    while for an ordered clause-set we take the order of the
00204    variables as found in the clause-list (this is more expensive).
00205    This is the only case where we have given an order on the clauses,
00206    but not on the variables, and where (different from cl2fcl) the order
00207    is not considered to be "arbitrary".
00208 */
00209 
00210 cs2ocs(F) := listify(F)$
00211 cs2cl(F) := listify(F)$
00212 fcs2ofcs(FF) := map(listify,FF)$
00213 fcs2fcl(FF) := map(listify,FF)$
00214 
00215 cs2fcl(F) := cl2fcl(cs2cl(F))$
00216 
00217 /* Downcasts: */
00218 
00219 ocs2cs(F) := setify(F)$
00220 cl2cs(F) := setify(F)$
00221 fcl2fcs(FF) := map(setify,FF)$
00222 ofcs2fcs(FF) := map(setify,FF)$
00223 
00224 /* RENAME: fcs2cs */
00225 clauses_f(FF) := FF[2]$
00226 fcs2cs(FF) := second(FF)$
00227 ofcs2ocs(FF) := second(FF)$
00228 fcl2cl(FF) := second(FF)$
00229 fcl2cs(F) := setify(second(F))$
00230 
00231 
00232 /* ***********************************
00233    * Selecting parts of a clause-set *
00234    ***********************************
00235 */
00236 
00237 /* All clauses of length k of a clause-set. */
00238 /* RENAME: scs_k */
00239 scls_k(F,k) := subset(F, lambda([C], is(length(C) = k)))$
00240 scs_k(F,k) := scls_k(F,k)$
00241 
00242 /* All clauses of a clause-set containing a literal. */
00243 /* RENAME: scs_l */
00244 scls_l(F,l) := subset(F, lambda([C], elementp(l,C)))$
00245 scs_l(F,l) := scls_l(F,l)$
00246 
00247 /* All clauses of a clause-set containing a variable.
00248 */
00249 /* RENAME: scs_v */
00250 scls_v(F,v) := subset(F, lambda([C], elementp(v,var_c(C))))$
00251 scs_v(F,v) := scls_v(F,v)$
00252 /* More generally, all clauses containing some of a given set of variables.
00253    This is denoted by "F_V" in articles.
00254  */
00255 /* RENAME: scs_V */
00256 scls_V(F,V) := subset(F, lambda([C], not disjointp(var_c(C),V)))$
00257 scs_V(F,V) := scls_V(F,V)$
00258 socs_V(F,V) := sublist(F, lambda([C], not disjointp(var_c(C),V)))$
00259 
00260 
00261 /* **************************
00262    * Crossing out variables *
00263    **************************
00264 */
00265 
00266 apply_sv_c(V,C) := setdifference(C,literals_v(V))$
00267 
00268 apply_sv_cs(V,F) := block([L : literals_v(V)],
00269   setify(map(lambda([C],setdifference(C,L)),listify(F))))$
00270 apply_sv_cl(V,F) := block([L : literals_v(V)],
00271   map(lambda([C],setdifference(C,L)),F))$
00272 apply_sv_ip_cl(V,_F) := block([L : literals_v(V)],
00273   _F :: map(lambda([C],setdifference(C,L)),ev(_F)),
00274   return(true))$
00275 
00276 restrict_V_cs(F,V) := block([L : literals_v(V)],
00277   disjoin({},setify(map(lambda([C],intersection(C,L)),listify(F)))))$
00278 restrict_V_cl(F,V) := block([L : literals_v(V)],
00279   delete({},map(lambda([C],intersection(C,L)),F)))$
00280 
00281 
00282 /* *****************************************
00283    * Printing clause-sets in Dimacs-format *
00284    *****************************************
00285 */
00286 
00287 /* Output a literal (with trailing space): */
00288 dimacs_l_string(x) := sconcat(x," ")$
00289 
00290 /* Output a clause (with trailing space): */
00291 dimacs_c_string(C) := dimacs_c_stringext(C,dimacs_l_string)$
00292 /* Allows the literal translation to be passed in as function f which
00293    takes a literal and returns a string. */
00294 dimacs_c_stringext(C,f) := xreduce(sconcat, map(f,listify(C)), "")$
00295 
00296 /* Print a formal clause-set in ("extended") Dimacs format where literals
00297    are translated to the strings printed using the function f, which takes
00298    a literal and returns a string. */
00299 /* RENAME: printextf_fcs */
00300 print_fcsext(comment,FF,f) := block(
00301   print_nlb(sconcat("c ", comment)),
00302   print_nlb(sconcat("p cnf ", nvar_fcs(FF), " ", ncl_fcs(FF))),
00303   for C in clauses_f(FF) do print_nlb(sconcat(dimacs_c_stringext(C,f), "0"))
00304 )$
00305 printextf_fcs(comment,FF,f) := print_fcsext(comment,FF,f)$
00306 printextf_fcl(comment,FF,f) := print_fcsext(comment,FF,f)$
00307 
00308 /* Print a formal clause-set in ("extended") Dimacs format (printing terms
00309    directly as strings): */
00310 /* RENAME: printext_fcs */
00311 print_cs_f(comment,FF) := print_fcsext(comment,FF,dimacs_l_string)$
00312 print_fcs(comment,FF) := print_cs_f(comment,FF)$
00313 printext_fcs(comment,FF) := printextf_fcs(comment,FF,dimacs_l_string)$
00314 printext_fcl(comment,FF) := printextf_fcl(comment,FF,dimacs_l_string)$
00315 
00316 /* Remark: The n-parameter in the parameter line is the number of *occurring*
00317    variables. So this function should not be used for printing of standard
00318    Dimacs format, but instead print_fcs_v(comment,FF,[]) should be used
00319    (except when the clause-set is standardised, and there are no gaps
00320    regarding occurring variables).
00321 */
00322 
00323 /* Output formal clause-set FF to file n (using printext_fcs): */
00324 /* RENAME: outputext_fcs */
00325 output_fcs(comment,FF,n) := output_fcsext(comment,FF,n,dimacs_l_string)$
00326 outputext_fcs(comment,FF,n) := outputextf_fcs(comment,FF,n,dimacs_l_string)$
00327 outputext_fcl(comment,FF,n) := outputextf_fcl(comment,FF,n,dimacs_l_string)$
00328 /* Takes additionally a function f which takes a literal and returns
00329    a string, which is used for literal translation at the basic level. */
00330 /* RENAME: outputextf_fcs */
00331 output_fcsext(comment,FF,n,f) := with_stdout(n, print_fcsext(comment,FF,f))$
00332 outputextf_fcs(comment,FF,n,f) := with_stdout(n, printextf_fcs(comment,FF,f))$
00333 outputextf_fcl(comment,FF,n,f) := with_stdout(n, printextf_fcl(comment,FF,f))$
00334 
00335 /* Print a formal clause-set in Dimacs format, together with a map
00336    which explains the meaning of variables (this is useful for example
00337    if variables have been standardised): */
00338 /* RENAME: print_fcs_v */
00339 print_cs_f_v(comment,FF,varlist) := block(
00340  [n : lmax(FF[1]), c : ncl_fcs(FF)],
00341   if n=minf then n:0,
00342   print_nlb(sconcat("c ", comment)),
00343   for i from 1 thru length(varlist) do print_nlb(sconcat("c ", i, " : ", varlist[i])),
00344   print_nlb(sconcat("p cnf ", n, " ", c)),
00345   for C in clauses_f(FF) do print_nlb(sconcat(dimacs_c_string(C), "0"))
00346 )$
00347 print_fcs_v(comment,FF,varlist) := print_cs_f_v(comment,FF,varlist)$
00348 print_fcl_v(comment,FF,varlist) := block(
00349  [n : lmax(FF[1]), c : ncl_fcs(FF)],
00350   if n=minf then n:0,
00351   print_nlb(sconcat("c ", comment)),
00352   block([i:1], for v in varlist do (
00353     print_nlb(sconcat("c ", i, " : ", v)), i : i + 1
00354   )),
00355   print_nlb(sconcat("p cnf ", n, " ", c)),
00356   for C in FF[2] do print_nlb(sconcat(dimacs_c_string(C), "0"))
00357 )$
00358 
00359 /* Output formal clause-set FF to file n, using a variable-list
00360    (based on print_fcs_v): */
00361 /* RENAME: output_fcs_v */
00362 output_cs_f_v(comment,FF,n,varlist) :=
00363   with_stdout(n, print_cs_f_v(comment,FF,varlist))$
00364 output_fcs_v(comment,FF,n,varlist) :=
00365   with_stdout(n, print_cs_f_v(comment,FF,varlist))$
00366 output_fcl_v(comment,FF,n,varlist) :=
00367   with_stdout(n, print_fcl_v(comment,FF,varlist))$
00368 
00369 /* Standard statistics of a formal clause-set as a string:
00370 */
00371 standard_statistics_fcs(FF) := block([S : extended_statistics_fcs(FF)],
00372 sconcat(
00373 "c Number of variables: ", S[1], "
00374 c Number of clauses: ", S[2], "
00375 c Number of literal occurrences: ", S[3], "
00376 c Minimal clause length: ", S[4], "
00377 c Maximal clause length: ", S[5], "
00378 c List of pairs [clause-length m, #clauses of length m]:
00379 c ", S[6], "
00380 c Minimal literal degree: ", S[7], "
00381 c Maximal literal degree: ", S[8], "
00382 c Minimal variable degree: ", S[9], "
00383 c Maximal variable degree: ", S[10]))$
00384 
00385 
00386 /* ****************************************
00387    * Reading clause-sets in Dimacs-format *
00388    ****************************************
00389 */
00390 
00391 oklib_plain_include("stringproc")$
00392 
00393 /* Read a formal clause-list from a DIMACS-file with name "name" (ignoring
00394    the clause-count from the parameter-line, while taking 1,...,n for the
00395    variable-list, where n is the variable-number); returns false in case no
00396    parameter-line was found:
00397 */
00398 read_fcl_f(name) := block([fh : openr(name), line, p_n, p_found : false],
00399   while not p_found and stringp(line : readline(fh))  do (
00400     if (slength(line) >= 1) and (charat(line,1) = "p") then (
00401       p_n : parse_string(tokens(line)[3]),
00402       p_found : true)
00403   ),
00404   if not p_found then false else
00405   [create_list(i,i,1,p_n), rest(map(setify, split_list(read_list(fh),0)),-1)])$
00406 
00407 
00408 /* **************************************
00409    * Printing clause-sets in PLA-format *
00410    **************************************
00411 */
00412 
00413 /* This has no place here, but should be under boolean functions. */
00414 
00415 /* A file in the PLA format represents a partial nxm boolean function f,
00416    that is, a function with domain a subset of {0,1}^n, and as codomain
00417    {0,1}^m. The file encodes a DNF of the relational form f' of f, that is,
00418    f' is the boolean function with domain a subset of {0,1}^{n+m} such that
00419    f'((I,O)) = 1 iff f(I) = O.
00420 ??? this makes no sense ??? DNF's can not specify partial boolean functions f
00421 in this way, since one can not recover the domain of f ???
00422 
00423    A PLA file has a header:
00424 
00425      .i n
00426      .o m
00427 
00428    followed by lines each containing two words I_S and O_S:
00429 
00430 ??? what does this mean ???
00431 
00432  strings of 1s, 0s,
00433    and "-" characters of length n and m respectively. Each such line
00434    indicates that f(I) = O for all I in I* and O in O*. I* and O* are
00435    the sets of all boolean vectors matching I_S and O_S on the 1 and 0
00436    characters, but where all "-" characters have been replaced
00437    (independently) by 0 or 1.
00438 
00439 ??? What is the meaning of "-" in O_S ???
00440 
00441 ??? Apparently what is meant is:
00442 After the two header-lines there are data-lines (possibly zero).
00443 A data-line consists of two strings, calling them x_i, x_o, separated by a
00444 space (how many? and what about comments?).
00445 x_i is of length n, over the alphabet {0,1,-}, while x_o is of length m,
00446 over the alphabet {0,1}. Each position in x_i corresponds to the
00447 input-variable of the same index, and each position in x_o corresponds to the
00448 output-variable of the same index. "-" in x_i states that both values are
00449 possible, and so for example for n=3,m=2 the line "--- 00"
00450 means the constant 2-bit boolean function 0 for all 8 input vectors.
00451 The various data-lines must be consistent with each other, and taken all
00452 together they constitute the partial boolean function.
00453 ???
00454 ??? And what about the input-vectors where no specification applies ??? is
00455 this taken into account into the constructed "partial function" or not ???
00456 or does an implicit totalisation happen ???
00457 
00458    For more information on the PLA format, see
00459    "Improve documentation for Espresso" in
00460    Buildsystem/ExternalSources/SpecialBuilds/plans/BooleanFunctions.hpp.
00461 */
00462 
00463 
00464 /* Outputting a formal clause-list F to PLA format.
00465 
00466    F is considered to be a DNF. The i-th clause in F corresponds to the i-th
00467    non-header line in the PLA. The i-th variable in F corresponds to the
00468    i-th input variable in the PLA, and the output variable of the PLA
00469    corresponds to the output of F w.r.t the corresponding DNF clause.
00470  */
00471 print_fcl2pla(comment, F) := block([F_std, vector],
00472   if comment # "" then print_nlb(sconcat("# ",comment)),
00473   print_nlb(sconcat(".i ", length(F[1]))),
00474   print_nlb(".o 1"),
00475   print_nlb(".type fd"),
00476   F_std : standardise_fcl(F),
00477   for C in F_std[1][2] do (
00478     vector :
00479       create_list(
00480         if elementp(F_std[2][i],C) then "1"
00481         else if elementp(-F_std[2][i],C) then "0"
00482         else "-",
00483         i, 1, length(F[1])),
00484     print_nlb(rreduce(sconcat, vector, " 1"))))$
00485 /* Note the clause-set is considered as a DNF, as this
00486 is the default for the PLA format. */
00487 output_fcl2pla(comment,F,n) := with_stdout(n,print_fcl2pla(comment,F))$
00488 
00489