general.hpp File Reference

On investigations into Ramsey problems. More...

Go to the source code of this file.

Detailed Description

On investigations into Ramsey problems.

Generation of problem instances
  • Generation of CNF representations:
    1. By the Maxima system, via "output_ramsey2_stdname(q,r,n)" we create "Ramsey_q_r_n.cnf", for ramsey_2^r(q).
    2. However, output_ramsey2_stdname(5,2,40) yields a segmentation fault on a 32-bit machine (not enough memory, when introducing the colouring symbols); so we need to use the following (C++) application.
    3. More generally (and faster), the application "Ramsey" can generate also non-diagonal problems, via
      Ramsey-O3-DNDEBUG q1 q2 r n | ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_q1_q2_r_n.cnf
      for ramsey_2^r(q1,q2).
How to handle experimental data?
Data sheets
  • All the numbers and all known information should be available on some html-page.
Experiments to be run
Investigate introduction of cardinality constraints
  • It is a conjecture of MG that any Ramsey problem of the form ramsey_2^2(q), if it has a solution, must have a solution where the number of edges labelled with one label differs at most one from the number of edges labelled with the other.
  • The intuition (and potential for generalisation to more than 2 labels/partitions) is that dominating a labelling/colouring of a graph with more of one label/colour than another, simply makes it harder to avoid forming monochromatic q-cliques in that label.
  • Satisfiability for n=5 is trivial for any SAT solver.
  • So is unsatisfiability for n=6.
  • Known is 102 <= ramsey_2^2(6) <= 165.
  • These clause-sets are too big (for direct representation).
Investigating the parameter tuple [[3,3],2]
  • Creating the relevant instances: by
    R5: ramsey2_ofcs(3,2,5);
    R6: ramsey2_ofcs(3,2,6);
    we create the two relevant (ordered formal) clause-sets.
  • Satisfying assignments:
    R5SAT : setify(all_sat_ofcs(R5))$
  • Now we need to investigate the operation of the automorphism group of R5 on R5SAT (what are the really different solutions?).
    1. For this we need to compute the automorphism group of R5; see "Automorphisms of Ramsey clause-sets" in RamseyTheory/Lisp/Ramsey/plans/general.hpp.
    2. One solution (as graph; see "Representing solutions as graphs" below) is the C^5, and we have all hamiltonian cycles of the K_5 as similar solutions under the operation of the S_5: This yields 4! / 2 = 12 solutions, so actually all solutions are isomorphic to C^5.
    3. We need to divide by 2 here since we are considering "cyclic permutations" (so that [1,2,3,4,5] is the same as [1,5,4,3,2]).
  • Via
    we see that there are only the obvious autarkies.
Exploring the parameter space
  • A systematic exploration of different parameter tuples is needed.
  • For instance, if one has parameters k and q, and then considers the Ramsey tuple ramsey_(k+1)^2(2,...k times...,2,q) for instance, how do such Ramsey numbers grow?
  • We should investigate autarkies of Ramsey-clause-sets.
  • It could be that for smaller n interesting autarkies exist, and so they could serve for providing lower bounds.
Blocked clauses
  • We should investigate blocked clauses of Ramsey-clause-sets.
Symmetry breaking
Representing solutions as graphs
  • A solution for the parameter-values ([[p,q],2]; n) (that is, a labelling of the K_n with colours 0,1 such that no clique of size p of colour 0 and no clique of size q of colour 1 exists), corresponds to a graph with n vertices not containing a clique of size p or an independent set of size q.
  • This graph representation brings with it a notion of isomorphic solutions by using graph isomorphisms.
  • If p = q, then as an additional symmetry we have the correspondence between a graph and its complement.
  • The underlying reasoning is as follows:
    1. We consider the general problem of when two solutions of a satisfiability problem are to be considered "similar".
    2. The strongest possibility (detecting the most similarities) seems to use the automorphism group of the set of all (total) solutions, and then to consider two solutions as similar iff they are in the same orbit under this operation (i.e., there is an automorphism turning the one solution into the other).
    3. This considers only the solution space, not the representation.
    4. Perhaps most common is to consider the automorphism group of the representation (and its operation), which yields a subgroup of the automorphism group of the solutions.
    5. For the Ramsey problems presented as clause-sets we know the automorphisms given by S_n, and S_n x ZZ_2 for symmetric problems.
    6. In the graph-case we are considering here this yields exactly to consider two solutions as similar iff their graphs are isomorphic, where for symmetric problems we consider also a graph and its complement as similar.
  • For the Ramsey parameter tuple [[3,3],2] and n = 5 we have the solution C^5 (the cycle with 5 edges), which is self-dual (and this is the only solution; see above).
  • We should have an extensive catalogue as possible for the known solution types (if possible, augmented by the information how many solutions in total they represent).
