Oliver Kullmann and his co-authors Marein Heule, and Victor Marek used SAT-solving techniques to solve a long standing open problem in Ramsey Theory known as the Boolean Pythagorean Triples Problem: It is impossible to divide the natural numbers into two parts such that none of the parts contains a Pythagorean triple, that is numbers a,b,c such that a^2+b^2=c^2. In fact, they found a smallest number N (namely N = 7825) such that the set {1,…,N} cannot be divided into two parts as described above.