SAT-based decision procedures for normal modal logics: a theoretical framework