> I definitely recall doing reductions to SAT in Algorithms courses.

> It was introduced only in the context of Cook's theorem, as the problem you needed to reduce other problems to in order to show NP-completeness.

Are you referring to reductions from SAT, or to SAT? You seem to be mentioning both?