Human computing for EDA

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 staggering expertise in approximations, abstractions and heuristics as a means to sidestep 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 multiplayer puzzle game for SAT solving. FunSAT leverages 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.