The TQBF framework: the door-and-quantifier protocol is solvable exactly when the quantified formula is true
DisprovedNintendo.fw_tqbfThe TQBF framework of Section 2.2 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): the abstract game whose levels are built from a quantified Boolean formula by the paper's quantifier gadget and its door system, the doors being traversable in only one direction at a time so that every universal quantifier must be tried both ways. The theorem states the framework's PSPACE-hardness shape: there is a constant such that, for every quantified formula with a 3-CNF matrix, 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 true exactly when a goal configuration of the level is reachable from its start. The protocol of the level: the quantifier row appends one free choice per existential quantifier and one forced truth per universal quantifier on the forward pass; the test path checks every clause; when a universal quantifier remains, the player returns to the last universal position, flips it to falsehood, and re-walks the suffix; the finish is reachable exactly when every universal has been tried both ways and every clause was satisfied on every pass.
Formalization Note The framework level is defined in the game layer as an explicit configuration protocol (start, row, test, back, and finish states); the door system of the paper is embodied in the back protocol's forced re-walk of the suffix after each flip. The truth of the quantified formula is as defined in the logic layer, the prefix read outermost first, and the hardness predicate is HardTqbf.
import Mathlib import Definitions.Def_Nintendo_sat import Definitions.Def_Nintendo_game import Definitions.Def_Nintendo_worlds
namespace Nintendo /-! Section 2.2 of the paper: the TQBF door framework. -/ theorem fw_tqbf : HardTqbf qfGame qfStart qfGoal qfLevelSize := 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 quantified Boolean formula with a 3-CNF matrix, 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 true 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: a quantifier row in which existential quantifiers contribute free choices and universal quantifiers contribute forced truths on the forward pass, a test path over the clauses, and a back protocol that returns to the last universal position, flips it to falsehood, and re-walks the suffix, so that the finish is reachable only after every universal quantifier has been visited in both truth values. The truth of the quantified formula is as defined in the logic layer, the prefix read outermost first.