OKlibrary  0.2.1.6
LargestAutarky.mac
Go to the documentation of this file.
00001 /* Matthew Lewsey, 17.5.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/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 
00024 /* Given a partial assignment phi and clause-set F, compute the largest
00025    autarky for F which is contained in phi. */
00026 largest_aut_cs(phi,F) := if emptyp(phi) then {} else block(
00027  [analyse_phi, FC],
00028   F : disjoin({},F),
00029   analyse_phi : analyse_pa(phi,F),
00030   FC : union(analyse_phi[2], analyse_phi[4]),
00031   if not emptyp(FC) then
00032     return(largest_aut_cs(restr_c_pa(phi,var_cs(FC)),F))
00033   else return(phi))$
00034