Declarative pattern mining has seen significant advancements in recent years, particularly through the application of symbolic AI techniques on various data types, including binary, numerical, and graph data, etc. The core idea behind these approaches is to reformulate the task of pattern mining as a model enumeration problem in classical logic. These methods have been developed for their flexibility, allowing for easier incorporation of additional user constraints during the mining process. In this paper, we first present a symbolic approach for enumerating closed interval patterns using the propositional satisfiability problem (SAT). Then, by extending the SAT-based encoding of classical patterns with additional constraints to eliminate redundancy, our method proves to be highly efficient. Finally, experimental evaluations on various datasets demonstrate that our SAT-based framework is highly competitive with state-of-the-art approaches, even on large numerical databases.