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.