OKlibrary  0.2.1.6
Translations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.1.2008 (Swansea) */
00002 /* Copyright 2008 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 
00024 /* *********************************************************
00025    * Translation to SAT according to Liffiton and Sakallah *
00026    *********************************************************
00027 */
00028 
00029 /* Based on [Liffiton, Sakallah, 2008; Searching for Autarkies to Trim
00030    Unsatisfiable Clause Sets]. */
00031 
00032 /* "lsav" : Liffiton-Sakallah autarky variables */
00033 kill(lsavl,lsavv,lsavc)$
00034 declare(lsavl, noun, lsavv, noun, lsavc, noun)$
00035 declare(lsavl, posfun, lsavv, posfun, lsavc, posfun)$
00036 lsavl_var(v,s) := nounify(lsavl)(v,s)$ /* v an original variable, s in {-1,1} */
00037 lsavv_var(v) := nounify(lsavv)(v)$ /* v an original variable */
00038 lsavc_var(C) := nounify(lsavc)(C)$ /* C an original clause */
00039 
00040 /* Meaning:
00041  - lsavv(v) is true iff the autarky uses v
00042  - lsavc(C) is true iff the autarky satisfies C
00043  - lsavl(v,1) is the literal v, lsavl(v,-1) is the literal -v;
00044    lsavl(v,1) is true iff v is assigned and set to true,
00045    lsavl(v,-1) is true iff v is assigned and set to false.
00046 */
00047 
00048 /* Auxiliary function to translate literals */
00049 trans_lit_ls(x) := if x > 0 then lsavl_var(x,1) else lsavl_var(-x,-1)$
00050 
00051 /* Input a formal clause-set FF, returns a formal clause-set GG whose
00052    satisfying assignments correspond to the autarkies of FF.
00053    More precisely, the assigned original variables v are those
00054    with lsavv(c) true, and the satisfied clauses C are those
00055    with lsavc(C) true. */
00056 /* Prerequisite: FF does not use variables created by lsavl, lsavv
00057    or lsavc (a sufficient test is that 
00058    freeof(lsavl, FF) and freeof(lsavv, FF) and freeof(lsavc, FF)
00059    is true).
00060 */
00061 aut_sat_ls(FF) := block([V : listify(FF[1]), L : listify(FF[2])],
00062   return(
00063    [union(FF[1],
00064      setify(create_list(lsavl_var(v,-1),v,V)),
00065      setify(create_list(lsavl_var(v,+1),v,V)),
00066      setify(create_list(lsavv_var(v),v,V)),
00067      setify(create_list(lsavc_var(C),C,L))),
00068     union(
00069      /* if a clauses is satisfied, then also some of its literals: */
00070      setify(create_list(adjoin(-lsavc_var(C),map(trans_lit_ls,C)),C,L)),
00071      /* make lsavl_var(v,1) equivalent to (lsavv_var(v) & v): */
00072      family_sets_union(V, lambda([v], {
00073        {-lsavl_var(v,1),lsavv_var(v)},
00074        {-lsavl_var(v,1),v},
00075        {lsavl_var(v,1),-lsavv_var(v),-v}})),
00076      /* make lsavl_var(v,-1) equivalent to (lsavv_var(v) & -v): */
00077      family_sets_union(V, lambda([v], {
00078        {-lsavl_var(v,-1),lsavv_var(v)},
00079        {-lsavl_var(v,-1),-v},
00080        {lsavl_var(v,-1),-lsavv_var(v),v}})),
00081      /* if a variable in a clause is assigned, then the clause must
00082         be satisfied: */
00083      setify(create_list({-lsavv_var(var_l(x)),lsavc_var(C)}, C,L, x,listify(C))))]))$
00084 
00085 /* The corresponding translation FF -> GG such that FF is lean iff 
00086    GG is unsatisfiable (adding a clause which demands that at least
00087    one variable is used in the autarky). */
00088 lean_usat_ls(FF) := block([T : aut_sat_ls(FF)],
00089   [T[1], adjoin(map(lsavv,FF[1]),T[2])])$
00090 
00091 
00092 /* Translates an autarky phi for formal clause-set FF into a satisfying 
00093    assignment for aut_sat_ls(FF). */
00094 /* Prerequisite: phi uses only variables from FF. */
00095 trans_aut_sat_ls(phi,FF) := block(
00096  [VF : listify(FF[1]), L : listify(FF[2]), S : sat_pa(phi,FF[2]), V, OV],
00097  phi : restr_pa(phi, FF[1]),
00098  V : var_pa(phi), /* the variables in the autarky */
00099  OV : setdifference(FF[1], V), /* unassigned variables */
00100  return(union(phi,
00101   map(lambda([x],lsavl_var(var_l(x),sign_l(x))), phi),
00102   map(lambda([x],-lsavl_var(var_l(x),-sign_l(x))), phi),
00103   map(lambda([v],-lsavl_var(v,-1)), OV),
00104   map(lambda([v],-lsavl_var(v,+1)), OV),
00105   map(lsavv_var,V),
00106   comp_sl(map(lsavv_var,OV)),
00107   map(lsavc_var, S),
00108   map(lambda([C],-lsavc_var(C)), setdifference(FF[2],S)))))$
00109 /* For
00110  check_ls(phi,FF) := satisfyingpap(trans_aut_sat_ls(phi,FF),aut_sat_ls(FF)[2])
00111    we have check_ls(phi,FF) = true iff phi is an autarky for FF.
00112 */
00113 
00114 /* Given a satisfying partial assignment phi for aut_sat_ls(FF), returns
00115    the set of clauses of FF satisfied by phi. */
00116 itransc_aut_sat_ls(phi,FF) := 
00117   map(lambda([x],args(x)[1]),subset(phi,lambda([x],is(not atom(x) and op(x) = lsavc))))$
00118 /* Given a satisfying partial assignment phi for aut_sat_ls(FF), returns
00119    the corresponding autarky for FF. */
00120 itrans_aut_sat_ls(phi,FF) := block(
00121  [active_vars : subset(phi,lambda([x],is(not atom(x) and op(x) = lsavv)))],
00122   return(intersection(phi, literals_v(map(lambda([x],args(x)[1]),active_vars)))))$
00123 
00124 
00125 /* Find an autarky for a formal clause-set FF by translation to 
00126    SAT, and using a SAT solver returning a partial assignment (or "false");
00127    the autarky uses only variables from FF and is non-empty iff possible. */
00128 find_autarky_ls_fcs(FF,solver) := block([GG : lean_usat_ls(FF), phi],
00129   phi : solver(GG), 
00130   if phi=false then return({})
00131   else return(itrans_aut_sat_ls(phi,FF)))$
00132