The 3-SAT framework: a level of Start, Variable, Clause, Check, and Crossover gadgets is solvable exactly when the formula is satisfiable
DisprovedNintendo.fw_satThe 3-SAT framework of Section 2.1 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): the abstract game whose levels are built from a 3-CNF formula by the paper's Start, Variable, Clause, Check, and Crossover gadgets. The theorem states the framework's NP-hardness shape: there is a constant such that, for every 3-CNF formula, the size of the framework level built from the formula is at most the constant times the square of the formula's size, and the formula is satisfiable exactly when a goal configuration of the level is reachable from its start by the legal steps. The protocol of the level: the player sets the variables one at a time; after each choice the player may visit the clause gadgets, a visit unlocking a clause exactly when the chosen literal occurs in it, the crossover gadgets routing the paths without interference; after the last variable the player walks the check path, whose clause gates open exactly when the corresponding clause has been unlocked.
Formalization Note The framework level is defined in the game layer as an explicit configuration protocol (start, variable-setting, literal, check, and finish states) rather than as a grid of tiles; the crossover gadgets of the paper, whose function is to let paths cross, are embodied in the protocol's freedom to visit clause gadgets between any two variable choices. The size is the square of the numbers of variable and clause gadgets, and the hardness predicate is Hard3Sat.
import Mathlib import Definitions.Def_Nintendo_sat import Definitions.Def_Nintendo_game import Definitions.Def_Nintendo_worlds
namespace Nintendo /-! Section 2.1 of the paper: the 3-SAT framework. -/ theorem fw_sat : Hard3Sat frameworkGame fwStart fwGoal fwLevelSize := by sorry end Nintendo
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: there is a constant such that, for every 3-CNF formula, the size of the framework level built from the formula is at most the constant times the square of one more than the formula's size, and the formula is satisfiable exactly when some finish configuration of the level is reachable from the start configuration. The framework level is the protocol defined in the game layer: variable-setting states in which the player chooses one truth value per variable, literal states in which visiting a clause state unlocks that clause exactly when the chosen literal occurs in it, and a check path whose gates open exactly when the corresponding clause has been unlocked. No hypotheses appear beyond the formula being 3-CNF.