OKlibrary  0.2.1.6
Transformations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.9.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/Statistics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Transformations.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Generators.mac")$
00028 
00029 
00030 kill(f)$
00031 
00032 /* **************************************************
00033    * Translated minimally unsatisfiable clause-sets *
00034    **************************************************
00035 */
00036 
00037 okltest_usat_musat_repo_sat() := [
00038  [{},{}],
00039  [{1},{{-1}}],
00040  [{1},{{1}}],
00041  [{1,2},{{1},{2}}]
00042 ]$
00043 
00044 okltest_usat_musat_repo_usat() := [
00045  [{},{{}}],
00046  [{1},{{1},{-1}}],
00047  [{1},{{},{1}}],
00048  [{1},{{},{1},{-1}}]
00049 ]$
00050 
00051 okltest_n_var_usat_musat(f) := block(
00052   for FF in okltest_usat_musat_repo_sat() do
00053     assert(f(FF) = nvar_f(usat_musat(FF))),
00054   for FF in okltest_usat_musat_repo_Usat() do
00055     assert(f(FF) = nvar_f(usat_musat(FF))),
00056   for n : 0 thru 3 do block([FF : full_fcs(n)],
00057     assert(f(FF) = nvar_f(usat_musat(FF)))),
00058   true)$
00059 
00060 okltest_n_cl_usat_musat(f) := block(
00061   for FF in okltest_usat_musat_repo_sat() do
00062     assert(f(FF) = ncl_fcs(usat_musat(FF))),
00063   for FF in okltest_usat_musat_repo_usat() do
00064     assert(f(FF) = ncl_fcs(usat_musat(FF))),
00065   for n : 0 thru 3 do block([FF : full_fcs(n)],
00066     assert(f(FF) = ncl_fcs(usat_musat(FF)))),
00067   true)$
00068 
00069 okltest_deficiency_usat_musat(f) := block(
00070   for FF in okltest_usat_musat_repo_sat() do
00071     assert(f(FF) = deficiency_fcs(usat_musat(FF))),
00072   for FF in okltest_usat_musat_repo_usat() do
00073     assert(f(FF) = deficiency_fcs(usat_musat(FF))),
00074   for n : 0 thru 3 do block([FF : full_fcs(n)],
00075     assert(f(FF) = deficiency_fcs(usat_musat(FF)))),
00076   true)$
00077 
00078 okltest_ncl_list_usat_musat(f) := block(
00079   for FF in okltest_usat_musat_repo_sat() do
00080     assert(f(FF) = ncl_list_fcs(usat_musat(FF))),
00081   for FF in okltest_usat_musat_repo_Usat() do
00082     assert(f(FF) = ncl_list_fcs(usat_musat(FF))),
00083   for n : 0 thru 3 do block([FF : full_fcs(n)],
00084     assert(f(FF) = ncl_list_fcs(usat_musat(FF)))),
00085   true)$
00086 
00087 okltest_n_var_sat_musat(f) := block(
00088   for FF in okltest_sat_musat_repo_sat() do
00089     assert(f(FF) = nvar_f(sat_musat(FF))),
00090   for FF in okltest_sat_musat_repo_Usat() do
00091     assert(f(FF) = nvar_f(sat_musat(FF))),
00092   for n : 0 thru 3 do block([FF : full_fcs(n)],
00093     assert(f(FF) = nvar_f(sat_musat(FF)))),
00094   true)$
00095 
00096 okltest_n_cl_sat_musat(f) := block(
00097   for FF in okltest_sat_musat_repo_sat() do
00098     assert(f(FF) = ncl_fcs(sat_musat(FF))),
00099   for FF in okltest_sat_musat_repo_usat() do
00100     assert(f(FF) = ncl_fcs(sat_musat(FF))),
00101   for n : 0 thru 3 do block([FF : full_fcs(n)],
00102     assert(f(FF) = ncl_fcs(sat_musat(FF)))),
00103   true)$
00104 
00105 okltest_deficiency_sat_musat(f) := block(
00106   for FF in okltest_sat_musat_repo_sat() do
00107     assert(f(FF) = deficiency_fcs(sat_musat(FF))),
00108   for FF in okltest_sat_musat_repo_usat() do
00109     assert(f(FF) = deficiency_fcs(sat_musat(FF))),
00110   for n : 0 thru 3 do block([FF : full_fcs(n)],
00111     assert(f(FF) = deficiency_fcs(sat_musat(FF)))),
00112   true)$
00113 
00114 okltest_ncl_list_sat_musat(f) := block(
00115   for FF in okltest_sat_musat_repo_sat() do
00116     assert(f(FF) = ncl_list_fcs(sat_musat(FF))),
00117   for FF in okltest_sat_musat_repo_Usat() do
00118     assert(f(FF) = ncl_list_fcs(sat_musat(FF))),
00119   for n : 0 thru 3 do block([FF : full_fcs(n)],
00120     assert(f(FF) = ncl_list_fcs(sat_musat(FF)))),
00121   true)$
00122 
00123 
00124 /* ********************************************************
00125    * Max-Clique translated to "SHORT RES" and "SMALL MUS" *
00126    ********************************************************
00127 */
00128 
00129 okltest_new_k(f) := (
00130   assert(f(0) = 0),
00131   assert(f(1) = 2),
00132   assert(f(2) = 5),
00133   assert(f(3) = 9),
00134   assert(f(4) = 14),
00135   true)$
00136 
00137 okltest_maxclique_start(f) := (
00138   assert(f(0) = {{}}),
00139   assert(f(1) = {{srfswx(1)}}),
00140   assert(f(2) = {{srfswx(1),srfswx(2),srfswy(1,2)}}),
00141   assert(f(3) = {{srfswx(1),srfswx(2),srfswx(3),srfswy(1,2),srfswy(1,3),srfswy(2,3)}}),
00142   true)$
00143 
00144 okltest_maxclique_edges(f) := (
00145 
00146   true)$
00147 
00148 okltest_maxclique_cleanup(f) := (
00149 
00150   true)$
00151 
00152 okltest_maxclique_mures_fcs(f) := (
00153 
00154   true)$
00155 
00156 maxclique_mures_testcases : append([
00157 [[{},{}],0],
00158 [[{},{}],1],
00159 [[{},{}],2],
00160 [[{},{}],3],
00161 [[{1},{}],0],
00162 [[{1},{}],1],
00163 [[{1},{}],2],
00164 [[{1},{}],3],
00165 [[{1,2},{{1,2}}],0],
00166 [[{1,2},{{1,2}}],1],
00167 [[{1,2},{{1,2}}],2],
00168 [[{1,2},{{1,2}}],3]
00169 ],
00170 create_list([complete_stdg(n),n],n,1,5),
00171 create_list([complete_stdg(n),n],n,1,6),
00172 create_list([pathgraph_g(n),3],n,1,5),
00173 create_list([cyclegraph_gl(n),3],n,3,5)
00174 )$
00175 
00176 okltest_nvar_maxclique_mures_fcs(f) := (
00177   for T in maxclique_mures_testcases do
00178     assert(apply(f,T) = nvar_fcs(apply(maxclique_mures_fcs,T))),
00179   true)$
00180 
00181 okltest_ncl_list_maxclique_mures_fcs(f) := block(
00182   for T in maxclique_mures_testcases do
00183     assert(apply(f,T) = ncl_list_fcs(apply(maxclique_mures_fcs,T))),
00184   true)$
00185