OKlibrary  0.2.1.6
Colouring.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 26.1.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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Transversals/Minimal/RecursiveSplitting.mac")$
00028 
00029 
00030 /* *******************************
00031    * Translations to boolean SAT *
00032    *******************************
00033 */
00034 
00035 /* Colouring variables: terms colv(v), where v is a vertex: */
00036 kill(colv)$
00037 declare(colv,noun)$
00038 declare(colv,posfun)$
00039 colv_var(v) := nounify(colv)(v)$
00040 
00041 /* Translates a colouring literal to an extended-dimacs compatible string: */
00042 colv_string(l) := sconcat(
00043   if abs(l) = l then "" else "-",
00044   block([S : args(args(abs(l))[1])],
00045     sconcat(
00046       if length(S) = 0 then "E"
00047       else xreduce(
00048         lambda([a,b],sconcat(a,"S",b)),
00049         rest(S),first(S)),
00050       " ")))$
00051 
00052 /* Translating the 2-colouring problem for hypergraph G into the SAT problem
00053    for a formal boolean clause-set: */
00054 tcol2sat_hg2fcs(G) := block(
00055  [Fpos : map(lambda([H], map(colv_var,H)), listify(G[2]))],
00056   [map(colv_var,G[1]), setify(append(Fpos, comp_cs(Fpos)))])$
00057 /* Using the vertices directly as variables; works for example for
00058    standardised hypergraphs: */
00059 tcol2sat_stdhg2stdfcs(G) := [G[1], union(G[2], comp_cs(G[2]))]$
00060 tcol2sat_stdohg2stdofcs(G) := [G[1], append(G[2], comp_cl(G[2]))]$
00061 
00062 /* Now for ordered hypergraphs, producing clause-lists: */
00063 /* If G does not contain an empty hyperedge, then the result is
00064    actually a (formal) ordered clause-list. */
00065 tcol2sat_ohg2fcl(G) := [map(colv_var,G[1]),
00066   block([Fpos : map(lambda([H], map(colv_var,H)), G[2])],
00067     append(Fpos, comp_cl(Fpos)))]$
00068 tcol2sat_stdohg2stdfcl(G) := [G[1], append(G[2], comp_cl(G[2]))]$
00069 
00070 gtcol2sat_ohg2fcl(G1,G2) :=
00071  [map(colv_var,stable_unique(append(G1[1],G2[1]))),
00072   append(map(lambda([H], map(colv_var,H)), G1[2]),
00073          comp_cl(map(lambda([H], map(colv_var,H)), G2[2])))
00074  ]$
00075 gtcol2sat_stdohg2stdfcl(G1,G2) := [
00076  create_list(i,i,1,max(length(G1[1]),length(G2[1]))),
00077  append(G1[2], comp_cl(G2[2]))
00078 ]$
00079 
00080 
00081 /* ***********************************
00082    * Translations to non-boolean SAT *
00083    ***********************************
00084 */
00085 
00086 /* Translating an S-colouring problem (S a set/list of colours) for
00087    hypergraph G into the SAT problem for a formal nb-clause-set (using
00088    non-boolean variables; with uniform domain).
00089 */
00090 
00091 /* For an (arbitrary) ohg G and a list S of colours, using variables colv(v)
00092    for vertices v of G:
00093 */
00094 col2sat_ohg2nbfclud(G,S) :=
00095  if emptyp(S) and emptyp(G[1]) then [[], G[2], []] else
00096  [
00097   map(colv_var,G[1]),
00098   block([Fpos : map(lambda([H], map(colv_var,H)), G[2])],
00099      lappend(create_list(map(lambda([C],cartesian_product(C,{c})),Fpos), c,S))),
00100   S]$
00101 /* Now just using the vertices as variables: */
00102 /* TODO: the function-name ("std") seems inappropriate, since arbitrary
00103    vertex-names make sense here.
00104 */
00105 col2sat_stdohg2stdnbfclud(G,S) :=
00106  if emptyp(S) and emptyp(G[1]) then [[], G[2], []] else
00107  [
00108   G[1],
00109   lappend(create_list(map(lambda([C],cartesian_product(C,{c})),G[2]), c,S)),
00110   S]$
00111 col2sat_stdhg2stdnbfcsud(G,S) :=
00112  if emptyp(S) and emptyp(G[1]) then [{}, G[2], {}] else
00113  [
00114   G[1],
00115   lunion(map(lambda([c], map(lambda([C],cartesian_product(C,{c})),G[2])), S)),
00116   S]$
00117 
00118 /* Generalised colouring, where for hypergraph GG[i] every hyperedge must
00119    contain a vertex not coloured by colour S[i].
00120    Prerequisite: length(GG) = length(S).
00121 */
00122 gcol2sat_ohg2nbfclud(GG,S) := [
00123  map(colv_var, stable_unique(lappend(map(first,GG)))),
00124  lappend(create_list(
00125           map(lambda([H], cartesian_product(map(colv_var,H),{S[i]})), GG[i][2]),
00126           i,1,length(S))),
00127  S]$
00128 gcol2sat_stdohg2stdnbfclud(GG,S) := [
00129  stable_unique(lappend(map(first,GG))),
00130  lappend(create_list(
00131           map(lambda([H], cartesian_product(H,{S[i]})), GG[i][2]),
00132           i,1,length(S))),
00133  S]$
00134 /* Checking the validity of the arguments (applies for both forms): */
00135 gcol2sat_ohg2nbfclud_p(GG,S) :=
00136   listp(GG) and listp(S) and is(length(GG)=length(S))
00137   and every_s(ohg_p,GG)$
00138 
00139 
00140 /* ***************************************************************
00141    * Determining all k-colourings via the transversal hypergraph *
00142    ***************************************************************
00143 */
00144 
00145 /* k-colourings of a hypergraph G using exactly k colours can be represented
00146    by k-subsets s of powerset(G[1]) such that s is a covering of G[1] by
00147    maximal independent subsets.
00148    Let us call such a representation s an "independent k-cover"; more
00149    precisely it seems better to use the pair [V, S], where V is the
00150    vertex set of G, while S is the set of all independent k-covers.
00151    Equivalently, one can use such k-sets S consisting of minimal transversals
00152    such that their common intersection is empty; but it seems more appropriate
00153    to convert such an S into an S of the first form by taking complements.
00154 
00155    Remarks:
00156     - For the empty vertex set the correspondence to colouring is broken
00157       in two cases:
00158      + An empty set as a maximal independent subset can be used here
00159        exactly when G = [{},{}] and k=1; this does not correspond to a
00160        colouring using exactly one colour.
00161      + And an independent 0-cover exists exactly for  G = [{},{{}}]; again
00162        this does not correspond to a colouring (using exactly null colours
00163        --- but G is not colourable).
00164     - If in the k-cover two maximal independent sets would coincide then this
00165       actually is not possible. So for example [{1,2},{}] has no independent
00166       2-cover (while it has 4 2-colourings).
00167 */
00168 
00169 /* Computing all k-colourings of hypergraph G as the set of all
00170    independent k-covers, using _hyptrans(G) for computing
00171    the transversal hypergraph of G:
00172 */
00173 allindkcov_hyptrans_hg(G,k,_hyptrans) := block([V : G[1]],
00174  [V, map(lambda([S],ecomp(S,V)),anti_edge_k_hg(_hyptrans(G),k)[2])])$
00175 
00176 /* The instantiation by the basic algorithm for computing the
00177    transversal hypergraph:
00178 */
00179 allindkcov_hyptrans_rs_hg(G,k) := allindkcov_hyptrans_hg(G,k,transversal_hg_rs)$
00180