OKlibrary  0.2.1.6
TseitinTranslation.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.12.2010 (Swansea) */
00002 /* Copyright 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 
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00026 
00027 
00028 /* ****************************
00029    * Translating DNF into CNF *
00030    ****************************
00031 */
00032 
00033 /* The natural CNF-representation of DNF-clause-set F via new
00034    variables, directly exploiting the Tseitin translation.
00035 */
00036 kill(dts)$ /* "dual Tseitin" */
00037 declare(dts, noun)$
00038 declare(dts, posfun)$
00039 dts_var(v) := nounify(dts)(v)$
00040 dtsext_var(v,d) := nounify(dts)(v,d)$
00041 
00042 /* The variables of dualts_fcl(FF) are:
00043     - the variables FF[1] from FF
00044     - plus the dts(i) for i from 1 to c = length(FF[2]) = number of clauses in
00045       FF.
00046    The clauses of dualts_fcl(FF) are given by the clauses C of FF with index i
00047    as the canonical translations of (C <-> dts(i)), plus the disjunction
00048    of all the dts(i).
00049    Thus we obtain per C one clause of length |C|+1, |C| clauses of length 2,
00050    and finally one clause of length |FF|.
00051    The order is that we first get all those mirror-clauses and then all those
00052    binary clauses (with the natural order on them, given by the order of
00053    clauses in FF and the order of the literals in C in FF), and finally
00054    the long clause.
00055 */
00056 /* TODO: bad order: this should be an extension of the reduced translation,
00057    and thus "those mirror-clauses" should come last. The plus-form has then
00058    also to be updated accordingly.
00059    The implementation perhaps should just use rcantrans_fcl2fcl(FF).
00060 */
00061 /* TODO: rename to cantrans_fcl2fcl. */
00062 dualts_fcl(FF) := block([c : length(FF[2]), NV, G1, G2],
00063   NV : create_list(dts_var(i),i,1,c),
00064   G1 : map(lambda([C,i], adjoin(dts_var(i),comp_sl(C))), 
00065         FF[2], create_list(i,i,1,c)),
00066   G2 : lappend(map(lambda([C,i], create_list({-dts_var(i),x},x,listify(C))),
00067         FF[2], create_list(i,i,1,c))),
00068   [append(FF[1],NV), append(G1,G2,[setify(NV)])])$
00069 dualts_cs(F) := fcl2cs(dualts_fcl(cs2fcl(F)))$
00070 
00071 
00072 /* The reduced canonical translation, using only the direction (C <- dts(i))
00073    from dualts_fcl(FF):
00074 */
00075 rcantrans_fcl2fcl(FF) := block([c : length(FF[2]), NV, G1],
00076   NV : create_list(dts_var(i),i,1,c),
00077   G1 : lappend(map(lambda([C,i], create_list({-dts_var(i),x},x,listify(C))),
00078         FF[2], create_list(i,i,1,c))),
00079   [append(FF[1],NV), append(G1,[setify(NV)])])$
00080 rcantrans_cs2cs(F) := fcl2cs(rcantrans_fcl2fcl(cs2fcl(F)))$
00081 
00082 
00083 /* dualtsplus_fcl(FF) has the same variables as dualts_fcl(FF).
00084    The clauses of dualts_fcl(FF) are those of dualts_fcl(FF), plus
00085    (x <-> D) for every literal x occurring in FF[2], where D is the
00086    conjunction of -dts(i) for those i with -x in C_i.
00087    Thus we obtain additionally one clause of length literal_degree_cs(FF[2],-x)
00088    for every literal x in FF[2]. Currently these new clauses are placed just
00089    before the final long clause of dualts_fcl(FF).
00090 */
00091 /* TODO: bad order: it should extend dualts_fcl(FF); and also the measures are
00092    needed.
00093 */
00094 dualtsplus_fcl(FF) := block([c : length(FF[2]), NV, G1, G2, G3],
00095   NV : create_list(dts_var(i),i,1,c),
00096   G1 : map(lambda([C,i], adjoin(dts_var(i),comp_sl(C))), 
00097         FF[2], create_list(i,i,1,c)),
00098   G2 : lappend(map(lambda([C,i], create_list({-dts_var(i),x},x,listify(C))),
00099         FF[2], create_list(i,i,1,c))),
00100   G3 : map(
00101          lambda([l], setify(
00102              cons(l, map(dts_var,
00103                  sublist_indices(FF[2], lambda([C], elementp(-l,C))))))),
00104          listify(literals_v(
00105              sublist(FF[1], lambda([v], elementp(v,var_cs(FF[2]))))))),
00106   [append(FF[1],NV), append(G1,G2,G3,[setify(NV)])])$
00107 
00108 
00109 /* The variation which uses value d (for "distinguish") as second parameter
00110    of dts_var (producing the same formal clause-list otherwise; this is
00111    needed to have distinct auxiliary variables for different applications
00112    of dualts_fcl):
00113 */
00114 dualtsext_fcl(FF,d) := block([c : length(FF[2]), NV, G1, G2],
00115   NV : create_list(dtsext_var(i,d),i,1,c),
00116   G1 : map(lambda([C,i], adjoin(dtsext_var(i,d),comp_sl(C))), 
00117         FF[2], create_list(i,i,1,c)),
00118   G2 : lappend(map(lambda([C,i], create_list({-dtsext_var(i,d),x},x,listify(C))),
00119         FF[2], create_list(i,i,1,c))),
00120   [append(FF[1],NV), append(G1,G2,[setify(NV)])])$
00121 
00122 
00123 /* Measures */
00124 
00125 nvar_dualts(FF) := length(FF[1])+length(FF[2])$
00126 /* Numerically, given the number of variables and clauses: */
00127 nvar_dualts_num(n,c) := n+c$
00128 /* For a full clause-set with n variables and c clauses: */
00129 nvar_full_dualts(n,c) := n+c$
00130 
00131 ncl_dualts(FF) := nlitocc_fcl(FF) + ncl_fcl(FF) + 1$
00132 /* Numerically, given the number of clauses and literal-occurrences: */
00133 ncl_dualts_num(c,l) := l + c + 1$
00134 /* For a full clause-set with n variables and c clauses: */
00135 ncl_full_dualts(n,c) := (n * c) + c + 1$
00136 
00137 ncl_list_dualts(FF) := sort(block(
00138   [ncl_list_FF : ncl_list_fcl(FF), ncl_h,
00139    n : nvar_fcl(FF), c : ncl_fcl(FF), nlitocc : nlitocc_fcl(FF),
00140    ncl_unit, ncl_cm1, other_cl],
00141   ncl_h : osm2hm(ncl_list_FF),
00142   ncl_unit : ev_hm_d(ncl_h,1,0), ncl_cm1 : ev_hm_d(ncl_h,c-1,0),
00143   other_cl : sublist(ncl_list_FF, lambda([P], is(P[1] # 1) and is(P[1] # c-1))),
00144   other_cl : map(lambda([a], [a[1]+1,a[2]]), other_cl),
00145   if c = 0 then [[0,1]]
00146   else if n = 0 then [[1,2]]
00147   else if c = 2 then append([[2,nlitocc+ncl_unit+1]],other_cl)
00148   else append([[2,nlitocc+ncl_unit],[c,1+ncl_cm1]],other_cl)))$
00149 /* We count the following clauses:
00150      - a binary clause for every literal occurrence L in FF, representing that
00151        dts(i) => L.
00152      - a (length(C)+1)-ary clause for every clause C in FF, representing that
00153        C => dts(i).
00154      - a clause specifying that at least one of the clauses in the input must
00155        be satisfied for the result to be satisfied, and therefore, one of the
00156        dts(i) variables must be set to true. This yields a single clause of
00157        length ncl_fcl(FF).
00158        
00159    Note that unit-clauses in the input will result in more binary clauses
00160    being counted than there are literal occurrences (as length(C)+1 where
00161    C is a unit-clause yields a binary clause in the output of dualts_fcl).
00162 */
00163 /* For a full clause-set with n variables and c clauses: */
00164 ncl_list_full_dualts(n,c) := sort(
00165   if c = 0 then [[0,1]]
00166   else if n = 0 then [[1,2]]
00167   else if n = 1 and c = 2 then [[2,2*c+1]]
00168   else if n = 1 and c # 2 then [[2,2*c],[c,1]]
00169   else if n+1 = c then [[2,n*c],[n+1,c+1]]
00170   else if c = 2 then [[2,n*c+1],[n+1,c]]
00171   else [[2,n*c],[c,1],[n+1,c]])$
00172 
00173    
00174 
00175