<span>The complexity of (classic Nintendo) games like Super Mario Bros., Donkey Kong Country and Metroid has been of interest to several researchers, which led to multiple articles introducing methods to prove complexity of such games. In a sequence of articles by Aloupis et al., results for several such games are given.
They introduced frameworks to show hardness of games for NP and PSPACE. Those frameworks combine the functionality of several components, so called gadgets. If these gadgets can be realized using a given games' mechanics, that game is NP- resp. PSPACE-hard. The frameworks, reducing from SAT resp. QSAT, specify game worlds given logic formulas. Playing the game represents the search for a satisfying assignment for the formula. If the player manages to reach the finish location, the formula is satisfiable.
There have been realizations of gadgets that turned out to be imperfect due to a too loose or even missing formal definition of the introduced gadgets, which allowed flaws to occur that led to incorrect results. The aim of this thesis is to refine the results in the article of Aloupis et al. by providing precise and detailed definitions. This is necessary to avoid flaws in the actual </span><span class="searchterm">implementations</span><span> of the frameworks for specific games. Also, the gadgets of the PSPACE-framework have been realized using the mechanics of Super Mario World, which proves this game to be PSPACE-hard and, performing a further step, PSPACE-complete.
As the complementary practical part of this thesis, both NP- and PSPACE-frameworks have been implemented in one actual game, based on the gadgets for Super Mario World. So the player runs through a game world that represents a (quantified) propositional formula and acts as solver to deliver results for SAT and QSAT problems.
Further, playing the game might (possibly) wake the player's interest in logic.</span>