Thursday, August 27, 2009

Satisfiability Problems Online Game

There's an article in the IEEE Spectrum regarding Crowdsourcing the Complexities of Electronic Design Automation, which talks about a game called FunSAT that could benefit chip makers in improving their designs. Humans can help at this stage because these kind of problems are difficult for computers to solve. The game simulates satisfiability problems (SATs), and presents the user with a set of buttons and bubbles, where the buttons can have a value of true, false, or unassigned, and the bubbles, which represent clauses, can be satisfied, unsatisfied, or undetermined. The goal is to turn all bubbles green. For a bubble to turn green, at least one of the literals in the corresponding clause must be true. If all of the literals are false, the bubble will turn red; otherwise, it will be gray.

Why are satisfiability problems important? Because they aid in the design verification stage of chip design. "For example, they are used to find out what input combinations result in exposing a potential bug in the design. If no such combination exists, then the designers don’t have to worry about that particular bug."

"Modern satisfiability solvers tend to prioritize and limit their searches to a few paths that look promising. By using this method, however, they don’t always find the best configuration. What humans lack in brute-force speed, they tend to make up for with pattern recognition and intuition—the ability to know a good move without being able to explain why it’s good. And, most important, they like to play games."

No comments: