Stromquist’s conjecture. For any k>2, consider (2^k) - 1 points evenly spaced on a circle, and colour each of them arbitrarily blue or red. Then we can always find k points with the same colour that divide the circle into arcs proportional to 1 : 2 : 4 : . . . : 2^(k-1), but not necessarily in this order. The conjecture holds for k<8 and open in general. For each k the conjecture can be encoded in a SAT-formula in a straightforward way. For details see the paper TBD.
The SAT formulas for k=4,5,6,7 in DIMACS CNF format:
A simple python script to generate the formula for arbitrary k: Formula maker