patternMinor
Playing video games to solve SAT instances
Viewed 0 times
playingsatinstancesgamesvideosolve
Problem
This paper shows that computer games, such as Super Mario, are NP-hard, by reduction from SAT. It may be possible to use this reduction to help solve hard instances of SAT: use the reduction to construct a Super Mario level and let experienced gamers play it. In the worst case, it might take them exponentially long; but, in some cases, there may be heuristics that experienced gamers may be able to notice, and this may lead them to quick solutions.
The main problem with this scheme is that it is one-sided: if a satisfying assignment exists, then the gamers may find it; but if no such assignment exists, then they will not find any proof for it.
So my question is: is there a way to construct a video game for solving SAT instances, such that if the instance has a solution - a gamer will eventually find it (after possibly exponentially long time), and if the instance has no solution - a gamer will eventually find an evidence for it? Can such a game be useful for solving hard SAT instances?
The main problem with this scheme is that it is one-sided: if a satisfying assignment exists, then the gamers may find it; but if no such assignment exists, then they will not find any proof for it.
So my question is: is there a way to construct a video game for solving SAT instances, such that if the instance has a solution - a gamer will eventually find it (after possibly exponentially long time), and if the instance has no solution - a gamer will eventually find an evidence for it? Can such a game be useful for solving hard SAT instances?
Solution
No. The gamer will basically have to work out the SAT problem in their head.
Think of any video game puzzle you've solved that wasn't easy. You probably solved it by working out a simpler version of the problem and then solving that. If you "complexify" SAT into a video game level, the best way to solve the video game level will be to simplify it back into SAT, then solve SAT.
Example: Perhaps your game lets you create a level where you must collect all the coins from all the rooms but you can only enter each room once. (This is a Hamiltonian Path problem, which SAT can be transformed to). When you collect all the coins, the exit door opens. You then go to the exit door and finish the level. How would you solve it?
Well, you would start by exploring the level and drawing a map. Then you might simplify the map by drawing the rooms as circles and the connections as lines. Then you have to figure out a way to get from the start to the exit while going through every room... i.e. you have to solve the Hamiltonian path yourself. But how do you solve the Hamiltonian path? Well, you might reason that if you go this way, then you can't go that way, and if you go that way, you can't go this way, .... and write down a list of rules about where you can go. Then, you have to logically deduce a path that matches all the rules. Which is SAT. You're back to where you started except with a lot of useless extra work.
Think of any video game puzzle you've solved that wasn't easy. You probably solved it by working out a simpler version of the problem and then solving that. If you "complexify" SAT into a video game level, the best way to solve the video game level will be to simplify it back into SAT, then solve SAT.
Example: Perhaps your game lets you create a level where you must collect all the coins from all the rooms but you can only enter each room once. (This is a Hamiltonian Path problem, which SAT can be transformed to). When you collect all the coins, the exit door opens. You then go to the exit door and finish the level. How would you solve it?
Well, you would start by exploring the level and drawing a map. Then you might simplify the map by drawing the rooms as circles and the connections as lines. Then you have to figure out a way to get from the start to the exit while going through every room... i.e. you have to solve the Hamiltonian path yourself. But how do you solve the Hamiltonian path? Well, you might reason that if you go this way, then you can't go that way, and if you go that way, you can't go this way, .... and write down a list of rules about where you can go. Then, you have to logically deduce a path that matches all the rules. Which is SAT. You're back to where you started except with a lot of useless extra work.
Context
StackExchange Computer Science Q#130367, answer score: 3
Revisions (0)
No revisions yet.