Go to the documentation of this file.
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. */
00022 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Generators/Ramsey.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")$
00026 /* The Ramsey-number ramsey_s^r(q_1, ..., q_s) is the smallest n >= 0 such
00027    that however the set of r-subsets of {1, ..., n} is divided into s
00028    (possibly empty) parts, there exists one part 1 <= i <= s containing
00029    all the possible r-subsets of some q-element subset of {1,...,n}.
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 s-colourable (see
00033    ComputerAlgebra/Hypergraphs/Lisp/Generators/Generators.mac; this hypergraph
00034    has as vertices the r-subsets of {1,...,n}, while the hyperedges are the
00035    sets of all r-subset-vertices within all possible q-subsets of {1,...,n}).
00036 */
00038 /* The boolean ordered formal clause-sets expressing that ramsey_2^r(q,q) > n; 
00039    a satisfying assignments yields a 2-colouring of the binom(q,r)-hypergraph
00040    with vertices all r-subsets of {1,...,n}, while the set of hyperedges is the
00041    set of the sets of all r-subsets obtained from the q-subsets of {1,...,n}.
00042    In other words, the clause-set is satisfiable iff one can assign 0 and
00043    1 to the r-element subsets (the "vertices") of {1,...,n} such that for 
00044    every q-element subset of {1,...,n} there are two such vertices which are
00045    subsets (of the q-element set) and which have different values assigned.
00046    For r=2 we have the interpretation, that the clause-set is satisfiable
00047    iff there exists an edge-labelling of the K_n with "colours" 1,2  such
00048    that no q-clique is monochromatic (w.r.t. the edges involved).
00049    For arbitrary r, instead of K_n^r one considers the K_n^r, the r-graph
00050    consisting of all r-element subsets of {1,...,n}; satisfying assignments
00051    are those labellings of the r-element subsets with "colours" 1,2 such
00052    that every q-element subset of {1,...,n} contains some r-element subset
00053    for each of the two colours.
00055    Variables are the colouring-variables colv(s) for the r-subsets of
00056    {1,...,n}, ordered lexicographically. The clause-list 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))$