OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 28.3.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012, 2013 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/Backtracking/DLL_solvers.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/InverseSingularDP.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/DeficiencyOne.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00030 
00031 
00032 kill(f)$
00033 
00034 
00035 /* *************************
00036    * Deciding irredundancy *
00037    *************************
00038 */
00039 
00040 okltest_impliesp_fcs(f) := block([S : dll_simplest_trivial1],
00041   assert(f([{},{}],{1},S) = false),
00042   assert(f([{},{{}}],{1},S) = true),
00043   assert(f([{},{{}}],{},S) = true),
00044   assert(f([{1,2},{{1}}],{1,2},S) = true),
00045   true)$
00046 
00047 okltest_impliesp_cs(f) := block([S : dll_simplest_trivial1],
00048   assert(f({},{},S) = false),
00049   assert(f({{}},{},S) = true),
00050   /* XXX */
00051   true)$
00052 
00053 okltest_min_unsat_bydef(f) := block([S : dll_simplest_trivial1],
00054   assert(f([{},{}],S) = false),
00055   assert(f([{},{{}}],S) = true),
00056   assert(f([{1},{{1}}],S) = false),
00057   assert(f([{1},{{1},{}}],S) = false),
00058   assert(f([{1},{{}}],S) = true),
00059   assert(f([{1},{{1},{-1}}],S) = true),
00060   for n : 0 thru 3 do
00061     assert(f(full_fcs(n),S) = true),
00062   if oklib_test_level = 0 then return(true),
00063   for n : 0 thru 3 do
00064     assert(f(weak_php_fcs(n+1,n),S) = true),
00065   true)$
00066 
00067 okltest_irredundant_bydef(f) := block([Sol : dll_simplest_trivial1],
00068   assert(f([{},{}],Sol) = true),
00069   assert(f([{1},{{1}}],Sol) = true),
00070   assert(f([{1,2},{{1},{1,2}}],Sol) = false),
00071   if oklib_test_level = 0 then return(true),
00072   block([oklib_test_level : oklib_test_level-1],
00073     okltest_min_unsat_bydef(buildq([f],lambda([FF,Sol], is(not Sol(FF) and f(FF,Sol)))))),
00074   true)$
00075 
00076 
00077 /* *****************************
00078    * Classification of clauses *
00079    *****************************
00080 */
00081 
00082 okltest_all_irrcl_bydef(f) := block([S : dll_simplest_trivial1],
00083   assert(f([{},{}],S) = {}),
00084   assert(f([{},{{}}],S) = {{}}),
00085   assert(f([{1},{{}}],S) = {{}}),
00086   assert(f([{1},{{1}}],S) = {{1}}),
00087   assert(f([{1},{{1},{-1}}],S) = {{1},{-1}}),
00088   assert(f([{1},{{1},{}}],S) = {{}}),
00089   assert(f([{1},{{1},{-1},{}}],S) = {}),
00090   assert(f([{1,2},{{1},{1,2}}],S) = {{1}}),
00091   true)$
00092 
00093 
00094 /* **************************************
00095    * Saturated minimal unsatisfiability *
00096    **************************************
00097 */
00098 
00099 okltest_saturated_min_unsat_bydef(f) := block([S : dll_simplest_trivial1],
00100   assert(f([{},{}],S) = false),
00101   assert(f([{},{{}}],S) = true),
00102   assert(f([{1},{{}}],S) = true),
00103   assert(f([{1},{{1}}],S) = false),
00104   assert(f([{1},{{1},{-1}}],S) = true),
00105   assert(f([{1,2},{{}}],S) = true),
00106   assert(f([{1,2},{{1,2},{-1},{-2}}],S) = false),
00107   assert(f([{1,2},{{1,2},{-1,2},{-2}}],S) = true),
00108   assert(f([{1,2},{{1,2},{-1},{-2,1}}],S) = true),
00109   for n : 0 thru if oklib_test_level=0 then 3 else 5 do
00110     assert(f(full_fcs(n),S) = true),
00111   for k : 0 thru if oklib_test_level=0 then 3 else 4 do
00112     assert(f(cs2fcs(uniform_usat_hitting_min(k)),S) = true),
00113   block([FF : full_fcs(2)],
00114     assert(basic_inverse_singulardp_fcs(FF,setdifference(FF[2],{{1,2}}),1,1) = true),
00115     assert(f(FF,S) = false)),
00116   true)$
00117 
00118 okltest_non_saturating_pas_bydef(f) := block([S : dll_simplest_trivial1],
00119   assert(f([{},{}],S) = {{}}),
00120   assert(f([{},{{}}],S) = {}),
00121   assert(f([{1},{{}}],S) = {}),
00122   assert(f([{1},{{1}}],S) = {{},{1}}),
00123   assert(f([{1},{{1},{-1}}],S) = {}),
00124   assert(f([{1,2},{{}}],S) = {}),
00125   assert(f([{1,2},{{1,2},{-1},{-2}}],S) = {{1},{2}}),
00126   assert(f([{1,2},{{1,2},{-1,2},{-2}}],S) = {}),
00127   assert(f([{1,2},{{1,2},{-1},{-2,1}}],S) = {}),
00128   true)$
00129 
00130 
00131 /* *************************************
00132    * Marginal minimal unsatisfiability *
00133    *************************************
00134 */
00135 
00136 okltest_marginal_min_unsat_bydef_fcs(f) := (
00137   assert(f([{},{}]) = false),
00138   assert(f([{},{{}}]) = true),
00139   assert(f([{1},{{1}}]) = false),
00140   assert(f([{1},{{},{1}}]) = false),
00141   assert(f([{1},{{1},{-1}}]) = true),
00142   assert(f([{1,2,3},{{1},{-1,2},{-1,-2,3},{-1,-2,-3}}]) = false),
00143   assert(f([{1,2,3},{{1},{-1,2},{-2,3},{-3}}]) = true),
00144   for n : 0 thru if oklib_test_level=0 then 3 else 5 do
00145     assert(f(full_fcs(n)) = true),
00146   for k : 0 thru if oklib_test_level=0 then 3 else 5 do
00147     assert(f(cs2fcs(marginal_musat1(k))) = true),
00148   true)$
00149 
00150