OKlibrary  0.2.1.6
TableauAlgorithm.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.7.2008 (Swansea) */
00002 /* Copyright 2008, 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 
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00029 
00030 
00031 /* ***********************
00032    * The basic algorithm *
00033    ***********************
00034 */
00035 
00036 /* For a clause-list "F" and a list "obligations" of clauses from F,
00037    determine whether there exists an autarky for F satisfying all
00038    clauses from obligations. Returns either an autarky or "false".
00039 */
00040 /* The heuristics h inherits F and obligations (trivial heuristics are given
00041    by the functions lambda([],first(obligations)) and
00042    lambda([],last(obligations)). */
00043 find_aut_cl_tableau_cl(F,obligations,h) :=
00044   find_aut_cl_tableau_cl_rec(F,obligations,{})$
00045 /* The recursive version, inheriting h. */
00046 /* Prerequisites: phi has been applied to F and obligations. */
00047 find_aut_cl_tableau_cl_rec(F,obligations,phi) :=
00048   if emptyp(obligations) then phi
00049   elseif empty_element_p(obligations) then false else
00050   block([C : h(), found : false],
00051     for x in C while found=false do
00052       found : find_aut_cl_tableau_cl_rec(
00053         sublist(F,lambda([C],disjointp({-x,x},C))),
00054         append(apply_pa_cl({x},obligations), 
00055                map(lambda([C],disjoin(-x,C)),
00056                  sublist(F,lambda([C],elementp(-x,C))))),
00057         adjoin(x,phi)),
00058     return(found))$
00059 
00060 /* Heuristics: choose first smallest clause: */
00061 min_cllength_h_tableau() := first_smallest_lb_l(obligations,1)$
00062 
00063 /* The instance using as heuristics "first smallest clause": */
00064 find_aut_cl_tableau_fs_cl(F,obl) := find_aut_cl_tableau_cl(F,obl,min_cllength_h_tableau)$
00065 
00066 
00067 /* ************************************
00068    * Finding some non-trivial autarky *
00069    ************************************
00070 */
00071 
00072 /* Finding a pair [phi,lvar], where phi is non-trivial autarky if one exists
00073    ({} otherwise), and lvar a set of variables contained in the lean 
00074    kernel: */
00075 find_aut_tableau_cl(F,h) := if emptyp(F) then [{},{}] else
00076  block([found : false, phi, lvar : {}],
00077   unless found do block([C : first(F)],
00078     phi : find_aut_cl_tableau_cl(F,[C],h),
00079     if setp(phi) then found : true else block([V : var_c(C)],
00080       lvar : union(lvar,V),
00081       apply_sv_ip_cl(V,'F),
00082       F : sublist(F,lambda([C], not emptyp(C))),
00083       if emptyp(F) then found : true
00084   )),
00085   if not setp(phi) then phi : {},
00086   return([phi,lvar]))$
00087 
00088 
00089 /* *****************************
00090    * Computing the lean kernel *
00091    *****************************
00092 */
00093 
00094 /* Now phi is an autarky yielding a maximal autark subset, and lvar is
00095    the set of all variables in the lean kernel: */
00096 find_autlvar_tableau_cl(F,h) := if emptyp(F) then [{},{}] else
00097  block([maxphi : {}, phi, lvar : {}],
00098   unless emptyp(F) do block([C : first(F)],
00099     phi : find_aut_cl_tableau_cl(F,[C],h),
00100     if setp(phi) then (
00101       apply_pa_ip_cl(phi,'F),
00102       maxphi : union(maxphi,phi)
00103     )
00104     else block([V : var_c(C)],
00105       lvar : union(lvar,V),
00106       apply_sv_ip_cl(V,'F),
00107       F : sublist(F,lambda([C], not emptyp(C))))
00108   ),
00109   return([maxphi,lvar]))$
00110 
00111 /* Computing a pair [L,phi], where L is the sublist of F containing the clauses
00112    from the lean kernel, while phi is an autarky for F certifying the lean
00113    kernel: */
00114 lean_kernel_tableau_cl(F,h) := block([phi,lvar,L],
00115   [phi,lvar] : find_autlvar_tableau_cl(F,h),
00116   L : union(phi,comp_sl(phi)),
00117   [sublist(F,lambda([C],disjointp(C,L))), phi])$
00118     
00119 
00120 /* *************
00121    * Instances *
00122    *************
00123 */
00124 
00125 /* The instances using as heuristics "first smallest clause": */
00126 find_aut_tableau_fs_cl(F) := find_aut_tableau_cl(F,min_cllength_h_tableau)$
00127 find_autlvar_tableau_fs_cl(F) := find_autkvar_tableau_cl(F,min_cllength_h_tableau)$
00128 lean_kernel_tableau_fs_cl(F) := lean_kernel_tableau_cl(F,min_cllength_h_tableau)$
00129 lean_kernel_tableau_fs_cs(F) := block([L:lean_kernel_tableau_fs_cl(cs2cl(F))],
00130  [cl2cs(first(L)),second(L)])$
00131 
00132