OKlibrary  0.2.1.6
LinearAutarkies.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 18.7.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 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Numerical/Lisp/LinearProgramming.mac")$
00026 
00027 /* ********************
00028    * Basic operations *
00029    ********************
00030 */
00031 
00032 /* Tests whether phi is a simple linear autarky for the ordered
00033    clause-set F: */
00034 laut_paocs_p(phi,F) := if emptyp(phi) or emptyp(F) then true else block(
00035  [FF : cl2fcl(F), A, h : sm2hm({}), pv : [], nv : []],
00036   A : ocom2m(cl_var_ocom_ofcs(FF)),
00037   block([i:1], for v in FF[1] do (set_hm(h,v,i),i:i+1)),
00038   for x in phi do
00039     if x>0 then pv : endcons(ev_hm(h,x),pv) else nv : endcons(ev_hm(h,-x),nv),
00040   return(is(solve_lineq(A,pv,nv,
00041     listify(setdifference(setify(FF[1]),setify(append(pv,nv))))) # false)))$
00042 
00043 /* The set of all simple linear autarkies for an ordered clause-set: */
00044 all_laut_ocs(F) := subset(all_pass(var_ocs(F)), 
00045   lambda([phi],laut_paocs_p(phi,F)))$
00046 /* The simple linear autarky monoid of an ordered clause-set: */
00047 lautmon_ocs(F) := [all_laut_ocs(F), compo_pass, {}]$
00048 
00049 /* Searching for a linear autarky extending a given partial assignment
00050    (returning false if no extension is possible, and otherwise the
00051    extension): */
00052 extlaut_paocs_p(phi,F) := if emptyp(phi) or emptyp(F) then phi else block(
00053  [FF : cl2fcl(F), A, h : sm2hm({}), pv : [], nv : [], S],
00054   A : ocom2m(cl_var_ocom_ofcs(FF)),
00055   block([i:1], for v in FF[1] do (set_hm(h,v,i),i:i+1)),
00056   for x in phi do
00057     if x>0 then pv : endcons(ev_hm(h,x),pv) else nv : endcons(ev_hm(h,-x),nv),
00058   S : solve_lineq(A,pv,nv,[]),
00059   if S = false then return(false),
00060   block([i:1], for x in S do (
00061     if x>0 then phi:adjoin(FF[1][i],phi) 
00062     elseif x<0 then phi:adjoin(-FF[1][i],phi),
00063     i : i + 1
00064   )),
00065   return(phi))$
00066 
00067 /* Searching for a non-trivial autarky, returning false if there is
00068    none (i.e., if the ocs F is linearly lean): */
00069 find_linearautarky_ocs(F) := block([L : literals_v(var_ocs(F)), phi : false],
00070   for x in L unless phi # false do
00071     phi : extlaut_paocs_p({x},F),
00072   return(phi))$
00073