OKlibrary  0.2.1.6
Deficiency2.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.5.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2012 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/MinimalUnsatisfiability/tests/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency2.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00029 
00030 kill(f)$
00031 
00032 
00033 /* *********************************************************************
00034    * The saturated minimally unsatisfiable clause-sets of deficiency 2 *
00035    *********************************************************************
00036 */
00037 
00038 /* Testing the characteristic properties of non-singular minimally 
00039    unsatisfiable formal clause-sets of deficiency 2: */
00040 charprop_nsmusatd2(FF,n) := 
00041   nvar_fcs(FF) = n and
00042   FF[1] = setn(n) and
00043   deficiency_fcs(FF) = 2 and
00044   min_unsat_bydef(FF,lambda([GG],dll_rk_trivial1(GG,1))) and
00045   literal_degrees_list_fcs(FF) = [[2,2*n]]$
00046 
00047 okltest_charprop_nsmusatd2(f) := (
00048   assert(f([{},{}],0) = false),
00049   assert(f([{},{{}}],1) = false),
00050   assert(f([{1,2},{{},{1},{2},{-1,-2}}],2) = false),
00051   assert(f([{1,2,3},{{-1,2},{-1,-2},{1,2,-3},{1,2,3},{1,-2}}],3) = false),
00052   assert(f(full_fcs(2),2) = true),
00053   assert(f(full_fcs(2),3) = false),
00054   assert(f([{1,2,3},{{-1,-2,-3},{1,2,3},{-1,2},{-2,3},{-3,1}}],3) = true),
00055   true)$
00056 
00057 okltest_musatd2_cl(f) := (
00058   assert(f(2) = [{1,2},{-1,-2},{-1,2},{-2,1}]),
00059   assert(f(3) = [{1,2,3},{-1,-2,-3},{-1,2},{-2,3},{-3,1}]),
00060   assert(f(4) = [{1,2,3,4},{-1,-2,-3,-4},{-1,2},{-2,3},{-3,4},{-4,1}]),
00061   true)$
00062 
00063 okltest_musatd2_fcs(f) := (
00064   for n : 2 thru 5 do block([FF : f(n)],
00065     assert(charprop_nsmusatd2(FF,n) = true),
00066     assert(elementp(setn(n),FF[2]) = true)
00067   ),
00068   true)$
00069 
00070 okltest_nvar_musatd2(f) := (
00071   for n : 2 thru 7 do block([nc : f(n)],
00072     assert(nc = nvar_fcs(musatd2_fcs(n))),
00073     assert(nc = nvar_fcl(musatd2_fcl(n)))
00074   ),
00075   true)$
00076 
00077 okltest_ncl_musatd2(f) := (
00078   for n : 2 thru 7 do block([c : f(n)],
00079     assert(c = ncl_fcs(musatd2_fcs(n))),
00080     assert(c = ncl_fcl(musatd2_fcl(n)))
00081   ),
00082   true)$
00083 
00084 okltest_ncl_list_musatd2(f) := (
00085   for n : 2 thru 7 do block([cl : f(n)],
00086     assert(cl = ncl_list_fcs(musatd2_fcs(n))),
00087     assert(cl = ncl_list_fcl(musatd2_fcl(n)))
00088   ),
00089   true)$
00090 
00091 okltest_nlitocc_musatd2(f) := (
00092   for n : 2 thru 7 do block([l : f(n)],
00093     assert(l = nlitocc_fcs(musatd2_fcs(n))),
00094     assert(l = nlitocc_fcl(musatd2_fcl(n)))
00095   ),
00096   true)$
00097 
00098 
00099 /* *****************************************************
00100    * Unsatisfiable hitting clause-sets of deficiency 2 *
00101    *****************************************************
00102 */
00103 
00104 okltest_hittingtype_d2_cs(f) := (
00105   assert(f({}) = false),
00106   assert(f({{}}) = false),
00107   assert(f({{1},{-1}}) = false),
00108   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}}) = 2),
00109   assert(f({{2,3},{-2,3},{2,-3},{-2,-3}}) = 2),
00110   assert(f({{1,2,3},{-1,-2,-3},{-1,2},{-2,3},{-3,1}}) = 3),
00111   assert(f({{1,-2,3},{-1,2,-3},{-1,-2},{2,3},{-3,1}}) = 3),
00112   /* XXX */
00113   true)$
00114 
00115 okltest_all_reps_uhitd2_t_fcs(f) := (
00116   for t : 2 thru 3 do
00117    for n : -1 thru 1 do
00118      assert(f(t,n) = {}),
00119   assert(f(3,2) = {}),
00120   assert(f(2,2) = {musatd2_fcs(2)}),
00121   assert(f(3,3) = {musatd2_fcs(3)}),
00122   assert(f(2,3) = { [{1,2,3},{{1,2},{1,-2},{-1,2},{-1,-2,-3},{-1,-2,3}}], [{1,2,3},{{1,2},{-1,2},{1,-2,-3},{-1,-2,-3},{-2,3}}], [{1,2,3},{{1,2,-3},{1,-2,-3},{-1,2,-3},{-1,-2,-3},{3}}] }),
00123   /* XXX */
00124   true)$
00125 
00126 okltest_all_reps_uhitd2_fcs(f) := (
00127  for n : -1 thru 1 do
00128    assert(f(n) = {}),
00129   assert(f(2) = {musatd2_fcs(2)}),
00130   assert(f(3) = {musatd2_fcs(3), [{1,2,3},{{1,2},{1,-2},{-1,2},{-1,-2,-3},{-1,-2,3}}], [{1,2,3},{{1,2},{-1,2},{1,-2,-3},{-1,-2,-3},{-2,3}}], [{1,2,3},{{1,2,-3},{1,-2,-3},{-1,2,-3},{-1,-2,-3},{3}}] }),
00131   /* XXX */
00132   true)$
00133 
00134 okltest_all_uhitd2_fcs(f) := (
00135  for n : -1 thru 1 do
00136    assert(f(n) = {}),
00137   assert(f(2) = {musatd2_fcs(2)}),
00138 
00139   /* XXX */
00140   true)$
00141 
00142