OKlibrary  0.2.1.6
MinVarDegrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 21.5.2011 (London) */
00002 /* Copyright 2011 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 
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/MinVarDegrees.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00030 
00031 /* For k >= 1 standardised formal lean clause-sets of deficiency k with
00032    minimal variable-degree nonmersenne(k):
00033 */
00034 extremal_lean_mvdd_fcs(k) := block([l : nonmersenne_level(k), F, d, C],
00035   F : full_cs(l),
00036   d : 2^l-l,
00037   C : choose_element(F),
00038   while d # k do (
00039     d : d+1, l : l+1,
00040     F : add_element(l,F),
00041     F : union(F,{{-l},C}),
00042     C : adjoin(l,C)
00043   ),
00044   [setn(l),F])$
00045