Making a Game of Hardware Design 60
no-life-guy writes "Researchers at the University of Michigan have developed a web-game to harness the natural human abilities for electronic design automation (EDA). Arguing that people are still much better than computers in games of strategy and visualization, and that we'll do anything as long as it's fun, a group created FunSAT — a game where an average Joe gets to solve a Boolean satisfiability problem. Known as SAT, this problem is an important component in various hardware design tools from formal verification to IC layout to scheduling. The pilot version is a puzzle-like single-player Java app (akin to those addictive web-games), but the researchers envision that it can be extended to a multi-player (and, perhaps, replace WoW as the favorite past-time of the millions), so anybody can be a hardware designer. If anything, this is definitely a great learning tool."
Re:Not so fun (Score:1, Informative)
Yes, I made it to level 3 and decided that the computer could enumerate (and evaluate) all choices faster than I could ever figure out the interactions.
Re:Not so fun (Score:3, Informative)
Exactly, and also taking into account that boolean operations are really, really, really fast on computers. All of those levels would had been solved faster than blink of an eye by computer, and you couldn't compete even if every person on this planet would play that game all the time.
doubts (Score:2, Informative)
I have my doubts that humans can solve these puzzles better than computers.
I myself have programmed several SAT solvers, which can solve problems with thousands of variables and constraints in seconds. And that was with just a little bit of hobby programming in python. Really good solvers like MINISAT (Google it if you're interested) can solve problems with hundreds of thousands of constraints in milliseconds.
Humans do have better visual pattern recognition skills than computers, but this helps us only if there are easily recognizable visible patterns in the puzzle. I've played with the game, but the relations between variables and constraints shown in the game are not very helpful.
I think a better approach is to use advanced visualization and exploration techniques, so humans can help simplify problems for computers to solve.
Still, the game does nicely show the difficulties in solving the SAT problem.
Re:Not so fun (Score:2, Informative)
Satisfiability, Sudoku, and NP-completeness (Score:3, Informative)
If I'm not mistaken, the boolean satisfiability problem is NP-complete. In fact, in 1971, Stephen Cook established a direct proof of its NP-completeness [wikipedia.org], which basically introduced the whole idea of NP-complete problems to theoretical computer science. Well, Sudoku is yet another game that is basically NP-complete as well [u-tokyo.ac.jp] (PDF link), and as might expected from their both being NP-complete, Sudoku problems are reducible to SAT problems (see here [umass.edu], also a PDF link), and presumably vice-versa. My guess is that perhaps the same people who get kicks out of solving Sudoku puzzles might have almost as much fun with this game as well.