SAT-Based Decision Procedures for Classical Modal Logics