I am not sure how practical this is, but given that verification takes place over months in chip design, this could well be interesting.
A bunch of people from the University of Michigan have created a web game, which tries to pose on-chip satisfiability (SAT) problems as a game. However, reading its description makes it sound more a DFT problem.
Essentially, each dot on a grid is controllable, which may or may not toggle a dot’s observability. Essentially, what they are doing is the exact opposite of this paper: Satisfiability-Based Automatic Test Program Generation and Design for Testability for Microprocessors. Rather than use a automatic solver for test-pattern generation, they are using humans to solve these puzzles.
I would not call it a true webgame sat solver - because that would entail a game in which you have to generate a combination where two puzzles dont match each other.
I am not entirely too sure about the objective of this study - unlike Amazon Mechanical Turk or Google Image Labeler, both of which are online initiatives which incentivizes (in the form of fun or financial compensation), small tasks which can be combined to create a meaningful whole result.
There is a technical basis for this question - unlike tagging images, test pattern generation cannot really be partitioned. If indeed it could be, then you could simply multi-thread them (or run something like MapReduce to enable distributed computing). A large enough problem, and you will have lost your ability to attract people, willing to solve the problem.
So, my conclusion is that this is an impractical, highly speculative academic exercise.