Self-dual solutions
  • For the Ramsey parameter tuple [[3,3],2] we have a self-dual solution (a graph isomorphic to its complement).
  • Are there self-dual solutions for all [[p,p],2] ??
  • We need to check the known cases!
  • For [[5,5],2] and n=42 the number of edges (861) of K_n is odd, so if the conjecture ramsey_2^2(5,5) = 43 is true, then there would be no self-dual solution here.
"Visualising" solutions
  • Via SAT solvers we can compute certain solutions for problems somewhat smaller than the interesting sizes.
  • The task is to "look" at these solutions, extract some structure, and then to systematically search for "such" solutions.
  • Of course, everything theoretically known needs to be explored.
  • From the practical side, there has been work (e.g., Marijn Heule) for van der Waerden problems.
  • See "Representing solutions as graphs" above; perhaps that's the best what we can do for those problems? But if we know more about the symmetries between solutions (i.e., the automorphism group of the solution space, then we might obtain further compression.
  • There is also the simple representation of these solutions using colours for the two labels/partitions.
  • Colouring edges rather than simply showing a graph with edges missing seems a much better solution, as from a visualisation point of view, one sees both the graph and it's complement at the same time, and so the colour symmetry is more obvious to the eye (as both the graph and it's complement are important for discerning patterns).
  • Both visualisations should be made available, and translations from a solution (set of literals using the canonical variable naming) to graphs and graph labellings should be written.
  • Both visualisations are now possible in the library for r=2,s=2:
    • Given a partial assignment S as a solution to the Ramsey problem "ramsey_2^2(p,q) > n?", one may show the underlying graph represented by the edges labelled with p in the following way:
      n : 17$
      S: {1,-2,-3,4,-5,-6,7,8,9,-10,11,-12,13,-14,-15,-16,-17,18,-19,-20,21,-22,23,24,
    • Given a partial assignment S as a solution to the Ramsey problem "ramsey_2^2(p,q) > n?", one may show the complete graph with different coloured edges for the labels p and q in the following way:
      n : 17$
      S: {1,-2,-3,4,-5,-6,7,8,9,-10,11,-12,13,-14,-15,-16,-17,18,-19,-20,21,-22,23,
      vis_ramsey_sol(n,S) :=
  • The real question is how to draw such things well.
Statistics functions are needed to analyse counter examples
  • Visualising counter examples as in '"Visualising" solutions' seems only to be useful for reasonably small "n" and therefore, one should also provide statistics functions to extract some summarised information from the satisfying assignments we get from these Ramsey problems.
  • Some example statistics:
    • Number of edges with each label.
    • Frequency distribution of number of a particular colour edges leaving each node.
    • Number of cycles of a given colour/label of a given length.
  • Several of these should be possible using the standard statistics/analysis functions already available for graphs.
Better SAT solvers
  • These problems seem to be quite structured, so that quite something is known (at least more than for Van der Waerden numbers), but SAT solvers apparently can't exploit any of it.
  • What about constraint solvers? What do they use, and how succesful are they?
  • Active clause-sets should be attractive.
    1. Incorporating some of the knowledge we have for these problems.
    2. They should also be able to better detect symmetries.
  • Compressed representation of clauses:
    1. If that ZAP systems, which allows to use "annotated clauses", clauses plus a permutation group acting on the variables, is open-source, then it would be very natural to apply it here:
      1. The clause-set F_R([q_1, ..., q_s], r, n) can be expressed then by just s clauses together with the symmetric group S_n.
      2. However it is not available.
      3. One should have a look at those papers.
      4. A point here is that S_n does act faithful but not strongly faithful on the clauses (i.e., on the underlying hypergraph) --- can this be repaired or improved (S_n is a rather large group here)?
Fix obsolete notations DONE

Definition in file general.hpp.