OKlibrary  0.2.1.6
Deficiency4.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.5.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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/MinimalUnsatisfiability/Deficiency2.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00024 
00025 /* Sequence of elements of MU(4) (as formal clause-sets, with standardised
00026    variables) according to [OK, XSZ, 2008], which realises the min-var-degree
00027    of 6. n >= 2 is the number of variables. */
00028 minvdegdef4(n) := block([FF : musatd2_fcs(n), S],
00029   S : {pos_c(n), neg_c(n), imp_c(1,n)},
00030   return(partial_gluing(FF,S,FF,S)))$
00031