OKlibrary  0.2.1.6
Search.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 7.10.2011 (Swansea) */
00002 /* Copyright 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/Resolution/Basics.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")$
00028 
00029 
00030 /* *******************
00031    * Tree resolution *
00032    *******************
00033 */
00034 
00035 /* Computes first(resolution_closure_cs(F)), where to every resolvent its
00036    tree-resolution computation is given, via a hash-map, target stands
00037    for a clause for which the search can be aborted when that clause
00038    has been derived (use for example target=0 if the full closure shall
00039    be computed).
00040 */
00041 resolution_closure_treecomp_cs(F,target) := block(
00042  [finished : F,
00043   complexity : sm2hm(cartesian_product(F,{1})),
00044   queue : cartesian_product({3},resolvents_cs(F)),
00045   abortion : false
00046  ],
00047   if elementp(target,finished) then return(complexity),
00048   while not emptyp(queue) and not abortion do block(
00049    [Rp : first_element(queue), R, m],
00050    queue : disjoin(Rp,queue),
00051    [m,R] : Rp,
00052    if not elementp(R,finished) then block(
00053      [partners : subset(finished, lambda([C], resolvable(C,R)))],
00054      finished : adjoin(R,finished),
00055      set_hm(complexity, R, m),
00056      if R=target then (abortion : true, return(false)),
00057      for C in partners do block([E : resolvent(C,R)],
00058        if not elementp(E,finished) then
00059          queue : adjoin([ev_hm(complexity,C)+ev_hm(complexity,R)+1,E], queue)
00060      )
00061    )
00062   ),
00063   return(complexity))$
00064 
00065 /* Computes the tree-resolution complexity of deriving the empty clause
00066    from clause-set F:
00067 */
00068 treecomp_refutation_cs(F) := ev_hm(resolution_closure_treecomp_cs(F,{}),{})$
00069 
00070 
00071 /* ***********************************
00072    * Short resolution proofs via SAT *
00073    ***********************************
00074 */
00075 
00076 /*
00077   Consider an ordered formal clause-set F. Let n := n(F), c := c(F).
00078   It is to be decided whether F has a resolution refutation using at most
00079   k resolution steps, for k >= 1.
00080 
00081   The signed formal non-boolean clause-list
00082     shortresref_fcl2snbfclfd(F,k)
00083   has its satisfying assignments correspond to such resolution refutations.
00084 */
00085 
00086 /* Variables */
00087 
00088 kill(sres_cl)$
00089 declare(sres_cl, noun)$
00090 sres_cl_var(p,i) := nounify(sres_cl)(p,i)$
00091 /* sres_cl(p,i) in {-1,0,+1} with meaning that position p in clause i in
00092    the resolution refutation is negative, not occurring, or positive;
00093    p in {1,...,n(F)}, i in {1,...,c(F)+k}.
00094 */
00095 
00096 kill(sres_rp1, sres_rp2)$
00097 declare(sres_rp1, noun, sres_rp2, noun)$
00098 sres_rp1_var(i) := nounify(sres_rp1)(i)$
00099 sres_rp2_var(i) := nounify(sres_rp2)(i)$
00100 /* sres_rp1_var(i), sres_rp2_var(i) in {1,...,i-1}
00101    mean the indices of the two parent clauses.
00102 */
00103 
00104 kill(sres_rv)$
00105 declare(sres_rv, noun)$
00106 sres_rv_var(i) := nounify(sres_rv)(i)$
00107 /* sres_rv(i) in {1,...,n} for i in {c(F)+1,...,c(F)+k} means the
00108    resolution variable for clause i in the resolution proof.
00109 */
00110 
00111 /* The list of non-boolean variables for parameters n,c,k: */
00112 var_shortres(n,c,k) := append(
00113  create_list(sres_cl_var(p,i), p,1,n, i,1,c+k),
00114  create_list(sres_rp1_var(i), i,c+1,c+k),
00115  create_list(sres_rp2_var(i), i,c+1,c+k),
00116  create_list(sres_rv_var(i), i,c+1,c+k)
00117 )$
00118 
00119 /* The ordered domains: */
00120 domain_shortres(n) := buildq([N:create_list(i,i,1,n)],
00121   lambda([v],
00122     if op(v)=sres_cl then [-1,0,+1]
00123     elseif op(v)=sres_rp1 or op(v)=sres_rp2 then create_list(i,i,1,first(args(v))-1)
00124     else N
00125   )
00126 )$
00127 
00128 
00129 /* Clauses */
00130 
00131 /* Resolution variables not in resolvent (c+1 <= i <= c+k): */
00132 sres_resvnresol_snbcl(i,n) :=
00133   create_list({[sres_rv_var(i),v,-1], [sres_cl_var(v,i),0,+1]}, v,1,n)$
00134 
00135 /* Resolution variables in parent clauses (c+1 <= i <= c+k): */
00136 sres_resvparent1_snbcl(i,n) :=
00137   create_list({[sres_rv_var(i),v,-1], [sres_rp1_var(i),p1,-1], [sres_cl_var(v,p1),1,+1]},
00138     v,1,n, p1,1,i-1)$
00139 sres_resvparent2_snbcl(i,n) :=
00140   create_list({[sres_rv_var(i),v,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p2),-1,+1]},
00141     v,1,n, p2,1,i-1)$
00142 
00143 /* No further conflicts in parent clauses (c+1 <= i <= c+k): */
00144 sres_noconflicts_snbcl(i,n) :=
00145   lappend(create_list(
00146     [{[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p1),1,-1], [sres_cl_var(v,p2),-1,-1]},
00147      {[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p1),-1,-1], [sres_cl_var(v,p2),1,-1]}],
00148     v,1,n, p1,1,i-1, p2,append(create_list(j,j,1,p1-1),create_list(j,j,p1+1,i-1))))$
00149 
00150 /* Literals tranferred from parent clauses to resolvent (c+1 <= i <= c+k): */
00151 sres_resolvent_snbcl(i,n) :=
00152   lappend(create_list(
00153     [{[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p1),1,-1], [sres_cl_var(v,i),1,+1]},
00154      {[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p2),1,-1], [sres_cl_var(v,i),1,+1]},
00155      {[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p1),-1,-1], [sres_cl_var(v,i),-1,+1]},
00156      {[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p2),-1,-1], [sres_cl_var(v,i),-1,+1]},
00157      {[sres_rv_var(i),v,1], [sres_rp1_var(i),p1,-1], [sres_rp2_var(i),p2,-1], [sres_cl_var(v,p1),0,-1], [sres_cl_var(v,p2),0,-1], [sres_cl_var(v,i),0,+1]}],
00158   v,1,n, p1,1,i-1, p2,append(create_list(j,j,1,p1-1),create_list(j,j,p1+1,i-1))))$
00159 
00160 
00161 /* Clause-sets */
00162 
00163 shortres_gen_snbfclfd(n,c,k) := [
00164   var_shortres(n,c,k),
00165   append(lappend(create_list(sres_resvnresol_snbcl(i,n),i,c+1,c+k)),
00166          lappend(create_list(sres_resvparent1_snbcl(i,n),i,c+1,c+k)),
00167          lappend(create_list(sres_resvparent2_snbcl(i,n),i,c+1,c+k)),
00168          lappend(create_list(sres_noconflicts_snbcl(i,n),i,c+1,c+k)),
00169          lappend(create_list(sres_resolvent_snbcl(i,n),i,c+1,c+k))),
00170   domain_shortres(n)]$
00171 
00172 /* Encoding a formal list of (boolean) clauses: */
00173 shortres_fcl2snbcl(FF) := block(
00174  [n : nvar_fcl(FF), c : ncl_fcl(FF), Avar : l2ary(first(FF)), Acl : l2ary(fcl2cl(FF))],
00175   create_list(
00176     {[sres_cl_var(p,i), if elementp(Avar[p],Acl[i]) then 1 else if elementp(-Avar[p],Acl[i]) then -1 else 0, 1]}, i,1,c, p,1,n))$
00177 
00178 /* Encoding the empty clause as target of the proof: */
00179 shortres_emptycl_snbcl(n,c,k) := create_list(
00180   {[sres_cl_var(p,c+k),0,1]}, p,1,n)$
00181 
00182 /* Translation of the condition, that the formal clause-list FF has a
00183    resolution refutation using k resolution steps, into a signed non-boolean
00184    formal clause-list:
00185 */
00186 shortresref_fcl2snbfclfd(FF,k) := block([n : nvar_fcl(FF), c : ncl_fcl(FF), T],
00187   T : shortres_gen_snbfclfd(n,c,k),
00188   [first(T),
00189    append(shortres_fcl2snbcl(FF), second(T), shortres_emptycl_snbcl(n,c,k)),
00190    third(T)])$
00191 
00192 /* Translation into a boolean clause-list: */
00193 shortresref_aloamo_fcl(FF,k) :=
00194   snbfclfd2fcl_aloamo(shortresref_fcl2snbfclfd(FF,k))$
00195 
00196 
00197 /* Additional clauses: */
00198 
00199 /* Setting the first resolvent as the resolvent of clauses i, j; FF is a
00200    formal clause-list: */
00201 shortresref_setfirstresolvent_snbcl(FF, i, j) := block(
00202  [n : nvar_fcl(FF), c : ncl_fcl(FF), Avar : l2ary(first(FF)),
00203   C : FF[2][i], D : FF[2][j], v, vi : 0, R],
00204   v : var_l(resolution_literal(C,D)),
00205   for k : 1 thru n while vi = 0 do if Avar[k] = v then vi : k,
00206   R : resolvent(C,D),
00207   append(
00208    create_list(
00209     {[sres_cl_var(p,c+1), if elementp(Avar[p],R) then 1 else if elementp(-Avar[p],R) then -1 else 0, 1]}, p,1,n),
00210    [{[sres_rv_var(c+1), vi, 1]}],
00211    [{[sres_rp1_var(c+1), i, 1]}, {[sres_rp2_var(c+1), j,1]}]))$
00212 
00213 
00214 /* Measures for the translated formulas */
00215 
00216 /* The number of variables in the signed non-boolean clause-set: */
00217 nvar_shortres_snbfclfd(n,c,k) := n*(c+k) + 3*k$
00218 
00219 /* The number of variables in the boolean translation: */
00220 nvar_shortres_aloamo(n,c,k) := n*(c+k)*3 + 2*(k^2/2+c*k-k/2) + k*n$
00221 /* Remark:
00222    sum(i-1,i,c+1,c+k) = k^2/2+c*k-k/2
00223 */
00224 
00225 /* The number of clauses in the generic basis of the signed non-boolean
00226    clause-list: */
00227 ncl_shortres_gen_snbfclfd(n,c,k) :=
00228   n* k + /* sres_resvnresol_snbcl */
00229   n* (k^2/2+c*k-k/2) * 2 + /* sres_resvparent1_snbcl, sres_resvparent2_snbcl */
00230   n* (k^3/3+c*k^2-k^2+c^2*k-2*c*k+2*k/3) * 2 + /* sres_noconflicts_snbcl */
00231   n* (k^3/3+c*k^2-k^2+c^2*k-2*c*k+2*k/3) * 5$ /* sres_resolvent_snbcl */
00232 /* Remarks:
00233    sum(i-1,i,c+1,c+k) = k^2/2+c*k-k/2
00234    sum((i-1)*(i-2),i,c+1,c+k) = k^3/3+c*k^2-k^2+c^2*k-2*c*k+2*k/3
00235 */
00236 
00237 /* The number of clauses in the completed signed non-boolean clause-list: */
00238 ncl_shortresref_snbfclfd(n,c,k) := ncl_shortres_gen_snbfclfd(n,c,k) +
00239   (c+1) * n$
00240 
00241 /* The number of clauses in the boolean translation: */
00242 ncl_shortresref_aloamo(n,c,k) := ncl_shortresref_snbfclfd(n,c,k) +
00243   n*(c+k)*(1+3) +
00244   2*(k + k^3/6+c*k^2/2-k^2/2+c^2*k/2-c*k+k/3) +
00245   k*(1+n*(n-1)/2)$
00246 /* Remark:
00247    sum(binomial(i-1,2),i,c+1,c+k) = k^3/6+c*k^2/2-k^2/2+c^2*k/2-c*k+k/3
00248 */
00249 
00250 /* Convenience versions, using the input FF instead of its parameters n, c: */
00251 
00252 nvar_shortres_fcl2snbfclfd(FF,k) := nvar_shortres_snbfclfd(nvar_fcl(FF), ncl_fcl(FF),k)$
00253 ncl_shortresref_fcl2snbfclfd(FF,k) := ncl_shortresref_snbfclfd(nvar_fcl(FF), ncl_fcl(FF),k)$
00254 
00255 nvar_shortres_aloamo_fcl(FF,k) := nvar_shortres_aloamo(nvar_fcl(FF), ncl_fcl(FF),k)$
00256 ncl_shortresref_aloamo_fcl(FF,k) := ncl_shortresref_aloamo(nvar_fcl(FF), ncl_fcl(FF),k)$
00257