OKlibrary  0.2.1.6
VanderWaerdenProblems.hpp File Reference

Plans for Maxima-generators related to van der Waerden problems (and generalisations) More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-generators related to van der Waerden problems (and generalisations)

Todo:
Connections
Todo:
Organisation : DONE
  • DONE Likely we should create a submodule "Lisp/Generators/RamseyTheory".
  • DONE There then the Green-Tao functions should go into a separate file.
  • DONE Perhaps we should split the module, as we have it now with Investigations/RamseyTheory; a question whether we should use "Problems" as part of the module names or not (as in ComputerAlgebra/RamseyTheory).
Todo:
Standardisation
  • As we have it now in output_vanderwaerden, standardisation for all non-standardised clause-sets should be done explicitly.
Todo:
Statistics
  • As discussed in "Accompanying statistics" in Satisfiability/Lisp/Generators/plans/general.hpp in general, we need statistics for all main measurements (and also for all others, if possible).
  • DONE First the hypergraph measurements needs to be established; see "Statistics" in Hypergraphs/Lisp/plans/Generators.hpp.
Todo:
Systematic output and output-functions
  • Likely, the outputs for van-der-Waerden and for Green-Tao problems should be very similar.
  • Regarding the naming of files, for the general (non-boolean, non- diagonal) form we should provide another form which translates for example [2,2,2,2,3,3,4] in "_7_2:4_3:2_4".
  • DONE What about the diagonal forms? Yet output_greentao2_stdname uses the length of the arithmetic progression in the filename twice, while output_greentaod_stdname writes out that length just once. This seems better.
  • The part "_sb" in the name (for symmetry-breaking) should perhaps be placed at the very end.
  • The output-function should use the clause-list-forms, not the clause-set-forms.
Todo:
Palindromic versions with arithmetic progressions of length 3
  • We consider parameter tuple (k=3,k').
  • For progression length k=3 and odd n >= 3, if the middle point (n+1)/2 is included, then all other points must be excluded (otherwise one gets an arithmetic progression of length 3).
  • However then for most values of k' we get an arithmetic progression of length k'.
  • Thus variable (n+1)/2 must be set to false.
  • This follows by r_2-reduction, but might pose a problem for some solver, so perhaps should be supplied by the translation.
  • The remaining question is to determine those odd n for given k' such that {1,...,n} - {(n+1)/2} contains an arithmetic progression of length k':
    1. Trivially for k' <= (n+1)/2-1.
    2. For n=5 this is tight, but not for n=3, where {1,3} contains (1,3), nor for n=7, where {1,2,3,5,6,7} contains (1,3,5,7).
    3. Call f(n) for odd n >= 3 the maximal length of an arithmetic progression in {1,...,n} - {(n+1)/2}.
    4. So f(n) >= (n+1)/2-1, f(3) = 2, f(5) = 2, f(7) = 4.
    5. n=9: {1,2,3,4,6,7,8,9} allows only progressions of length 4, so f(9) = 4.
    6. n=11: {1,2,3,4,5,7,8,9,10,11} allows (1,3,5,7,9,11), so f(11) = 6.
    7. Thus one guesses that in case of (n+1)/2 odd on has f(n) = (n+1)/2-1, while otherwise we have f(n) = (n+1)/2.
    8. So the exceptional n, where the lower-bound can be increased by one, would be the n where n+1 contains prime-factor 2 at least twice.
    9. That is, the n of the form 4*k-1, k >= 1, are exceptional.
    10. The formula thus is (with simple proof): If n = 4*k-1, then f(n) = (n+1)/2, while otherwise f(n) = (n+1)/2-1.
  • Perhaps we implement then pd_vanderwaerden3k_fcl(k,n), which includes that additional unit-clauses in case of k <= f(n).
  • If later we find other interesting implications (prime implicates), then we might add further versions.
Todo:
Alternative handling of parameter-values 2
  • A parameter value 2 means that the corresponding part can contain at most one element.
  • Currently this gets (automatically) translated using the standard representation of AMO for the vertices, using binomial(n,2) binary clauses (since two different vertices make always a progression of length 2).
  • An alternative is presented in "At-most-one as a CNF" in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/plans/Thresholds.hpp, and one should try this.
  • We should also provide standard generators for these two AMO-representations.
  • Another alternative generalises the treatment of the transversal case (all parameters except of one equal 2):
    1. Let the parameter tuple be [2,..,2,t], where t contains no 2, and where we have p 2's. And let the length of t be q (so that the length of the whole tuple is p + q).
    2. One could use non-boolean variables with q+1 values, where we have on the first q values the ordinary constraints coming from t, while using some additional parameter B for the first value we add the condition that the number of variables with that value is equal to B.
    3. B is here the number of variables *not* available to satisfy the t-requirements.
    4. The task is to maximise B; using as generalised transversal number tau(F) of an arbitrary satisfiable clause-set F the minimum of n(phi) for satisfying partial assignments phi, this corresponds to compute tau(F) = n - B.
    5. Such generalised transversal problems (for arbitrary F) can be handled as above, by introducing the additional value to indicate variables not to be used.
    6. However, just having negative monosigned literals is not enough, but we need to consider monosigned literals. And actually, since for q >= 3 negative monosigned literals must be used w.r.t. t, we have a problem w.r.t. handling the value "undefined"! Perhaps an extension of monosigned literals is needed, allowing to express "v<>val but v is defined" ?! For q=2 the t-part can be expressed using positive monosigned literals, and so monosigned literals are altogether enough here.
    7. See "Parameterisation" in Algorithms/AllSolutions/plans/MinimalAssignments.hpp for general plans at the C++ level.
Todo:
DONE More than two parts
Todo:
Symmetry breaking for vdW-problems
  • The symmetry-breaking should happen as with the Green-tao problems, only that the distinguished vertex is a central one.
  • This needs to be investigated; it seems that floor(n/2)-1 is always a vertex with maximal degree.

Definition in file VanderWaerdenProblems.hpp.