OKlibrary  0.2.1.6
Transformations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.9.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2011 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 
00025 
00026 /* **************************************************
00027    * Translated minimally unsatisfiable clause-sets *
00028    **************************************************
00029 */
00030 
00031 /* The translations into MUSAT according to [Papadimitriou, Wolfe 1988] */
00032 
00033 /* New variables are "mupw(i)", where i is the index of the clause in F */
00034 kill(mupw)$
00035 declare(mupw, noun)$
00036 declare(mupw, posfun)$
00037 mupw_var(i) := nounify(mupw)(i)$
00038 
00039 /* Input a formal clause-set F, returns a formal clause-set G such that
00040    if F is satisfiable then G is satisfiable, while if F is unsatisfiable
00041    then G is minimally unsatisfiable.
00042    Thus USAT is reduced to MUSAT. */
00043 usat_musat(FF) := if not freeof(mupw, FF) then error("usat_musat[ERROR]: input contains variable scheme mupw!") else
00044  block([L : listify(FF[2]), m : length(FF[2]), Y],
00045   Y : setify(create_list(mupw_var(i), i, 1, m)),
00046   return(
00047     [union(FF[1], Y), setify(append(
00048       create_list(union(L[i], disjoin(mupw_var(i), Y)), i, 1, m),
00049       create_list(union({-listify(L[i])[j], -mupw_var(i)}, disjoin(mupw_var(i), Y)), i,1,m, j,1,length(L[i])),
00050       create_list({-mupw_var(i), -mupw_var(j)}, i,1,m-1, j,i+1,m)))]
00051   ))$
00052 
00053 /* Measures for the translated formulas */
00054 
00055 /* Number of variables: */
00056 n_var_usat_musat(FF) := nvar_f(FF) + ncl_fcs(FF)$
00057 
00058 /* Number of clauses: */
00059 n_cl_usat_musat(FF) := block([l : nlitocc_fcs(FF), c : ncl_fcs(FF)],
00060   c + l + c*(c-1)/2)$
00061 
00062 /* Deficiency: */
00063 deficiency_usat_musat(FF) := block(
00064  [l : nlitocc_fcs(FF), c : ncl_fcs(FF), n : nvar_f(FF)],
00065   l + c*(c-1)/2 - n)$
00066 
00067 /* List of clause-counts as with ncl_list_fcs: */
00068 ncl_list_usat_musat(FF) := block(
00069  [l : nlitocc_fcs(FF), c : ncl_fcs(FF), h : sm2hm({})],
00070   if l # 0 then set_hm(h, 1+c, l),
00071   if c >= 2 then set_hm(h, 2, ev_hm_d(h,2,0) + c*(c-1)/2),
00072   for P in ncl_list_fcs(FF) do block([cl : P[1]+c-1],
00073     set_hm(h, cl, ev_hm_d(h,cl,0) + P[2])),
00074   return(listify(hm2sm(h))))$
00075 
00076 
00077 /* Input a formal clause-set F, returns a formal clause-set GP such that
00078    if F is satisfiable then GP is minimally unsatisfiable, 
00079    while if F is unsatisfiable then GP is unsatisfiable but not minimally
00080    unsatisfiable. Thus SAT is reduced to MUSAT. */
00081 sat_musat(FF) := block([m : length(FF[2]), Y, G],
00082  Y : setify(create_list(mupw_var(i), i, 1, m)),
00083  G : usat_musat(FF),
00084  return([G[1], union(G[2],{Y})]))$
00085 
00086 /* Measures for the translated formulas */
00087 
00088 /* Number of variables: */
00089 n_var_sat_musat(FF) := n_var_usat_musat(FF)$
00090 
00091 /* Number of clauses: */
00092 n_cl_sat_musat(FF) := n_cl_usat_musat(FF) + 1$
00093 
00094 /* Deficiency: */
00095 deficiency_sat_musat(FF) := deficiency_usat_musat(FF) + 1$
00096 
00097 /* List of clause-counts as with ncl_list_fcs: */
00098 ncl_list_sat_musat(FF) := block(
00099  [l : nlitocc_fcs(FF), c : ncl_fcs(FF), h : sm2hm({})],
00100   if l # 0 then set_hm(h, 1+c, l),
00101   set_hm(h,c,1), /* this is additional, compared to ncl_list_usat_musat(FF) */
00102   if c >= 2 then set_hm(h, 2, ev_hm_d(h,2,0) + c*(c-1)/2),
00103   for P in ncl_list_fcs(FF) do block([cl : P[1]+c-1],
00104     set_hm(h, cl, ev_hm_d(h,cl,0) + P[2])),
00105   return(listify(hm2sm(h))))$
00106 
00107 
00108 /* ********************************************************
00109    * Max-Clique translated to "SHORT RES" and "SMALL MUS" *
00110    ********************************************************
00111 */
00112 
00113 /* According to [Fellows, Szeider, Wrightson; 2006]. */
00114 
00115 /* Variables are "srfswx(i)", "srfswy(i,j)" and "srfswz(v,i)" for natural
00116    numbers i,j and vertices v. */
00117 kill(srfswx,srfswy,srfswz)$
00118 declare(srfswx, noun, srfswy, noun, srfswz, noun)$
00119 declare(srfswx, posfun, srfswy, posfun, srfswz, posfun)$
00120 srfswx_var(i) := nounify(srfswx)(i)$
00121 srfswy_var(i,j) := nounify(srfswy)(i,j)$
00122 srfswz_var(v,i) := nounify(srfswz)(v,i)$
00123 
00124 new_k(k) := binomial(k,2) + 2 * k$
00125 
00126 /* Input a graph G and k >= 0, output a formal clause-set FF 
00127    which contains a minimally unsatisfiable sub-clause-set of size 
00128      at most new_k(k) + 1 iff
00129    FF has a resolution-dag with at most new_k(k) non-source-nodes iff
00130    G contains a clique of size k. 
00131 
00132    Thus contains_us_bydef(maxclique_mures(G,k), new_k(k)+1, Solver) is true
00133    iff G contains a clique of size k.
00134 
00135    Furthermore FF is unsatisfiable iff G has at least one edge.
00136 */
00137 /* Auxiliary functions */
00138 
00139 /* The singleton clause-set {C}, where C is the set of all srfswx(i) for
00140    1 <= i <= k and srfswy(i,j) for 1 <= i < j <= k: */
00141 maxclique_start(k) := {setify(append(create_list(srfswx_var(i),i,1,k), create_list(srfswy_var(i,j), i,1,k-1, j,i+1,k)))}$
00142 maxclique_edges(E,k) := setify(create_list({-srfswy_var(i,j), srfswz_var(listify(E[e])[1],i), srfswz_var(listify(E[e])[2],j)}, i,1,k-1, j,i+1,k, e,1,length(E)))$
00143 /* Remark to maxclique_edges: the underlying paper is ambiguous here whether to use
00144 the orientation of the edges or not (we do). */
00145 maxclique_vertices(V,k) := setify(create_list({-srfswx_var(i), srfswz_var(V[v],i)}, i,1,k, v,1,length(V)))$
00146 maxclique_cleanup(V,k) := setify(create_list({-srfswz_var(V[v],i)}, i,1,k, v,1,length(V)))$
00147 
00148 /* The main function: */
00149 maxclique_mures_fcs(G,k) := block([V : listify(G[1]), E : listify(G[2])],
00150  [union(setify(create_list(srfswx_var(i),i,1,k)), 
00151         setify(create_list(srfswy_var(i,j), i,1,k-1, j,i+1,k)),
00152         setify(create_list(srfswz_var(V[v],i), v,1,length(V), i,1,k))),
00153   union(maxclique_start(k),maxclique_edges(E,k),maxclique_vertices(V,k),maxclique_cleanup(V,k))])$
00154 
00155 /* Measures for the translated formulas */
00156 
00157 /* Number of variables: */
00158 nvar_maxclique_mures_fcs(G,k) := k + binomial(k,2) + length(G[1]) * k$
00159 
00160 /* List of clause-counts as with ncl_list_fcs: */
00161 ncl_list_maxclique_mures_fcs(G,k) := 
00162 block([n : length(G[1]), m : length(G[2])],
00163  if k = 0 then [[0,1]]
00164  elseif k = 1 then 
00165    if n=0 then [[1,1]] else [[1,n+1], [2,n]]
00166  elseif k = 2 then 
00167    if n=0 then [[3,1]] 
00168    elseif m=0 then [[1,2*n],[2,2*n],[3,1]] else
00169    [[1,2*n], [2,2*n], [3,m+1]] 
00170  else
00171    if n=0 then 
00172      if m=0 then [[k+binomial(k,2),1]] else 
00173      [[3,binomial(k,2)*m], [k+binomial(k,2),1]]
00174    elseif m=0 then [[1,n*k], [2,n*k], [k+binomial(k,2), 1]]
00175    else
00176  [[1, n * k], [2, n * k], [3, binomial(k,2) * m ], [k + binomial(k,2), 1]])$
00177 
00178