Donkey Kong Country is NP-hard and PSPACE-hard
ProvedNintendo.dkc_hardTheorems 4.1-4.4 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): deciding whether a level of Donkey Kong Country is solvable is NP-hard and PSPACE-hard. The statement is a conjunction of the two explicit-level hardness predicates over the Donkey Kong Country level family of the worlds layer. First, there is a constant such that every 3-CNF formula has a level whose size is at most the constant times the square of the formula's size and which is solvable — some goal configuration reached alive from the start — exactly when the formula is satisfiable. Second, the same shape holds for quantified Boolean formulas with 3-CNF matrices and truth. The gadgets live in the game's own mechanics: barrels picked up from piles and thrown at the zingers in the row below, cannons that carry the Kong to their destinations, and the platforming moves between them.
Formalization Note The levels are levels of the worlds-layer Donkey Kong Country model, the Kong occupying a single cell; the two conjuncts are LevelHard3Sat and LevelHardTqbf over the same level family, and the size is the level-extent square.
import Mathlib import Definitions.Def_Nintendo_sat import Definitions.Def_Nintendo_game import Definitions.Def_Nintendo_worlds
namespace Nintendo
/-! Theorems 4.1-4.4 of the paper: Donkey Kong Country is NP-hard and PSPACE-hard. -/
theorem dkc_hard :
LevelHard3Sat dkcGame dkcStart dkcGoal dkcLevelSize ∧
LevelHardTqbf dkcGame dkcStart dkcGoal dkcLevelSize := by sorry
end Nintendo
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: two statements about the Donkey Kong Country level family of the worlds layer. First, there is a constant such that every 3-CNF formula has a level of the family whose size is at most the constant times the square of one more than the formula's size and which is solvable — some goal configuration reached alive from the start — exactly when the formula is satisfiable. Second, the same with quantified Boolean formulas: every quantified formula with a 3-CNF matrix has a level of at most the bounded size solvable exactly when the formula is true, the truth being as defined in the logic layer. The mechanics are those of the worlds-layer model: the Kong walks, jumps, and falls, picks up a barrel from a pile and throws it at the first zinger in the row below, and fires a cannon that carries him to its destination; zingers kill.