Finite model generation can be regarded as a special case of the Constraint Satisfaction Problem (CSP). It has many applications in AI, computer science and mathematics. In the past two years, we built SEM, a System for Enumerating finite Models of first-order many-sorted theories. To the best of our knowledge, SEM outperforms any other finite model generation system on many test problems. The high performance of SEM relies on the following two techniques: (a) an efficient implementation of constraint propagation which requires little dynamic allocation of storage; (b) a powerful heuristic which eliminates many isomorphic partial models during the search. Our experimental results show that general purpose finite model generators are indeed useful in many applications. We also combine some local search techniques with backtracking techniques to obtain a very powerful model generator.