Formula Game¶

Evaluate a closed quantified Boolean formula as a perfect-information contest in which Existential and Universal assign their variables in prefix order and truth is equivalent to Existential having a winning strategy.

Version: v3 · 2026-09-19 · History
Domain-specific #: 1868
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Theoretical Computer Science, Computational Complexity → Computer Science & Software Engineering
Aliases: QBF game, FORMULA-GAME

Core Idea¶

The Formula Game turns the truth of a closed quantified Boolean formula into a two-player, finite, perfect-information game. Write the formula in prenex form as a sequence of quantifiers followed by a propositional matrix. Moving from left to right, player E chooses the truth value of each existentially quantified variable and player A chooses each universally quantified variable. After every variable is assigned, E wins exactly when the matrix evaluates to true; A wins otherwise.

This game is not merely an analogy. It is an operational semantics for the quantifiers. An existential quantifier asks whether E has some choice that succeeds against the continuation. A universal quantifier asks whether the continuation succeeds for every choice A can make.

How would you explain it like I'm…

The Switch-Flipping Game

Two players take turns flipping switches to ON or OFF, in a set order. Each switch belongs to one player. When every switch is set, a light either turns on or stays off. One player wins if the light is on, and the other wins if it's off. The Formula Game asks: can the light-on player always win, no matter what the other does?

There-Is versus For-Every Game

Some logic puzzles say things like "there is some choice for x such that, for every choice of y, the statement works." The Formula Game turns this into a game between two players. Player E picks the "there is some" choices, and player A picks the "for every" choices, going in order from left to right. When all choices are made, E wins if the statement comes out true, and A wins if it comes out false. The puzzle is true exactly when E has a plan that always wins, no matter what A does.

Quantifier Game Semantics

A quantified Boolean formula has a list of quantifiers (∃x, ∀y, ...) followed by a true/false expression. The Formula Game reads that list left to right: player E chooses true/false for each ∃ variable and player A for each ∀ variable. After everything is set, E wins if the expression is true. The formula is true if and only if E has a winning strategy, so 'there exists' means E can pick well and 'for all' means E must survive every pick by A. A key difference from ordinary satisfiability is that E's later choices may depend on what A already chose, so the answer is a strategy, not one fixed assignment.

Take a closed QBF in prenex form, Q₁x₁ … Qₙxₙ φ, where φ is a propositional matrix. The Formula Game is a finite, perfect-information game: moving left to right, E assigns the ∃-variables and A assigns the ∀-variables. After all n assignments, E wins if and only if φ evaluates to true. This is more than an analogy. It is an operational semantics for the quantifiers. ∃ means E has some move that succeeds against the rest of the game, and ∀ means the rest succeeds for every move A can make. So the QBF is true if and only if E has a winning strategy. In complexity theory, FORMULA-GAME is the set of encodings where E wins. It coincides with TQBF and is PSPACE-complete. The game makes alternation explicit: a witness is a strategy whose existential choices may depend on earlier universal moves, not one assignment fixed in advance.

Scope of Application¶

Formula Game belongs to mathematical logic, complexity theory, QBF solving, and the teaching of alternation. It is used as the canonical source problem in reductions showing that planning, puzzles, and two-player perfect-information games are PSPACE-hard. The game presentation also explains why QBF models policies and reactive choices: existential decisions can depend on earlier universal uncertainty but not on future moves.

The identity is narrow by design. Broader game semantics extends verifier/falsifier play to first-order, modal, fixed-point, and program logics; those systems have different arenas and winning conditions. This node retains the Boolean domain and closed prefix game.

Clarity¶

For ∀x ∃y (x ↔ y), A chooses x first and E observes that choice before choosing y=x; E has a winning strategy, so the formula is true. For ∃y ∀x (x ↔ y), E must commit to y before seeing x; A chooses the opposite value and wins, so the formula is false. The propositional matrix is the same, but information order reverses the result.

Manages Complexity¶

The game compresses recursive quantifier semantics into a familiar adversarial procedure. Rather than repeatedly expanding ∀ into conjunction and ∃ into disjunction, one can inspect a game tree: E-nodes require some winning child; A-nodes require all children to remain winning for E.

It also provides a reduction interface. A target problem is PSPACE-hard when a formula game can be encoded so that E's choices correspond to one player's moves, A's choices correspond to the opponent or environment, and satisfaction corresponds to reaching a winning target.

Abstract Reasoning¶

Backward induction. Label terminal assignments by the matrix truth value. At an existential node, label true if at least one child is true; at a universal node, label true only if every child is true. The root label is the QBF truth value.

Strategy extraction. At each winning existential node, record a true child. The collection is an E strategy, potentially represented as Boolean functions of preceding universal variables.

Knowledge Transfer¶

The full abstraction transfers among QBF instances, solvers, proof systems, and complexity reductions. Outside these settings, “an existential player versus a universal player” can illuminate adversarial planning, but it is only a literal Formula Game when the choices encode a closed Boolean quantifier prefix and the terminal matrix determines the winner.

The portable residue belongs to Quantifier, Zero Sum Game, contingent strategy, and alternation. The domain-specific package fixes their precise Boolean-logic coupling.

Relationships to Other Abstractions¶

Current abstraction Formula Game Domain-specific

Parents (2) — outgoing typed relations

Formula Game is a kind of Zero Sum Game Prime

zero_sum_game: truth for E is falsity for A, with no jointly preferred outcome.
Formula Game includes Quantifier Prime

quantifier: existential and universal quantifiers allocate control and define branching semantics.

Hierarchy paths (2) — routes to 2 parentless roots

Formula Game → is a kind of Zero Sum Game → presupposes Game-Theoretic Strategy → is a decomposition of Function (Mapping)

Show alternative path (1)

Neighborhood in Abstraction Space¶

Formula Game sits in a sparse region of the domain-specific corpus (89^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Game-Theoretic Models & Paradoxes (38 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-25