Plans for Maximagenerators related to van der Waerden problems (and generalisations)
More...
Go to the source code of this file.
Detailed Description
Plans for Maximagenerators 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 GreenTao 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 nonstandardised clausesets 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 outputfunctions

Likely, the outputs for vanderWaerden and for GreenTao problems should be very similar.

Regarding the naming of files, for the general (nonboolean, 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 symmetrybreaking) should perhaps be placed at the very end.

The outputfunction should use the clauselistforms, not the clausesetforms.
 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_2reduction, 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':

Trivially for k' <= (n+1)/21.

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).

Call f(n) for odd n >= 3 the maximal length of an arithmetic progression in {1,...,n}  {(n+1)/2}.

So f(n) >= (n+1)/21, f(3) = 2, f(5) = 2, f(7) = 4.

n=9: {1,2,3,4,6,7,8,9} allows only progressions of length 4, so f(9) = 4.

n=11: {1,2,3,4,5,7,8,9,10,11} allows (1,3,5,7,9,11), so f(11) = 6.


Thus one guesses that in case of (n+1)/2 odd on has f(n) = (n+1)/21, while otherwise we have f(n) = (n+1)/2.

So the exceptional n, where the lowerbound can be increased by one, would be the n where n+1 contains primefactor 2 at least twice.

That is, the n of the form 4*k1, k >= 1, are exceptional.

The formula thus is (with simple proof): If n = 4*k1, then f(n) = (n+1)/2, while otherwise f(n) = (n+1)/21.

Perhaps we implement then pd_vanderwaerden3k_fcl(k,n), which includes that additional unitclauses 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 parametervalues 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 "Atmostone 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 AMOrepresentations.

Another alternative generalises the treatment of the transversal case (all parameters except of one equal 2):

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).

One could use nonboolean 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.

B is here the number of variables *not* available to satisfy the trequirements.

The task is to maximise B; using as generalised transversal number tau(F) of an arbitrary satisfiable clauseset F the minimum of n(phi) for satisfying partial assignments phi, this corresponds to compute tau(F) = n  B.

Such generalised transversal problems (for arbitrary F) can be handled as above, by introducing the additional value to indicate variables not to be used.

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 tpart can be expressed using positive monosigned literals, and so monosigned literals are altogether enough here.


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 vdWproblems

The symmetrybreaking should happen as with the Greentao 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.