Abstract: Boolean Satisfiability is probably the most studied of combinatorial search problems and finds a number of applications in electronic design automation (EDA). In recent years, quite a few new and efficient SAT solvers have been developed, which make it possible solving much larger problem instances. We highlight the use of SAT algorithm to solve lots of EDA problems in such diverse areas as test pattern generation, symbolic model checking, combinational equivalence checking, and verification for RTL design. In addition, it is stressed how the useful information of circuit structure and specific problems to be solved is introduced to accelerate the SAT based algorithms.