The Ramsey number R(s,t) is the smallest integer n such that every red-blue coloring of the edges of the complete graph Kn contains a red clique of size s or a blue clique of size t. Ramsey numbers and their variants are some of the most famous numbers in combinatorics, yet computing even small exact values is notoriously difficult. Indeed, Erdős quipped that it would be more difficult for humans to compute the Ramsey number R(6,6) than to fend off an alien invasion. In this talk we highlight recent successes of Boolean satisfiability (SAT) solvers in Ramsey theory in both the arithmetic and graph theoretic settings.