On performance of symmetry breaking techniques on Ramsey problems.
More...
Go to the source code of this file.
Detailed Description
On performance of symmetry breaking techniques on Ramsey problems.
 Todo:
 Handling symmetries using extended resolution

OK mentioned that there was a paper which mentions small proof refutations for unsatisfiable Ramsey problems using symmetry rules.

OK also suggested that there was evidence that such things could be translated or replicated using the extended resolution proof system, maintaining the succinctness of the proof.

MG: Is this the paper being referred to [The Symmetry Rule in Propositional Logic]? It doesn't seem to mention Ramsey problems?
 Todo:
 Performance of symmetry breaking by fixing monochromatic cliques

Systematic experiments need to be run examining the performance of different classes of solvers on various Ramsey problems when additional symmetry breaking clauses are added, in particular, symmetry breaking clauses derived from the "Fixing monochromatic cliques" method.

MG ran some experiments using other solvers (picosat, minisat 2.1, hybridGM7 etc) which need to be included in the library (both the solvers and the results.

NOTE, for ramsey_2^2(5) <= 49, functions such as "ramsey2_symbr2_cs" ( See ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/RamseyProblems.mac) when added to associated clause set, will fix a monochromatic clique of size 5 (as 49 is a *known* upper bound for ramsey_2^2(5)), which will make the clause set unsatisfiable (as it should be).

This is not a problem, but it should be noted that symmetry breaking using this method is not making some huge breakthrough here.

See ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/RamseyProblems.mac.
 Todo:
 Using cardinality constraints

For ramsey_2^2(4) <= 18, OKsolver seems to perform worse (taking considerably longer per node when monitoring at the same depth) when using cardinality constraints (that is, number of variables set to true restricted to between floor(153/2) and ceil(153/2)).

However, this should be looked into further, as the time per node is irrelevant if overall less nodes are used.

Consider combining the PHP symmetry breaking, which already gives ramsey_2^2(4) = 18 in reasonable time, with the cardinality constraints (they are perfectly compatible).

MG should include the results from initial experiments he did using various solvers (such as picosat, minisat, OKsolver_2002) etc. on this.

From the paper "Subgraph Counting Identities and Ramsey Numbers" by McKay and Radziszowski, there are 656 nonisomorphic solutions for "ramsey_2_2(5,5) > 42 ?" (available at http://cs.anu.edu.au/~bdm/data/ramsey.html), where 16 of these have floor(binomial(42,2)/2) = 430 edges of one label.

However, there there are far more known solutions further from this central number (this can also be seen in the distribution of all ramsey_2^2(4,4) solutions), and with respect to this, Dr McKay offers that it seems that the solutions seem to like being slightly away from this central number of edges (number of one label).

When considering the conjecture, then, it seems reasonable to consider that perhaps a solution might only lie in a certain bound, within a certain distance of this central area (although there seem to be no available counterexamples to the original conjecture)?

See ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/plans/RamseyProblems.hpp.

DONE MG should search for or email McKay regarding the solutions for high n values for ramsey_2^2(5) mentioned in [A new upper bound for the Ramsey number R(5,5)] and check to see whether this conjecture holds in these cases.

DONE MG has emailed McKay regarding this and is awaiting a reply.
Definition in file SymmetryBreaking.hpp.