OKlibrary  0.2.1.6
DeficiencyOne.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 20.2.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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/Conflicts.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Basic.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/DeficiencyOne.mac")$
00028 
00029 kill(f)$
00030 
00031 /* ************************
00032    * Tree representations *
00033    ************************
00034 */
00035 
00036 /* ****************************
00037    * Generating all instances *
00038    ****************************
00039 */
00040 
00041 okltest_all_smusat1_cs(f) := (
00042   assert(f(0) = [{{}}]),
00043   assert(f(1) = [ {{1},{-1}} ]),
00044   assert(f(2) = [ {{1},{-1,2},{-1,-2}}, {{2},{-2,1},{-2,-1}}, {{-1},{1,2},{1,-2}}, {{-2},{2,1},{2,-1}} ]),
00045   /* XXX */
00046   true)$
00047 
00048 okltest_num_all_smusat1(f) := (
00049   for n : 0 thru if oklib_test_level=0 then 3 else 5 do
00050     assert(f(n) = length(all_smusat1_cs(n))),
00051   true)$
00052 
00053 
00054 /* ******************************************************
00055    * Heuristical approach: removing literal occurrences *
00056    * to achieve a given maximal variable degree         *
00057    ******************************************************
00058 */
00059 
00060 okltest_remlitocc_greedy(f) := block(
00061   assert(f({},inf,0) = [{},minf]),
00062   assert(f({{}},0,0) = [{{}},minf]),
00063   assert(f({{1},{-1}},1,1) = [false,inf]),
00064   assert(f({{1},{-1}},1,2) = [{{1},{-1}},2]),
00065   for n : 1 thru 3 do (
00066     F : f(uniform_usat_hitting_min(n),1,2)[1],
00067     assert(nvar_cs(F) = 2^n - 1),
00068     assert(deficiency_cs(F) = 1)),
00069     assert(is_tree(g2mg(cg_cs(F))) = true),
00070   true)$
00071 
00072 okltest_marginal_musat1(f) := block(
00073   assert(f(0) = {{}}),
00074   for k : 1 thru 4 do block([F : f(k)],
00075     assert(length(F) = 2^k),
00076     assert(max_variable_degree_cs(F) = 2),
00077     assert(graphiccsp(F) = true),
00078     assert(is_tree(g2mg(cg_cs(F))) = true)),
00079   true)$
00080