Summary: The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we consider satisfiability in modal \(K(m)\), that is modal \(K\) with \(m\) modalities, and develop an algorithm, called \(K\mathcal{SAT}\) , on top of an implementation of the Davis-Putnam-Longemann-Loveland procedure. \(K\mathcal{SAT}\) is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system \(K\mathcal{KRIS}\). The experimental results show that \(K\mathcal{SAT}\) outperforms \(K\mathcal{KRIS}\) and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for \(K(m)\).