Explicit modal logic was introduced by S. Artemov. Whereas the traditional modal logic uses atoms ☐F with a possible semantics “F is provable”, the explicit modal logic deals with atoms of form t:F, where t is a proof polynomial denoting a specific proof of a formula F. Artemov found the explicit modal logic $ \mathcal{L}\mathcal{P} $ \mathcal{L}\mathcal{P} in this new format and built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation in K. Gödel’s modal provability calculus $ \mathcal{S}4 $ \mathcal{S}4 . In this paper we study the complexity of $ \mathcal{L}\mathcal{P} $ \mathcal{L}\mathcal{P} as well as the complexity of explicit counterparts of the modal logics $ \mathcal{K}, \mathcal{D}, \mathcal{T}, \mathcal{K}\mathcal{A}, \mathcal{D}4 $ \mathcal{K}, \mathcal{D}, \mathcal{T}, \mathcal{K}\mathcal{A}, \mathcal{D}4 found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class ∑₂ ^p 2 of the polynomial hierarchy. Similar problem for the original modal logics is known to be PSPACE-complete. Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics.