Many a mathematical proof presents a symmetry argument to bypass an otherwise cumbersome case distinction. Similarly, combinatorial solvers can exploit symmetry to reduce the search space. This talk gives an overview of the techniques used in SAT solving to exploit symmetry properties of the problem at hand. It covers the topics of symmetry detection - typically via a transformation to graph automorphism though an argument for other approaches can be made; types of symmetry - different types have different needs; static and dynamic symmetry breaking - which remove symmetrical solutions from the solution set; symmetrical learning - which adds a symmetry rule to CDCL's proof system; and completeness of symmetry exploitation techniques - which arguably is the ultimate goal. The talk elaborates on the strengths and weaknesses of each technique, highlighting open questions and future research opportunities. As a common thread, we discuss the performance of each technique on the SAT encoding of the pigeonhole principle, which -in theory- can be decided in polynomial time using a symmetry argument. In practice however, efficiently deciding the SAT encoding of the pigeonhole principle remains a daunting challenge, as even after decades of research, none of the current techniques is able to fully detect and exploit the available symmetry.