OKlibrary  0.2.1.6
RamseyProblems.hpp File Reference

How to use the Ramsey problem generators. More...

Go to the source code of this file.


Detailed Description

How to use the Ramsey problem generators.

Ramsey problems via Maxima in the OKlibrary

Generating additional clauses for symmetry breaking

  • One may generate a symmetry breaking partial assignment for a given Ramsey problem of the form "R(q,q;2) > n" in the following way :
    RSP_pass : ramsey_symbr1_pass(q,n);
       
  • One can also generate additional clauses for symmetry breaking of a given Ramsey problem of the form "R(q,q;2) > n" in the following way :
    RSB : ramsey_symbr2_cs(n);
       
  • The above assumes that variables are given in the form "colv({a,b})" for edges connecting vertices "a" and "b". This need not be the case, and then the second and third argument to the function are functions mapping from the undirected edges (e.g., {a,b}) to their corresponding undirected edges, and vice versa.
  • The reason for the above notation ("colv({a,b})") etc. in the example above is that the result of this can easily be converted to the format "aSb" sometimes used when generating clause-sets for the Ramsey problems in the extended Dimacs format. This can be done like so :
    RSB_e : map(lambda([a], map(lambda([b], sconcat(if sign(b) = neg then "-" else "",listify(args(abs(b))[1])[1],"S",listify(args(abs(b))[1])[2])),a)), RSB);
       
  • For a generated clause-set, the following code may be used to output the clause-set in extended Dimacs format:
    colv2str(x) := block([vals_abs],
      vals_abs : listify(args(abs(x))[1]),
      return(sconcat(if sign(x) = neg then "-" else "",
          vals_abs[1], "S", vals_abs[2])))$
    
    output_cs_ef(n,F,f) := 
      with_stdout(n, block(
        print(sconcat("p ", length(var_cs(F)), " ",length(F))),
        for C in F do block([C_str],
          C_str : uaapply(sconcat, listify(
              map(lambda([a], sconcat(f(a)," ")), C))),
          C_str : sconcat(C_str, " 0"),
          print(C_str))))$
    
    output_cs_ef(filename, clause_set, colv2str)$
       

Definition in file RamseyProblems.hpp.