OKlibrary
0.2.1.6

00001 /* Oliver Kullmann, 4.9.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/Hypergraphs/Lisp/Generators/Ramsey.mac")$ 00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")$ 00024 00025 00026 /* The Ramseynumber ramsey_s^r(q_1, ..., q_s) is the smallest n >= 0 such 00027 that however the set of rsubsets of {1, ..., n} is divided into s 00028 (possibly empty) parts, there exists one part 1 <= i <= s containing 00029 all the possible rsubsets of some qelement subset of {1,...,n}. 00030 00031 If q_1 = ... = q_s = q, then we have a hypergraph colouring problem, where 00032 the question is whether ramsey_ohg(q,r,n) is scolourable (see 00033 ComputerAlgebra/Hypergraphs/Lisp/Generators/Generators.mac; this hypergraph 00034 has as vertices the rsubsets of {1,...,n}, while the hyperedges are the 00035 sets of all rsubsetvertices within all possible qsubsets of {1,...,n}). 00036 */ 00037 00038 /* The boolean ordered formal clausesets expressing that ramsey_2^r(q,q) > n; 00039 a satisfying assignments yields a 2colouring of the binom(q,r)hypergraph 00040 with vertices all rsubsets of {1,...,n}, while the set of hyperedges is the 00041 set of the sets of all rsubsets obtained from the qsubsets of {1,...,n}. 00042 In other words, the clauseset is satisfiable iff one can assign 0 and 00043 1 to the relement subsets (the "vertices") of {1,...,n} such that for 00044 every qelement subset of {1,...,n} there are two such vertices which are 00045 subsets (of the qelement set) and which have different values assigned. 00046 For r=2 we have the interpretation, that the clauseset is satisfiable 00047 iff there exists an edgelabelling of the K_n with "colours" 1,2 such 00048 that no qclique is monochromatic (w.r.t. the edges involved). 00049 For arbitrary r, instead of K_n^r one considers the K_n^r, the rgraph 00050 consisting of all relement subsets of {1,...,n}; satisfying assignments 00051 are those labellings of the relement subsets with "colours" 1,2 such 00052 that every qelement subset of {1,...,n} contains some relement subset 00053 for each of the two colours. 00054 00055 Variables are the colouringvariables colv(s) for the rsubsets of 00056 {1,...,n}, ordered lexicographically. The clauselist contains first 00057 the positive clauses, then the negative clauses, each sublist ordered 00058 lexicographically. 00059 */ 00060 ramsey2_ofcs(q,r,n) := tcol2sat_ohg2fcl(ramsey_ohg(q,r,n))$ 00061 00062