Boolean satisfiabilty (SAT) has many applications in the area of electronic design automation. In this project, a genuine multi-valued (MV) SAT solver, CAMA, is developed. Unlike encoding approaches, it directly deals with MV variables. We extended the major speed-up techniques used in state-of-the-art binary SAT solvers, such as two literal watch-based Boolean constraint propagation (BCP), conflict-based learning with identifying unique interception point (UIP), non-chronological back-tracking, and so on. An efficient conflict analysis algorithm-based MV SAT is developed. It makes the learned clauses as compact as possible, which has a dramatic impact on the overall performance. Finally, the performance of CAMA is compared to that of Chaff , one of the best binary SAT solvers known so far, using a one hot encoding scheme. Our experimental results show that for hard MV SAT problems, CAMA outperforms Chaff. And our analysis also reveals some fundamental reasons why a MV SAT solver has inherent advantages over a binary SAT solver.