Model checking is an important and practical formal method, which is widely used in verifying properties of concurrent systems. Wu's method is an efficient method in symbolic computation, and has succeeded in theorem proving. In this paper, we apply Wu's method to symbolic model checking. Briefly, we use Wu's method to calculate the polynomials which represent Boolean sets with BDDs in symbolic model checking. This is a new approach to symbolic model checking, and may be another successful application of Wu's method.