3.1.8. cnfgen.families.ramsey module

CNF Formulas for Ramsey-like statements

PythagoreanTriples(N)

There is a Pythagorean triples free coloring on N

The formula claims that it is possible to bicolor the numbers from 1 to \(N\) so that there is no monochromatic triplet \((x,y,z)\) so that \(x^2+y^2=z^2\).

Parameters:

N : int

size of the interval

Raises:

ValueError

Parameters are not positive

TypeError

Parameters are not integers

References

[1]	M. J. Heule, O. Kullmann, and V. W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. arXiv preprint arXiv:1605.00723, 2016.

RamseyNumber(s, k, N)

Ramsey number r(s,k) > N

This formula, given \(s\), \(k\), and \(N\), claims that there is some graph with \(N\) vertices which has neither independent sets of size \(s\) nor cliques of size \(k\).

It turns out that there is a number \(r(s,k)\) so that every graph with at least \(r(s,k)\) vertices must contain either one or the other. Hence the generated formula is satisfiable if and only if

\[r(s,k) > N\]

Parameters:

s : int

independent set size

k : int

clique size

N : int

number of vertices

Returns:

A CNF object

Raises:

ValueError

Parameters are not positive

TypeError

Parameters are not integers

VanDerWaerden(N, k1, k2, *ks)

Formula claims that van der Waerden number vdw(k1,k2,k3,k4,…) > N

Consider a coloring the of integers from 1 to \(N\), with \(d\) colors. The coloring has an arithmetic progression of color \(c\) of length \(k\) if there are \(i\) and \(d\) so that all numbers

\[i, i+d, i+2d, \ldots, i +(k-1)d\]

have color \(c\). In fact, given any number of lengths \(k_1\), \(k_2\),…, \(k_C\), there is some value of \(N\) large enough so that no matter how the integers \(1, \ldots, N\) are colored with \(C\) colors, such coloring must have one arithmetic progression of color \(c\) and length \(k_c\).

The smallest \(N\) such that it is impossible to avoid the arithmetic progression regardless of the coloring is called van der Waerden number and is denotes as

\[VDW(k_1, k_2 , \ldots, k_C)\]

The formula, given \(N\) and :math`k_1`, :math`k_2` , ldots, :math`k_C`, is the CNF encoding of the claim

\[VDW(k_1, k_2 , \ldots, k_C) > N\]

which is expressed, more concretely, as a CNF which forbids, for each color \(c\) between 1 and \(C\), all arithmetic progressions of length \(k_C\)

Parameters:

N : int

size of the interval

k1: int

length of the arithmetic progressions of color 1

k2: int

length of the arithmetic progressions of color 2

*ks : optional

lengths of the arithmetic progressions of color >2

Returns:

A CNF object

Raises:

ValueError

Parameters are not positive

TypeError

Parameters are not integers