 Recent advances in SAT hybrid strategies coupled with supercomputing power has allowed a team of three computing scientists to solve the Boolean Pythagorean Triples Problem, a long-standing open question in Ramsey Theory: Can the set {1, 2,...} of natural numbers be divided into two parts with no part containing a triple (a, b, c) such that a2 + b2 = c2? Heule, Kullmann &amp; Marek 2016 proved that this cannot be done by showing that the set {1, 2, … , n} can be so partitioned for n = 7824 but that this is impossible for n ≥ 7825. Expressing this deceptively simple question as a SAT problem required close to 38,000 clauses and 13,000 variables with about half of these going to represent that the problem is satisfiable when n = 7824 and the other half to represent that it is not when n = 7825; of the two, proving the latter was far more challenging since it demanded a proof of unsatisfiability, i.e. that no such partition exists. A naïve brute-force approach considering all 27825 possible two-part partitions was clearly out of the question and the problem was attacked by using “clever” algorithms within a multi-stage SAT-based framework for solving hard problems in combinatorics, consisting of five phases: Encode (encoding the problem as SAT formulas), Transform (optimizing the encoding using clause elimination and symmetry breaking techniques), Split (dividing the problem effectively into subproblems using splitting heuristics), Solve (searching for satisfying assignments or their lack thereof using fast processing), and Validate (validating the results of the earlier phases). Of special importance was the application of cube-and-conquer, a hybrid SAT strategy particularly effective for hard combinatorial problems. The strategy combines look-ahead with conflict-driven clause-learning (CDCL), with the former aiming to construct small binary search trees using global heuristics and the latter aiming to find short refutations using local heuristics.