OKlibrary  0.2.1.6
Colouring.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 22.7.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Hypergraphs/Lisp/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Generators/Generators.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")$
00027 
00028 
00029 kill(f)$
00030 
00031 
00032 /* *******************************
00033    * Translations to boolean SAT *
00034    *******************************
00035 */
00036 
00037 okltest_colv_string(f) := (
00038   assert(f(colv({})) = "E "),
00039   assert(f(-colv({})) = "-E "),
00040   assert(f(colv({1})) = "1 "),
00041   assert(f(-colv({1})) = "-1 "),
00042   assert(f(colv({1,2})) = "1S2 "),
00043   assert(f(-colv({1,2})) = "-1S2 "),
00044   assert(f(colv({1,2,3,4})) = "1S2S3S4 "),
00045   true)$
00046 
00047 okltest_tcol2sat_hg2fcs(f) := (
00048   assert(f([{},{}]) = [{},{}]),
00049   assert(f([{},{{}}]) = [{},{{}}]),
00050   assert(f([{1},{{},{1}}]) = [{colv(1)},{{},{colv(1)},{-colv(1)}}]),
00051   assert(f([{1,2},{{1},{1,2}}]) = [{colv(1),colv(2)},{{colv(1)},{colv(1),colv(2)},{-colv(1)},{-colv(1),-colv(2)}}]),
00052   true)$
00053 
00054 okltest_tcol2sat_stdhg2stdfcs(f) := (
00055   assert(f([{},{}]) = [{},{}]),
00056   assert(f([{},{{}}]) = [{},{{}}]),
00057   assert(f([{1},{{},{1}}]) = [{1},{{},{1},{-1}}]),
00058   assert(f([{1,2},{{1},{1,2}}]) = [{1,2},{{1},{1,2},{-1},{-1,-2}}]),
00059   true)$
00060 
00061 okltest_tcol2sat_ohg2fcl(f) := (
00062   assert(f([[],[]]) = [[],[]]),
00063   assert(f([[],[{}]]) = [[],[{},{}]]),
00064   assert(f([[1],[{},{1}]]) = [[colv(1)],[{},{colv(1)},{},{-colv(1)}]]),
00065   assert(f([[2,1],[{1},{1,2}]]) = [[colv(2),colv(1)],[{colv(1)},{colv(1),colv(2)},{-colv(1)},{-colv(1),-colv(2)}]]),
00066   assert(okltest_tcol2sat_hg2fcs(buildq([f],lambda([G],fcl2fcs(f(hg2ohg(G))))))),
00067   true)$
00068 
00069 okltest_tcol2sat_stdohg2stdfcl(f) := (
00070   assert(f([[],[]]) = [[],[]]),
00071   assert(f([[],[{}]]) = [[],[{},{}]]),
00072   assert(f([[2],[{2},{}]]) = [[2],[{2},{},{-2},{}]]),
00073   assert(f([[2,1],[{1},{1,2}]]) = [[2,1],[{1},{1,2},{-1},{-1,-2}]]),
00074   assert(okltest_tcol2sat_stdhg2stdfcs(buildq([f],lambda([G],fcl2fcs(f(hg2ohg(G))))))),
00075   true)$
00076 
00077 
00078 /* ***********************************
00079    * Translations to non-boolean SAT *
00080    ***********************************
00081 */
00082 
00083 okltest_col2sat_ohg2nbfclud(f) := block([x],
00084   assert(f([[],[]],[]) = [[],[],[]]),
00085   assert(f([[],[{}]],[]) = [[],[{}],[]]),
00086   assert(f([[],[{},{}]],[]) = [[],[{},{}],[]]),
00087   assert(f([[],[{}]],[1,2]) = [[],[{},{}],[1,2]]),
00088   assert(f([[2,1],[{}]],[2]) = [[colv(2),colv(1)],[{}],[2]]),
00089   assert(f([[2,1],[{1,2},{1}]],[3,x]) = [[colv(2),colv(1)], 
00090     [{[colv(1),3],[colv(2),3]},{[colv(1),3]},{[colv(1),x],[colv(2),x]},{[colv(1),x]}], [3,x]]),
00091   /* XXX */
00092   true)$
00093 
00094 okltest_col2sat_stdohg2stdnbfclud(f) := block([x,y],
00095   assert(f([[],[]],[]) = [[],[], []]),
00096   assert(f([[],[{}]],[]) = [[],[{}], []]),
00097   assert(f([[],[{},{}]],[]) = [[],[{},{}], []]),
00098   assert(f([[],[{}]],[1,2]) = [[],[{},{}], [1,2]]),
00099   assert(f([[1,2],[{1},{1,2}]],[x,y]) = [[1,2],
00100     [{[1,x]},{[1,x],[2,x]},{[1,y]},{[1,y],[2,y]}], [x,y]]),
00101   assert(okltest_col2sat_stdhg2stdnbfcsud(buildq([f], lambda([G,S], nbfclud2nbfcsud(f(hg2ohg(G), listify(S)))))) = true),
00102   /* XXX */
00103   true)$
00104 
00105 okltest_col2sat_stdhg2stdnbfcsud(f) := block([x,y],
00106   assert(f([{},{}],{}) = [{},{},{}]),
00107   assert(f([{},{{}}],{}) = [{},{{}},{}]),
00108   assert(f([{},{{}}],{1,2}) = [{},{{}}, {1,2}]),
00109   assert(f([{1,2},{{1},{1,2}}],{x,y}) = [{1,2},
00110     {{[1,x]},{[1,x],[2,x]},{[1,y]},{[1,y],[2,y]}}, {x,y}]),
00111   /* XXX */
00112   true)$
00113 
00114 okltest_gcol2sat_ohg2nbfclud(f) := block([x,y],
00115   assert(f([],[]) = [[],[],[]]),
00116   assert(f([[[],[]]],[x]) = [[],[],[x]]),
00117   assert(f([[[],[{}]]],[x]) = [[],[{}],[x]]),
00118   assert(f([[[2,1],[{}]]],[x]) = [[colv(2),colv(1)],[{}],[x]]),
00119   assert(f([[[2,1],[{},{1},{2},{1,2}]]],[x]) = [[colv(2),colv(1)],[{},{[colv(1),x]},{[colv(2),x]},{[colv(1),x],[colv(2),x]}],[x]]),
00120   assert(f([[[],[]],[[],[]]],[x,y]) = [[],[],[x,y]]),
00121   assert(f([[[2,3],[]],[[1,3],[]]],[x,y]) = [[colv(2),colv(3),colv(1)],[],[x,y]]),
00122   assert(f([[[2,3],[{}]],[[1,3],[{}]]],[x,y]) = [[colv(2),colv(3),colv(1)],[{},{}],[x,y]]),
00123   assert(f([[[2,3],[{}]],[[1,3],[{1},{1,3}]]],[x,y]) = [[colv(2),colv(3),colv(1)],[{},{[colv(1),y]},{[colv(1),y],[colv(3),y]}],[x,y]]),
00124   assert(f([[[2,3],[{3},{2,3},{}]],[[1,3],[{1},{1,3}]]],[x,y]) = [[colv(2),colv(3),colv(1)],[{[colv(3),x]},{[colv(2),x],[colv(3),x]},{},{[colv(1),y]},{[colv(1),y],[colv(3),y]}],[x,y]]),
00125   assert(okltest_gcol2sat_stdohg2stdnbfclud(buildq([f],lambda([GG,S], ev(f(GG,S), colv(x):=x, nouns)))) = true),
00126   true)$
00127 
00128 okltest_gcol2sat_stdohg2stdnbfclud(f) := block(
00129   assert(f([],[]) = [[],[],[]]),
00130   assert(f([[[],[]]],[x]) = [[],[],[x]]),
00131   assert(f([[[],[{}]]],[x]) = [[],[{}],[x]]),
00132   assert(f([[[2,1],[{}]]],[x]) = [[2,1],[{}],[x]]),
00133   assert(f([[[2,1],[{},{1},{2},{1,2}]]],[x]) = [[2,1],[{},{[1,x]},{[2,x]},{[1,x],[2,x]}],[x]]),
00134   assert(f([[[],[]],[[],[]]],[x,y]) = [[],[],[x,y]]),
00135   assert(f([[[2,3],[]],[[1,3],[]]],[x,y]) = [[2,3,1],[],[x,y]]),
00136   assert(f([[[2,3],[{}]],[[1,3],[{}]]],[x,y]) = [[2,3,1],[{},{}],[x,y]]),
00137   assert(f([[[2,3],[{}]],[[1,3],[{1},{1,3}]]],[x,y]) = [[2,3,1],[{},{[1,y]},{[1,y],[3,y]}],[x,y]]),
00138   assert(f([[[2,3],[{3},{2,3},{}]],[[1,3],[{1},{1,3}]]],[x,y]) = [[2,3,1],[{[3,x]},{[2,x],[3,x]},{},{[1,y]},{[1,y],[3,y]}],[x,y]]),
00139   true)$
00140 
00141 okltest_gcol2sat_ohg2nbfclud_p(f) := block(
00142   assert(f(0,0) = false),
00143   /* XXX */
00144   true)$
00145 
00146 
00147 /* ***************************************************************
00148    * Determining all k-colourings via the transversal hypergraph *
00149    ***************************************************************
00150 */
00151 
00152 /* Testing whether f(G,k) is the set-system of all independent k-covers
00153    of G (together with G[1]):
00154 */
00155 okltest_allindkcov_hg(f) := (
00156   assert(f([{},{}],0) = [{}, {{}}]),
00157   assert(f([{},{}],1) = [{}, {{{}}}]),
00158   assert(f([{},{}],2) = [{}, {}]),
00159   assert(f([{},{{}}],0) = [{}, {{}}]),
00160   assert(f([{},{{}}],1) = [{}, {}]),
00161   assert(f([{},{{}}],2) = [{}, {}]),
00162   assert(f([{1},{}],0) = [{1},{}]),
00163   assert(f([{1},{}],1) = [{1},{{{1}}}]),
00164   assert(f([{1},{}],2) = [{1},{}]),
00165   assert(f([{1},{{}}],0) = [{1},{}]),
00166   assert(f([{1},{{}}],1) = [{1},{}]),
00167   assert(f([{1},{{}}],2) = [{1},{}]),
00168   assert(f([{1},{{1}}],0) = [{1},{}]),
00169   assert(f([{1},{{1}}],1) = [{1},{}]),
00170   assert(f([{1},{{1}}],2) = [{1},{}]),
00171   assert(f([{1,2},{}],0) = [{1,2},{}]),
00172   assert(f([{1,2},{}],1) = [{1,2},{{{1,2}}}]),
00173   assert(f([{1,2},{}],2) = [{1,2},{}]),
00174   assert(f([{1,2},{}],3) = [{1,2},{}]),
00175   assert(f([{1,2},{{}}],0) = [{1,2},{}]),
00176   assert(f([{1,2},{{}}],1) = [{1,2},{}]),
00177   assert(f([{1,2},{{}}],2) = [{1,2},{}]),
00178   assert(f([{1,2},{{}}],3) = [{1,2},{}]),
00179   assert(f([{1,2},{{1}}],0) = [{1,2},{}]),
00180   assert(f([{1,2},{{1}}],1) = [{1,2},{}]),
00181   assert(f([{1,2},{{1}}],2) = [{1,2},{}]),
00182   assert(f([{1,2},{{1}}],3) = [{1,2},{}]),
00183   assert(f([{1,2},{{1},{2}}],0) = [{1,2},{}]),
00184   assert(f([{1,2},{{1},{2}}],1) = [{1,2},{}]),
00185   assert(f([{1,2},{{1},{2}}],2) = [{1,2},{}]),
00186   assert(f([{1,2},{{1},{2}}],3) = [{1,2},{}]),
00187   assert(f([{1,2},{{1,2}}],0) = [{1,2},{}]),
00188   assert(f([{1,2},{{1,2}}],1) = [{1,2},{}]),
00189   assert(f([{1,2},{{1,2}}],2) = [{1,2},{{{1},{2}}}]),
00190   assert(f([{1,2},{{1,2}}],3) = [{1,2},{}]),
00191   assert(f([{1,2},{{},{1,2}}],0) = [{1,2},{}]),
00192   assert(f([{1,2},{{},{1,2}}],1) = [{1,2},{}]),
00193   assert(f([{1,2},{{},{1,2}}],2) = [{1,2},{}]),
00194   assert(f([{1,2},{{},{1,2}}],3) = [{1,2},{}]),
00195   assert(f([{1,2},{{1},{1,2}}],0) = [{1,2},{}]),
00196   assert(f([{1,2},{{1},{1,2}}],1) = [{1,2},{}]),
00197   assert(f([{1,2},{{1},{1,2}}],2) = [{1,2},{}]),
00198   assert(f([{1,2},{{1},{1,2}}],3) = [{1,2},{}]),
00199   assert(f([{1,2},{{1},{2},{1,2}}],0) = [{1,2},{}]),
00200   assert(f([{1,2},{{1},{2},{1,2}}],1) = [{1,2},{}]),
00201   assert(f([{1,2},{{1},{2},{1,2}}],2) = [{1,2},{}]),
00202   assert(f([{1,2},{{1},{2},{1,2}}],3) = [{1,2},{}]),
00203   assert(f([{1,2,3},{{1,2,3}}],0) = [{1,2,3},{}]),
00204   assert(f([{1,2,3},{{1,2,3}}],1) = [{1,2,3},{}]),
00205   assert(f([{1,2,3},{{1,2,3}}],2) = [{1,2,3},{{{1,2},{2,3}},{{1,2},{1,3}},{{1,3},{2,3}}}]),
00206   assert(f([{1,2,3},{{1,2,3}}],3) = [{1,2,3},{{{1,2},{2,3},{1,3}}}]),
00207   assert(f([{1,2,3},{{1,2,3}}],4) = [{1,2,3},{}]),
00208   for n : 1 thru if oklib_test_level = 0 then 4 else 6 do
00209     for r : 1 thru 2 do
00210       for k : 0 thru n+1 do
00211         assert(f(complete_stdhg(n,r),k) = [setn(n), if r=1 then {} elseif k=n then {singletons(setn(n))} else {}]),
00212   /* XXX */
00213   true)$
00214 
00215