Electronic design automation is a field replete with challenging ? and often intractable ? problems to be solved over very large instances. As a result, the field of design automation has developed a ng expertise in approximations, abstractions and heuristics as a means to side-step the NP-hard nature of these problems. Approximations and heuristics are at heart a natural application of human reasoning. In this work we propose to harness human potential to solve some of these problems. Specifically, we propose FunSAT, a massively multi-player puzzle game for SAT solving. FunSAT s visual pattern recognition skills, abstract perception and intuitive strategy skills of humans to solve complex SAT instances. Players are motivated by the puzzle-solving challenges of the game and by its social interaction aspects. Categories and Subject Descriptors