OKlibrary  0.2.1.6
Deficiency3.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(3) (as formal clause-sets, with standardised
00026    variables) according to [OK, XSZ, 2008], which realises the min-var-degree
00027    of 5. n >= 2 is the number of variables. */
00028 minvdegdef3(n) := block([FF : musatd2_fcs(n),F,V, P, N, C, S, F2, S2],
00029   V : FF[1],
00030   F : FF[2],
00031   P : pos_c(n),
00032   N : neg_c(n),
00033   C : imp_c(1,n),
00034   S : {P,N,C},
00035   F2 : adjoin({-1},setdifference(F,{N,C})),
00036   S2 : {P,{-1}},
00037   return(partial_gluing(FF,S,[V,F2],S2)))$
00038