Playing video games to solve SAT instances

Question

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?

Answer 1

Given a SAT instance A, another SAT instance B can be constructed such that if it is found satisfiable the satisfying assignment proves the unsatisfiability of A. But the proof is one-sided; if B is found to be unsatisfiable that in itself does not prove that A is satisfiable.

This is accomplished by crafting B's clauses such that its variable assignments specify the inference steps of some proof system known to be sound and complete for propositional logic and whose starting state is A. Using the resolution rule as an example proof system, if there are a series of steps that starts with A and ends with the empty clause then B is satisfiable and the steps prove that A is unsatisfiable.

The one-sidedness of the proof comes from the fact that the length of the proof is limited by the number of inference steps that can be encoded in the variables and clauses of B, which is limited by the number of variables and clauses in B. If B has too few variables and clauses to write a valid proof of A's unsatisfiability then B's unsatisfiability says nothing about A's satisfiability, it only says that any proof of A's unsatisfiability is longer than what can be encoded in any satisfying assignment of B.

For the best chance at proving A's unsatisfiability with a feasibly-sized B, B should encode a proof system strong enough to encode short proofs of A type problems. As an example, using the resolution rule alone would be a poor choice for pigeonhole type problems since it is known that such problems require exponentially-sized resolution proofs. Using the resolution rule along with Tseitin's extension rule is adequate to write polynomially-sized unsatisfiability proofs of such problems.

So to use video games to solve your problem you could take your target SAT problem A and construct another SAT instance B as described above, then reduce both to Super Mario Bros. games. If game experts win the game reduced from A, then A is satisfiable. If experts win the game reduced from B, then A is unsatisfiable. The bad news is that since we don't know if NP = coNP, B's size might need to be exponentially larger than A to guarantee you will get a definitive answer of unsatisfiability.

Answer 2

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.