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 (