OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 14.12.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/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00026 
00027 
00028 /* ***************************
00029    * Single resolution steps *
00030    ***************************
00031 */
00032 
00033 /* Checks */
00034 
00035 /* Checks whether two clauses are resolvable: */
00036 resolvable(C,D) := singletonp(intersection(C, comp_sl(D)))$
00037 
00038 /* Checks whether two clauses are resolvable and that the resolvent subsumes
00039    the two parents: */
00040 two_subsumption_resolvable(C,D) := resolvable(C,D) and is(length(symmdifference(C,D)) = 2)$
00041 
00042 
00043 /* Basic resolution operations */
00044 
00045 /* The resolution literal of two resolvable clauses: */
00046 resolution_literal(C,D) := single_element(intersection(C, comp_sl(D)))$
00047 
00048 /* The resolvent of two resolvable clauses: */
00049 resolvent(C,D) := block([x : resolution_literal(C,D)], union(disjoin(x, C), disjoin(-x, D)))$
00050 
00051 
00052 /* Resolution operations as partial operations, returning either [R]  or []. */
00053 
00054 /* If clauses C,D are resolvable with resolution literal x, then return [x],
00055    else return []: */
00056 resolvable_p(C,D) :=  block([clashs : intersection(C, comp_sl(D))],
00057  if length(clashs) = 1 then [single_element(clashs)] else [])$
00058 
00059 /* If C,D are 2-subsumption-resolvable, return [R], else []: */
00060 two_subsumption_resolvent_p(C,D) := block([x : resolvable_p(C,D)],
00061  if not emptyp(x) then
00062   block([x : x[1], R],
00063    R : disjoin(x,C), if R = disjoin(-x,D) then return([R]) else return([]))
00064  else return([]))$
00065 /* two_subsumption_resolvent_p(C,D) =
00066  if two_subsumption_resolvable(C,D) then [resolvent(C,D)] else [] */
00067 
00068 
00069 /* The variations for sets of parent clauses */
00070 
00071 /* Checks whether a set of clauses is resolvable: */
00072 resolvable_s(S) := setp(S) and length(S)=2 and
00073  block([L : listify(S)], resolvable(L[1], L[2]))$
00074 
00075 /* The resolvent of a resolvable set of clauses: */
00076 resolvent_s(S) := block([L : listify(S)], resolvent(L[1], L[2]))$
00077 
00078 
00079 /* The variation for a given resolution literal */
00080 
00081 /* Checks whether two clauses are resolvable on a given resolution literal: */
00082 resolvable_l(C,D,x) := is(intersection(C, comp_sl(D)) = {x})$
00083 
00084 /* Checks whether a set of clauses is resolvable on a given resolution literal: */
00085 resolvable_s_l(S,x) := block([L : listify(S)], resolvable_l(L[1], L[2], x) or
00086  resolvable_l(L[1], L[2], -x))$
00087 
00088 /* The resolvent of two resolvable clauses on a given resolution literal: */
00089 resolvent_l(C,D,x) := union(disjoin(x, C), disjoin(-x, D))$
00090 
00091 /* The resolvent of a resolvable set of clauses on a given resolution literal:
00092 */
00093 resolvent_s_l(S,x) := block([L : listify(S)], setdifference(union(L[1], L[2]), {x,-x}))$
00094 
00095 
00096 /* *************************
00097    * Adding all resolvents *
00098    *************************
00099 */
00100 
00101 /* The resolvable 2-sets of a clause-set: */
00102 resolvable_cs(F) := block([LF : l2array(listify(F)), l : length(F), R : []],
00103  for i : 1 thru l-1 do block([C : LF[i]],
00104   for j : i+1 thru l do
00105    if resolvable(C, LF[j]) then R : cons({C,LF[j]}, R)),
00106  return(setify(R)))$
00107 /* resolvable_cs(F) = subset(powerset(F,2), resolvable_s) */
00108 
00109 /* The 2-subsumption-resolvable 2-sets of a clause-set: */
00110 two_subsumption_resolvable_cs(F) := block(
00111  [LF : l2array(listify(F)), l : length(F), R : []],
00112  for i : 1 thru l-1 do block([C : LF[i]],
00113   for j : i+1 thru l do
00114    if two_subsumption_resolvable(C, LF[j]) then R : cons({C,LF[j]}, R)),
00115  return(setify(R)))$
00116 
00117 /* All resolvents of a clause-set: */
00118 resolvents_cs(F) := map(resolvent_s, resolvable_cs(F))$
00119 
00120 /* All 2-subsumption-resolvents of a clause-set: */
00121 two_subsumption_resolvents_cs(F) := map(resolvent_s, two_subsumption_resolvable_cs(F))$
00122 
00123 /* Returns a pair [res, R], where res is the set of 2-subsumption-resolvents
00124    of F, while R is the set of remaining clauses of F, i.e., clauses not
00125    subsumed by their 2-subsumption-resolvents: */
00126 two_subsumption_resolvents_rem_cs(F) := block(
00127  [L : l2array(listify(F)), l : length(F), subsumed, result : {}],
00128   subsumed : okl_make_array(fixnum, l),
00129   for i : 1 thru l - 1 do block([C : L[i], used : false],
00130     for j : i+1 thru l do block([R : two_subsumption_resolvent_p(C,L[j])],
00131       if not emptyp(R) then (
00132         result : adjoin(R[1], result),
00133         used : true, subsumed[j] : 1)),
00134     if used then subsumed[i] : 1),
00135   return([result,setify(sublist_indicator(array2l(L),subsumed))]))$
00136 
00137 /* Adds all resolvents to a clause-set: */
00138 add_resolvents_cs(F) := union(F, resolvents_cs(F))$
00139 
00140 
00141 
00142 /* ***********************
00143    * Iterated resolution *
00144    ***********************
00145 */
00146 
00147 monitorcheck_resolution_closure_init(name) := if oklib_monitor then (
00148   print(sconcat("M[",name,"]:"), history))$
00149 monitorcheck_resolution_closure_loop(name) := if oklib_monitor then (
00150   print(last(history)))$
00151 
00152 
00153 /* The (full) resolution closure of a clause-set, returning a pair, where
00154    the second element is the list of clause-counts for the stages: */
00155 resolution_closure_cs(F) := block(
00156  [nF : add_resolvents_cs(F), history : [length(F)]],
00157   history : append(history, [length(nF)]),
00158   monitorcheck_resolution_closure_init("resolution_closure_cs"),
00159   while length(nF) > length(F) do (
00160     F : nF, nF : add_resolvents_cs(F),
00161     history : append(history, [length(nF)]),
00162     monitorcheck_resolution_closure_loop("resolution_closure_cs")
00163   ),
00164   return([nF, rest(history,-1)]))$
00165 
00166 
00167 /* Adds all resolvents to a clause-set and then applies
00168    subsumption-elimination: */
00169 min_add_resolvents_cs(F) := min_elements(add_resolvents_cs(F))$
00170 
00171 /* The prime-implicates of a clause-set F (as CNF), and the list of
00172    clause-counts for the successive extensions of F (until a fixed point is
00173    reached): */
00174 min_resolution_closure_cs(F) := block(
00175  [nF : min_add_resolvents_cs(F), history : [length(F)]],
00176   history : append(history, [length(nF)]),
00177   monitorcheck_resolution_closure_init("min_resolution_closure_cs"),
00178   while nF # F do (
00179     F : nF, nF : min_add_resolvents_cs(F),
00180     history : append(history, [length(nF)]),
00181     monitorcheck_resolution_closure_loop("min_resolution_closure_cs")
00182   ),
00183   return([nF, rest(history,-1)]))$
00184 /* A basic equality is
00185    min_resolution_closure_cs(F)[1] = min_elements(resolution_closure_cs(F)[1]).
00186    Another basic equality (yielding an alternative computation) is
00187    min_resolution_closure_cs(F)[1] = min_2resolution_closure_cs(expand_fcs(cs2fcs(F))[2]).
00188 */
00189 
00190 
00191 /* *****************
00192    * DP resolution *
00193    *****************
00194 */
00195 
00196 /* The resolvable 2-sets of a clause-set on a given resolution literal: */
00197 resolvable_cs_l(F,x) :=
00198   subset(powerset(F,2), lambda([Cs], resolvable_s_l(Cs,x)))$
00199 
00200 /* All resolvents of a clause-set on a given resolution literal: */
00201 resolvents_cs_l(F,x) :=
00202   map(lambda([S], resolvent_s_l(S,x)), resolvable_cs_l(F,x))$
00203 
00204 /* The DP-operator in one step for clause-set F and resolution literal v: */
00205 /* RENAME: dp_operator_cs */
00206 dp_operator(F,v) := block(
00207  [Fv : subset(F, lambda([C], not disjointp(C, {v,-v})))],
00208   union(setdifference(F, Fv), resolvents_cs_l(Fv,v)))$
00209 dp_operator_cs(F,v) := dp_operator(F,v)$
00210 dp_operator_fcs(FF,v) := [disjoin(v,FF[1]), dp_operator_cs(FF[2],v)]$
00211 
00212 /* DP combined with subsumption elimination: */
00213 /* RENAME: min_dp_operator_cs */
00214 min_dp_operator(F,v) := min_elements(dp_operator(F,v))$
00215 min_dp_operator_cs(F,v) := min_dp_operator(F,v)$
00216 
00217 /* Returns a list of pairs [s,c], where s is the size of DP-procedure-run
00218    (the sum of sizes of the clause-sets) and c is the count, where the list
00219    is sorted by ascending s: */
00220 distribution_min_dp(FF) := block(
00221  [P : permutations(FF[1]), l : length(FF[2]), hash, counts : {}],
00222   for p in P do block([F : FF[2], s : l],
00223     for v in p do (
00224       F : min_dp_operator(F,v),
00225       s : s + length(F)
00226     ),
00227     if elementp(s, counts) then hash[s] : hash[s] + 1 else (
00228       counts : adjoin(s, counts), hash[s] : 1)
00229   ),
00230   return(create_list([s, hash[s]], s, listify(counts))))$
00231 
00232 
00233 /* ****************************
00234    * Width-bounded resolution *
00235    ****************************
00236 */
00237 
00238 /* Checks whether two clauses are k-resolvable: */
00239 kresolvable(C,D,k) := resolvable(C,D) and (length(C)<=k or length(D)<=k)$
00240 /* Checks whether a set of clauses is k-resolvable: */
00241 kresolvable_s(S,k) := resolvable_s(S) and
00242   (length(first(S))<=k or length(second(S))<=k)$
00243 /* The k-resolvable 2-sets of a clause-set: */
00244 kresolvable_cs(F,k) := block([LF : l2array(listify(F)), l : length(F), R : []],
00245  for i : 1 thru l-1 do block([C : LF[i]],
00246   for j : i+1 thru l do
00247    if kresolvable(C,LF[j],k) then R : cons({C,LF[j]}, R)),
00248  setify(R))$
00249 /*
00250   kresolvable_cs(F,k) = subset(powerset(F,2), lambda([S],kresolvable_s(S,k))
00251 */
00252 
00253 
00254 /* All k-resolvents of a clause-set: */
00255 kresolvents_cs(F,k) := map(resolvent_s, kresolvable_cs(F,k))$
00256 /* Adds all k-resolvents to a clause-set: */
00257 add_kresolvents_cs(F,k) := union(F, kresolvents_cs(F,k))$
00258 
00259 
00260 monitorcheck_kresolution_closure_init(name) := if oklib_monitor then (
00261   print(sconcat("M[",name,"]:"), history))$
00262 monitorcheck_kresolution_closure_loop(name) := if oklib_monitor then (
00263   print(last(history)))$
00264 
00265 /* The k-resolution (asymmetric width) closure of a clause-set, returning a
00266    pair, where the second element is the list of clause-counts for the
00267    stages:
00268 */
00269 kresolution_closure_cs(F,k) := block(
00270  [nF : add_kresolvents_cs(F,k), history : [length(F)]],
00271   history : append(history, [length(nF)]),
00272   monitorcheck_kresolution_closure_init("kresolution_closure_cs"),
00273   while length(nF) > length(F) do (
00274     F : nF, nF : add_kresolvents_cs(F,k),
00275     history : append(history, [length(nF)]),
00276     monitorcheck_kresolution_closure_loop("kresolution_closure_cs")
00277   ),
00278   return([nF, rest(history,-1)]))$
00279 
00280 /* Adds all k-resolvents to a clause-set and then applies
00281    subsumption-elimination: */
00282 min_add_kresolvents_cs(F,k) := min_elements(add_kresolvents_cs(F,k))$
00283 
00284 /* The minimal clauses derivable by k-resolution of a clause-set F,
00285    and the list of clause-counts for the successive extensions of F (until a
00286    fixed point is  reached):
00287 */
00288 min_kresolution_closure_cs(F,k) := block(
00289  [nF : min_add_kresolvents_cs(F,k), history : [length(F)]],
00290   history : append(history, [length(nF)]),
00291   monitorcheck_kresolution_closure_init("min_kresolution_closure_cs"),
00292   while nF # F do (
00293     F : nF, nF : min_add_kresolvents_cs(F,k),
00294     history : append(history, [length(nF)]),
00295     monitorcheck_kresolution_closure_loop("min_kresolution_closure_cs")
00296   ),
00297   return([nF, rest(history,-1)]))$
00298 /* A basic equality is
00299     min_kresolution_closure_cs(F,k)[1] =
00300       min_elements(kresolution_closure_cs(F,k)[1]).
00301 */
00302 
00303 
00304 /* Checks whether two clauses are symmetric k-resolvable
00305    ("bounded resolution"):
00306 */
00307 bresolvable(C,D,k) := length(C)<=k and length(D)<=k and resolvable(C,D) and
00308  length(resolvent(C,D))<=k$
00309 /* Checks whether a set of clauses is symmetric k-resolvable: */
00310 bresolvable_s(S,k) := length(S)=2 and bresolvable(first(S),second(S),k)$
00311 /* The symmetric k-resolvable 2-sets of a clause-set: */
00312 bresolvable_cs(F,k) := block([LF : l2array(listify(F)), l : length(F), R : []],
00313  for i : 1 thru l-1 do block([C : LF[i]],
00314   for j : i+1 thru l do
00315    if bresolvable(C,LF[j],k) then R : cons({C,LF[j]}, R)),
00316  setify(R))$
00317 /*
00318   bresolvable_cs(F,k) = subset(powerset(F,2), lambda([S],bresolvable_s(S,k))
00319 */
00320 
00321 
00322 /* All symmetric k-resolvents of a clause-set: */
00323 bresolvents_cs(F,k) := map(resolvent_s, bresolvable_cs(F,k))$
00324 /* Adds all symmetric k-resolvents to a clause-set: */
00325 add_bresolvents_cs(F,k) := union(F, bresolvents_cs(F,k))$
00326 
00327 
00328 /* The symmetric k-resolution closure of a clause-set, returning a pair, where
00329    the second element is the list of clause-counts for the stages:
00330 */
00331 bresolution_closure_cs(F,k) := block(
00332  [nF : add_bresolvents_cs(F,k), history : [length(F)]],
00333   history : append(history, [length(nF)]),
00334   monitorcheck_kresolution_closure_init("bresolution_closure_cs"),
00335   while length(nF) > length(F) do (
00336     F : nF, nF : add_bresolvents_cs(F,k),
00337     history : append(history, [length(nF)]),
00338     monitorcheck_kresolution_closure_loop("bresolution_closure_cs")
00339   ),
00340   return([nF, rest(history,-1)]))$
00341 
00342 /* Adds all symmetric k-resolvents to a clause-set and then applies
00343    subsumption-elimination: */
00344 min_add_bresolvents_cs(F,k) := min_elements(add_bresolvents_cs(F,k))$
00345 
00346 /* The minimal clauses derivable by symmetric k-resolution of a clause-set F,
00347    and the list of clause-counts for the successive extensions of F (until a
00348    fixed point is  reached):
00349 */
00350 min_bresolution_closure_cs(F,k) := block(
00351  [nF : min_add_bresolvents_cs(F,k), history : [length(F)]],
00352   history : append(history, [length(nF)]),
00353   monitorcheck_kresolution_closure_init("min_bresolution_closure_cs"),
00354   while nF # F do (
00355     F : nF, nF : min_add_bresolvents_cs(F,k),
00356     history : append(history, [length(nF)]),
00357     monitorcheck_kresolution_closure_loop("min_bresolution_closure_cs")
00358   ),
00359   return([nF, rest(history,-1)]))$
00360 /* A basic equality is
00361     min_bresolution_closure_cs(F,k)[1] =
00362       min_elements(bresolution_closure_cs(F,k)[1]).
00363 */
00364 
00365 
00366 /* *******************
00367    * Blocked clauses *
00368    *******************
00369 */
00370 
00371 /* A clause C is blocked for a clause-set F if there exists a literal l in C,
00372    called the blocking literal, such that no resolution in F on l with C
00373    is possible.
00374 
00375    A blocked extension of a clause-set F is a clause-set F' such that
00376    the (confluent) result of removing blocked clauses from union(F',F)
00377    and F yields the same result. This is equivalent to checking whether
00378    the result of removing blocked clauses from union(F',F) is a subset of F.
00379 */
00380 
00381 /* Checking whether l is a blocking literal in a clause C for clause-set F: */
00382 blocking_literal_p(F,C,l) :=
00383   elementp(C,F) and elementp(l,C) and
00384     every_s(lambda([D], not(elementp(-l,D)) or not(resolvable(C,D))), F)$
00385 
00386 /* Checking whether the clause C is blocked for F: */
00387 blocked_cs_p(F,C) := some_s(lambda([l], blocking_literal_p(F,C,l)), C)$
00388 
00389 /* Eliminating blocked clauses from F: */
00390 elim_blocked_cs(F) := block([tF : F, had_blocked : true],
00391   while had_blocked do block([F_blocked],
00392     F_blocked : subset(tF, lambda([C], blocked_cs_p(tF,C))),
00393     if emptyp(F_blocked) then had_blocked : false
00394     else tF : setdifference(tF, F_blocked)),
00395   return(tF))$
00396 /* Eliminating blocked clauses of length at most k from F: */
00397 elim_blockedk_cs(F,k) := block([tF : F, had_blocked : true],
00398   while had_blocked do block([F_blocked],
00399     F_blocked : subset(tF, lambda([C], is(length(C)<=k) and blocked_cs_p(tF,C))),
00400     if emptyp(F_blocked) then had_blocked : false
00401     else tF : setdifference(tF, F_blocked)),
00402   return(tF))$
00403 
00404 
00405 /* Checking whether eF is a blocked extension of F: */
00406 blocked_extension_cs_p(eF,F) :=
00407   subsetp(elim_blocked_cs(union(eF,F)), F)$
00408