Both my Alma Maters had courses that used these extensively, and also planners like (Pl|Tr|L)ingeling. We also covered reducability and SAT in multiple courses in both.

These should also be taught in an advanced PL course, e.g liquid, dependent etc types.