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.

Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre (Ed.), Theory and Applications of Satisfiability Testing – SAT 2016. (pp. 228-245). Springer.