This paper presents a new diagnosis method for locating stuck-at and timing faults in the scan chains. Generating diagnostic patterns for locating the faulty scan cell is formulated as a Boolean Satisfiability (SAT) problem so that any state-of-the-art SAT solvers can be directly employed for diagnostic test generation. Several modeling techniques are introduced to facilitate the task. Experimental results show that the proposed approach can very precisely locate the faulty scan cell for almost all benchmark circuits with which we have experimented. In comparison with the existing approaches, the proposed method achieves better diagnosis resolution.