OKlibrary  0.2.1.6
NonBooleanTranslations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.4.2009 (Swansea) */
00002 /* Copyright 2009, 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/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00030 
00031 
00032 /* ****************************
00033    * The "direct" translation *
00034    ****************************
00035 */
00036 
00037 /* Variables are "nbv(v,e)", meaning that variable v has value e: */
00038 kill(nbv)$
00039 declare(nbv, noun)$
00040 declare(nbv, posfun)$
00041 nbv_var(v,e) := nounify(nbv)(v,e)$
00042 
00043 /* First for non-boolean clause-sets. */
00044 
00045 /* Just translating the clauses: */
00046 /* Variables are returned in lexicographical order when considering first the
00047    original variables and then the values. */
00048 nbfclfd2fcl_core(FF) :=
00049  [create_list(nbv_var(v,x), v,FF[1], x,FF[3](v)),
00050   map(lambda([C],map(lambda([x],-apply(nbv_var,x)),C)),FF[2])]$
00051 nbfclud2fcl_core(FF) := nbfclfd2fcl_core(nbfclud2nbfclfd(FF))$
00052 nbfcsfd2fcs_core(FF) := fcl2fcs(nbfclfd2fcl_core(nbfcsfd2nbfclfd(FF)))$
00053 
00054 /* The "weak" translation, allowing that a variable gets multiple values: */
00055 nbfclfd2fcl_alo(FF) := block([GG : nbfclfd2fcl_core(FF)],
00056  [GG[1], append(GG[2],
00057     create_list(setify(create_list(nbv_var(v,p), p,FF[3](v))), v,FF[1]))])$
00058 nbfclud2fcl_alo(FF) := nbfclfd2fcl_alo(nbfclud2nbfclfd(FF))$
00059 nbfcsfd2fcs_alo(FF) := fcl2fcs(nbfclfd2fcl_alo(nbfcsfd2nbfclfd(FF)))$
00060 
00061 /* The "strong" translation, establishing a 1-1 correspondence between the
00062    sets of satisfying assignments before and after translation:
00063 */
00064 nbfclfd2fcl_aloamo(FF) := block([GG : nbfclfd2fcl_alo(FF)],
00065  [GG[1], append(GG[2],
00066     create_list({-nbv_var(v,first(p)), -nbv_var(v,second(p))},
00067                 v,FF[1], p,powerset_l(FF[3](v),2)))])$
00068 nbfclud2fcl_aloamo(FF) := nbfclfd2fcl_aloamo(nbfclud2nbfclfd(FF))$
00069 nbfcsfd2fcs_aloamo(FF) := fcl2fcs(nbfclfd2fcl_aloamo(nbfcsfd2nbfclfd(FF)))$
00070 nbfcsud2fcs_aloamo(FF) := fcl2fcs(nbfclud2fcl_aloamo(nbfcsud2nbfclud(FF)))$
00071 
00072 
00073 /* Now for signed non-boolean clause-sets. */
00074 
00075 /* Just translating the clauses: */
00076 /* Variables are returned in lexicographical order when considering first the
00077    original variables and then the values. */
00078 snbfclfd2fcl_core(FF) :=
00079  [create_list(nbv_var(v,x), v,FF[1], x,FF[3](v)),
00080   map(lambda([C],map(lambda([x],third(x)*apply(nbv_var,rest(x,-1))),C)),
00081       FF[2])]$
00082 snbfclud2fcl_core(FF) := snbfclfd2fcl_core(snbfclud2snbfclfd(FF))$
00083 snbfcsfd2fcs_core(FF) := fcl2fcs(snbfclfd2fcl_core(snbfcsfd2snbfclfd(FF)))$
00084 
00085 /* Here we need to use both alo- and amo-clauses: */
00086 snbfclfd2fcl_aloamo(FF) := block([GG : snbfclfd2fcl_core(FF)],
00087  [GG[1],
00088   append(GG[2],
00089     create_list(setify(create_list(nbv_var(v,p), p,FF[3](v))), v,FF[1]),
00090     create_list({-nbv_var(v,first(p)), -nbv_var(v,second(p))},
00091                 v,FF[1], p,powerset_l(FF[3](v),2)))
00092  ])$
00093 snbfclud2fcl_aloamo(FF) := snbfclfd2fcl_aloamo(snbfclud2snbfclfd(FF))$
00094 snbfcsfd2fcs_aloamo(FF) := fcl2fcs(snbfclfd2fcl_aloamo(snbfcsfd2snbfclfd(FF)))$
00095 
00096 
00097 /* Tools: */
00098 
00099 /* For a partial assignments with variables nbv(i,j), extract the corresponding
00100    block-partition:
00101 */
00102 extract_partition(pa) := block(
00103  [number_blocks : lmax(map(second,pa)), A],
00104   if number_blocks = minf then return([]),
00105   A : okl_make_array(any,number_blocks),
00106   for i : 1 thru number_blocks do A[i] : {},
00107   for x in pa do A[second(x)] : adjoin(first(x), A[second(x)]),
00108   ary2l(A))$
00109 
00110 
00111 /* **************************************
00112    * The generalised nested translation *
00113    **************************************
00114 */
00115 
00116 /* The same variables nbv(v,e) are used, but now in the form nbv(v,i),
00117    where i is an index. */
00118 
00119 /* Consider a non-boolean formal clause-set FF = [V,F,D]; so
00120    D is the function-domain, and for a variable v the set D(v) is the
00121    set of values of v. We assume that V does not contain variables of the
00122    form nbv(x,y). And we assume that all domains are non-empty.
00123    We consider FF as CNF (so we use "SAT-terminology").
00124 
00125    We assume further that T(v) is an (arbitrary) labelled ordered boolean
00126    unsatisfiable clause-set where the label set contains D(v),
00127    while all variables are of the form nbv(v,i) for in principal arbitrary i.
00128    The clauses of T(v) associated to values e in D(v) are denoted by
00129    T(v,e), while TR(v) := T(v) - {T(v,e) : e in D(v)} is the (possibly
00130    empty) clause-set containing the remaining clauses.
00131 
00132    We assume that all clauses in T(v) - TR(v) are necessary, that is,
00133    for every e in D(v) there is a total assignment phi for the variables
00134    in T(v) such that all clauses except of T(v,e) are satisfied.
00135 
00136    The standard nested translation uses 1 <= i < |D(v)| (while for the
00137    above standard translation we have 1 <= i <= D(v)).
00138 
00139    The translation now replaces every clause C in F by the clause which
00140    is the union of the clauses T(v,e) for the literals [v,e] in C, and
00141    adds furthermore all clauses in T'(v) for all v in V.
00142 
00143    Let D(v) = {e_1, ..., e_k} (k >= 1).
00144 
00145    We obtain the above weak standard translation by letting
00146      T(v) = { {-nbv(v,e_1)}, ..., {-nbv(v,e_k)} } +
00147             { {nbv(v,e_1), ..., nbv(v,e_k)} }
00148    where T(v,e_i) = {-nbv(v,e_i)}.
00149    For the strong standard translation we just add the binary clauses
00150    {-nbv(v,e_i), -nbv(v,e_j)} for i <> j.
00151 
00152    The standard nested translation uses
00153      T(v) = smusat_horn_stdfcl(k-1)
00154    where T(v,e_i) uses some permutation of the clause-list (which is of
00155    length k), and where the variables 1, ..., k-1 are replaced by nbv(v,i).
00156 
00157 */
00158 
00159 /* For a map T(v,e), depending on variables and their values and computing
00160    a clause-set, translate a non-boolean clause C into a new clause which is
00161    the union of the results of applying T to the elements of C:
00162 */
00163 gennest_clause_trans(C,T) := lunion(map(lambda([x],apply(T,x)), C))$
00164 
00165 /* Given a non-boolean formal clause-list FF, a map T(v,e) which associates
00166    to every variable v and its values e a boolean clause in the
00167    variables nbv(v,i), a map TR(v) which associates to every variable v
00168    a clause-list (the "remaining" clauses), and a map TV(v) which associates
00169    to every variable v the list of variables of T(v,e), compute the
00170    boolean clause-set as specified above:
00171 */
00172 gennest_nbfcl2fcl(FF,T,TR,TV) := [
00173  lappend(map(TV,FF[1])),
00174  append(
00175    map(lambda([C], gennest_clause_trans(C,T)), FF[2]),
00176    lappend(map(TR,FF[1]))
00177  )]$
00178 /* Remark: See gennest_nbfcl2fcl_p below for checking correctness. */
00179 
00180 
00181 /* The direct translation */
00182 
00183 standtrans_T(v,e) := {-nbv_var(v,e)}$
00184 standtrans_fd_weak_TR(D) := buildq([D],
00185  lambda([v], [setify(create_list(nbv_var(v,e), e, D(v)))]))$
00186 standtrans_ud_weak_TR(D) := buildq([D],
00187  lambda([v], [setify(create_list(nbv_var(v,e), e, D))]))$
00188 standtrans_fd_TV(D) := buildq([D],
00189  lambda([v], create_list(nbv_var(v,e), e, D(v))))$
00190 standtrans_ud_TV(D) := buildq([D],
00191  lambda([v], create_list(nbv_var(v,e), e, D)))$
00192 
00193 nbfclfd2fcl_alo_2(FF) := gennest_nbfcl2fcl(rest(FF,-1), standtrans_T, standtrans_fd_weak_TR(FF[3]), standtrans_fd_TV(FF[3]))$
00194 nbfclud2fcl_alo_2(FF) := gennest_nbfcl2fcl(rest(FF,-1), standtrans_T, standtrans_ud_weak_TR(FF[3]), standtrans_ud_TV(FF[3]))$
00195 
00196 
00197 /* The standard nested translation */
00198 
00199 /* Using a uniform non-empty domain D, and ordering the saturated Horn clause
00200    in the same way (from smallest to largest):
00201 */
00202 standnest_T(D) := block([k : length(D), h : osm2hm(l2osm_inv(D))],
00203  buildq([k,h],
00204   lambda([v,e], block([i : ev_hm(h,e)],
00205    if i < k then setify(cons(nbv_var(v,i),create_list(-nbv_var(v,j),j,1,i-1)))
00206    else setify(create_list(-nbv_var(v,j),j,1,i-1))))))$
00207 standnest_TR(D) := lambda([v], [])$
00208 standnest_strong_TR(D) := buildq([Vt : standnest_TV(D)],
00209  lambda([v], listify(powerset(setify(Vt(v)),2))))$
00210 standnest_TV(D) := buildq([l:length(D)],
00211  lambda([v], create_list(nbv_var(v,i), i,1,l-1)))$
00212 
00213 nbfclud2fcl_standnest(FF) := gennest_nbfcl2fcl(rest(FF,-1), standnest_T(FF[3]), standnest_TR(FF[3]), standnest_TV(FF[3]))$
00214 nbfclud2fcl_standnest_strong(FF) := gennest_nbfcl2fcl(rest(FF,-1), standnest_T(FF[3]), standnest_strong_TR(FF[3]), standnest_TV(FF[3]))$
00215 
00216 
00217 /* The logarithmic translation */
00218 
00219 /* For non-empty D only. */
00220 logarithmic_T(D) := block([k : length(D), h : osm2hm(l2osm_inv(D)), A],
00221  A : l2ary(take_l(k,full_cl(ceiling(ld(k))))),
00222  buildq([A,h], lambda([v,e],
00223    map(lambda([x], if x>0 then nbv_var(v,x) else -nbv_var(v,-x)), A[ev_hm(h,e)]))))$
00224 logarithmic_TR(D) := block([k : length(D), L],
00225  L : rest(full_cl(ceiling(ld(k))),k),
00226  buildq([L], lambda([v],
00227    map(lambda([C], map(lambda([x], if x>0 then nbv_var(v,x) else -nbv_var(v,-x)), C)), L))))$
00228 logarithmic_TV(D) := buildq([l:ceiling(ld(length(D)))],
00229  lambda([v], create_list(nbv_var(v,i), i,1,l)))$
00230 
00231 nbfclud2fcl_logarithmic(FF) := gennest_nbfcl2fcl(rest(FF,-1), logarithmic_T(FF[3]), logarithmic_TR(FF[3]), logarithmic_TV(FF[3]))$
00232 
00233 
00234 /* The reduced (nested) translation */
00235 
00236 /* Using a uniform non-empty domain D, and placing the long clause
00237    at the last value:
00238 */
00239 reduced_T(D) := block([k : length(D), h : osm2hm(l2osm_inv(D))],
00240  buildq([k,h],
00241   lambda([v,e], block([i : ev_hm(h,e)],
00242    if i < k then {nbv_var(v,i)}
00243    else setify(create_list(-nbv_var(v,j),j,1,i-1))))))$
00244 reduced_TR(D) := lambda([v], [])$
00245 reduced_strong_TR(D) := buildq([Vt : reduced_TV(D)],
00246  lambda([v], listify(powerset(setify(Vt(v)),2))))$
00247 reduced_TV(D) := buildq([l:length(D)],
00248  lambda([v], create_list(nbv_var(v,i), i,1,l-1)))$
00249 
00250 nbfclud2fcl_reduced(FF) := gennest_nbfcl2fcl(rest(FF,-1), reduced_T(FF[3]), reduced_TR(FF[3]), reduced_TV(FF[3]))$
00251 nbfclud2fcl_reduced_strong(FF) := gennest_nbfcl2fcl(rest(FF,-1), reduced_T(FF[3]), reduced_strong_TR(FF[3]), reduced_TV(FF[3]))$
00252 
00253 
00254 /* ************************************************
00255    * Tools for the generalised nested translation *
00256    ************************************************
00257 */
00258 
00259 /* Checking for correctness of the arguments T,TR,TV of gennest_nbfcl2fcl:
00260    V is the list of variables, D is the functional domain (yielding for
00261    every variable in V a repetition-free list of values), S is a
00262    SAT solver (input a boolean formal clause-set, output true/false).
00263 */
00264 gennest_nbfcl2fcl_p(V,D_,S_, T_,TR_,TV_) := block([counterexample : false],
00265   for v in V unless counterexample do block(
00266    [Fv : map(lambda([e],T_(v,e)),D_(e)), Fr : TR_(v), F,Vv],
00267     if not cl_p(Fv) or not cl_p(Fr) then (counterexample : true, return()),
00268     F : setify(append(Fv, Fr)), Vv : var_cs(F),
00269     if not subsetp(Vv, setify(TV_(v))) or
00270         S_([Vv,F]) # false or
00271         some_s(lambda([E], impliesp_cs(disjoin(E,F),E,S_)), Fv)
00272     then counterexample : true
00273   ),
00274   if counterexample then return(false),
00275   for P in powerset(setify(V),2) unless counterexample do
00276     if not apply(disjointp, map(setify,map(TV_, listify(P)))) then counterexample : true,
00277   return(not counterexample))$
00278 
00279 
00280 /* Find a maximal set of binary clauses (without new variables) which
00281    can be added to the union of F1, F2 while maintaining that all clauses
00282    in F1 are necessary.
00283    Prerequisites: F1, F2 are clause-sets, S is some SAT-solver (input a
00284    boolean formal clause-set, output true/false).
00285 */
00286 add_bincl_nec(F1,F2,S) := block(
00287  [U : union(F1,F2), V],
00288   V : var_cs(U),
00289   for C in random_permutation(setdifference(all_pass_n(V,2),U)) do block(
00290    [new_U : adjoin(C,U)],
00291     if every_s(lambda([D], not impliesp_cs(disjoin(D,new_U),D,S)), F1) then
00292       U : new_U
00293   ),
00294   return(setdifference(U,union(F1,F2))))$
00295 /* Remarks: For a variable v with domain D the meaning of F1, F2
00296    w.r.t. the above description is
00297      F1 = {T(v,e) : e in D}
00298      F2 = TR(v).
00299    add_bincl_nec(F1,F2,S) then computes some maximal set of binary clauses
00300    which can be added to TR(v).
00301 */
00302