← back to the atlas

d4-conf-atal-2016-0309 (d4-conf-atal-2016-0309)

Answer: Polynomial-time solvable in \(m,\tau,T,L\), including the exact initial value and polynomial-size circuits for one pair of SPE behavioral strategies.

The anchor (named result in the paper)

Lemma 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateTwo histories have the same value if they have selected the same players to play (but may be in different orders) and Team 1 won the same number of rounds. Based on the above lemma, the histories can be parti- tioned to equivalence classes, such that each equivalence class corresponds to a four-tuple (k, X, Y, w): k is a num- ber in [T ] which denotes the number of past rounds; X is a subset of A of size k; Y is a subset of B of size k; X, Y denote the players that have played; w is a number in [k] which denotes how many rounds Team 1 has won so far.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a fixed horizon \(T\), finite type sets \(S_A,S_B\), positive rational masses \(\mu_t,\nu_u\) summing to one, rational match probabilities \(p_{tu}\), and terminal zero-sum utility \(U(w)\), where each supported type has at least \(T\) interchangeable representatives, compute the exact SPE value and behavioral strategies when both teams choose a type simultaneously each round, use a fresh representative, observe the result, and adapt.

Packaged proof task (what the prover saw — nothing else)

Each team is a nonatomic society given by its support: a nonempty finite list of types with positive binary rational masses, summing to one separately for each team. Write \(m=\max\{|S_A|,|S_B|\}\) and \(\tau=|S_A|+|S_B|\); \(\tau\) counts supported types, not possible types.
The input includes a positive integer horizon \(T\), rational probabilities \(p_{tu}\in[0,1]\), and an explicit rational utility table \(U(0),\ldots,U(T)\) satisfying \(U(w)+U(T-w)=0\). Let \(L\) be the total binary input length.
Every supported type supplies at least \(T\) interchangeable representatives. Each round, both teams simultaneously choose any supported type and use a fresh representative; there are no constraints tying selection probabilities to masses, and individual selection does not deplete mass.
Conditional on the chosen types \(t,u\) and any prior history, Team A wins with probability \(p_{tu}\), otherwise Team B wins. Both choices and the outcome become public; all input data are common knowledge.
If Team A wins \(w\) rounds, terminal payoffs are \(U(w)\) and \(-U(w)\). Behavioral strategies assign distributions over supported types to public histories; compute the exact initial SPE value and one pair of SPE behavioral strategies, represented by circuits evaluating those distributions at any history.

Is this exact SPE computation problem solvable in polynomial time in \(m,\tau,T,L\), or is it NP-hard?

For finite teams whose players can each play once, histories with identical sets of used players and the same win count have equal values; backward induction over these classes computes SPE values and strategies. [Source](https://www.ifaamas.org/Proceedings/aamas2016/pdfs/p14.pdf)
No result settling the specified nonatomic problem was identified in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The specified exact SPE computation problem is polynomial-time solvable in \(m,\tau,T,L\). The algorithm computes two rational matrix-game equilibria, fills a table with \(O(T^2)\) entries, and constructs polynomial-size circuits for the behavioral strategies.

The proof accommodates arbitrary utility tables satisfying the stated hypotheses; monotonicity is unnecessary.

1. Two matrix games suffice

Enumerate the supports as \(S_A=\{1,\ldots,a\}\) and \(S_B=\{1,\ldots,b\}\), and write \(P=(p_{ij})\). Let \(\Delta_a,\Delta_b\) denote their probability simplices. For any real \(a\times b\) matrix \(M\), define its zero-sum value, with A maximizing, by

\(v(M)=\max_{x\in\Delta_a}\min_{y\in\Delta_b}x^{\mathsf T}My=\min_{y\in\Delta_b}\max_{x\in\Delta_a}x^{\mathsf T}My.\)

The equality and existence of optimal distributions follow from the finite zero-sum minimax theorem.

Compute optimal distribution pairs \((x^+,y^+)\) for \(P\) and \((x^-,y^-)\) for \(-P\). Define

\(\alpha=v(P),\qquad \beta=-v(-P).\)

Because every entry of \(P\) lies in \([0,1]\), both \(\alpha\) and \(\beta\) lie in \([0,1]\).

Let \(J\) be the all-ones \(a\times b\) matrix. For arbitrary real numbers \(c,d\),

\(v(cJ+dP)=\begin{cases}c+d\alpha,&d>0,\\c,&d=0,\\c+d\beta,&d<0.\end{cases}\)

Moreover, an optimal distribution pair is \((x^+,y^+)\) when \(d>0\), \((x^-,y^-)\) when \(d<0\), and any pair when \(d=0\).

Justification. For every pair of distributions, \(x^{\mathsf T}Jy=1\). Adding \(cJ\) therefore adds the constant \(c\) to every expected payoff. Multiplication by a positive scalar preserves optimal distributions and scales the value.

If \(d<0\), then \(dP=(-d)(-P)\), where \(-d>0\). Hence the optimal pair for \(-P\) remains optimal, and

\(v(cJ+dP)=c+(-d)v(-P)=c+d\beta.\)

The negative case is essential because the utility table need not be monotone.

2. Backward recursion

A state is a pair \((k,w)\), where \(k\) rounds have been completed and A has won \(w\) of them. Its domain is \(0\leq w\leq k\leq T\).

At every nonterminal history, every supported type remains available. Indeed, fewer than \(T\) representatives have been used in total, while each supported type supplies at least \(T\). The masses impose no selection restrictions. Thus the available type choices do not depend on earlier choices.

Define numbers \(V_{k,w}\) backward, beginning with

\(V_{T,w}=U(w)\qquad(0\leq w\leq T).\)

Suppose the entries for round count \(k+1\) have been defined. Put

\(c_{k,w}=V_{k+1,w},\qquad d_{k,w}=V_{k+1,w+1}-V_{k+1,w}.\)

If the current choices are \(i,j\), their expected continuation value is

\(M^{k,w}_{ij}=p_{ij}V_{k+1,w+1}+(1-p_{ij})V_{k+1,w}=c_{k,w}+d_{k,w}p_{ij}.\)

Consequently, define

\(V_{k,w}=\begin{cases}c_{k,w}+d_{k,w}\alpha,&d_{k,w}>0,\\c_{k,w},&d_{k,w}=0,\\c_{k,w}+d_{k,w}\beta,&d_{k,w}<0.\end{cases}\)

At every history with state \((k,w)\), prescribe the pair \((x^+,y^+)\) if \(d_{k,w}>0\), the pair \((x^-,y^-)\) if \(d_{k,w}<0\), and a fixed pair of pure supported types if \(d_{k,w}=0\).

These prescriptions define behavioral strategies at every nonterminal public history.

3. Proof of subgame perfection

We prove by backward induction the following stronger assertion: at every history with state \((k,w)\), the prescribed strategy for A guarantees expected payoff at least \(V_{k,w}\) against every behavioral strategy for B, and the prescribed strategy for B guarantees A’s expected payoff at most \(V_{k,w}\) against every behavioral strategy for A.

This assertion quantifies over arbitrary history-dependent deviations.

At \(k=T\), the payoff is \(U(w)=V_{T,w}\), so both guarantees hold.

Now fix a history with state \((k,w)\), assuming both guarantees hold at every successor history.

First, suppose B follows the prescribed strategy and A deviates arbitrarily. Let \(x\) be A’s distribution at the current history, and let \(y^*\) be B’s prescribed distribution.

Conditional on the current choices and outcome, the induction hypothesis bounds A’s continuation payoff above by \(V_{k+1,w+1}\) after an A win and by \(V_{k+1,w}\) after an A loss. Therefore A’s expected payoff is at most

\(x^{\mathsf T}M^{k,w}y^*.\)

By Section 1, \(y^*\) is an optimal minimizing distribution for \(M^{k,w}\). Thus, for every \(x\),

\(x^{\mathsf T}M^{k,w}y^*\leq v(M^{k,w})=V_{k,w}.\)

This proves B’s guarantee.

Conversely, suppose A follows its prescribed strategy and B deviates arbitrarily. Write \(x^*\) for A’s prescribed distribution and \(y\) for B’s current distribution. The continuation guarantees for A give an expected payoff at least

\((x^*)^{\mathsf T}M^{k,w}y.\)

Because \(x^*\) is an optimal maximizing distribution,

\((x^*)^{\mathsf T}M^{k,w}y\geq v(M^{k,w})=V_{k,w}.\)

This proves A’s guarantee and completes the induction.

When both teams follow the prescribed strategies, the two guarantees force expected payoff \(V_{k,w}\). Neither team can profitably deviate in any subgame. Hence the constructed pair is an SPE, and the exact initial value is \(V_{0,0}\).

In particular, histories with equal round count and win count have equal values, regardless of their previous type choices.

4. Exact computation and bit complexity

Computing the two matrix-game equilibria

We use the standard theorem that rational linear programming admits exact optimization in time polynomial in the binary encoding length. Optimal rational solutions can be chosen with polynomial encoding length. These facts follow from polynomial-time LP algorithms and the determinant bounds for basic feasible solutions; see [Goemans’s linear programming notes](https://ocw.mit.edu/courses/6-854j-advanced-algorithms-fall-2008/908fe54d659623efadda2d033b895caf_notes_lp.pdf).

For completeness, the applicable LPs have especially simple hypotheses. For each \(M\in\{P,-P\}\), solve the maximizing-player LP

\(\max z\quad\text{subject to}\quad x\in\Delta_a,\quad \sum_{i=1}^{a}x_iM_{ij}\geq z\ \text{for every }j,\quad -1\leq z\leq1,\)

and the minimizing-player LP

\(\min z\quad\text{subject to}\quad y\in\Delta_b,\quad \sum_{j=1}^{b}M_{ij}y_j\leq z\ \text{for every }i,\quad -1\leq z\leq1.\)

All coefficients are rational. The feasible regions are nonempty and compact: any simplex distribution with \(z=-1\) is feasible for the maximizing LP, and any simplex distribution with \(z=1\) is feasible for the minimizing LP. Since entries of \(M\) lie in \([-1,1]\), the bounds on \(z\) do not alter the optimal values. Minimax, equivalently LP duality, identifies their common value and optimal distributions.

Each LP has \(O(m)\) variables and \(O(\tau)\) constraints, with polynomial input length. Thus both equilibrium pairs and both values are computable exactly in polynomial time. Let \(B\) be a polynomial bound in \(m,\tau,L\) on the bit length of each resulting rational number.

Controlling all continuation denominators

A polynomial number of rational operations alone would not suffice; their operands must also have polynomial bit length. Here that follows from a common-denominator construction.

Let \(R\) be the product of the positive denominators of the input utilities. Then

\(RU(w)\in\mathbb Z\quad\text{for every }w,\qquad \log_2R=O(L).\)

Choose a common denominator \(Q\) for \(\alpha,\beta\), for example the product of their positive denominators. Write

\(\alpha=A_0/Q,\qquad \beta=B_0/Q,\)

where \(A_0,B_0\) are integers satisfying \(0\leq A_0,B_0\leq Q\), and \(\log_2Q=O(B)\).

We claim that every continuation value has the representation

\(V_{k,w}=\dfrac{N_{k,w}}{RQ^{T-k}},\qquad N_{k,w}\in\mathbb Z.\)

At \(k=T\), set \(N_{T,w}=RU(w)\). Suppose the representation holds at \(k+1\). The two successor values have the same denominator, so the sign of \(d_{k,w}\) is exactly the sign of

\(N_{k+1,w+1}-N_{k+1,w}.\)

Choose \(C=A_0\) for a positive difference, \(C=B_0\) for a negative difference, and \(C=0\) for a zero difference. The recurrence becomes the integer calculation

\(N_{k,w}=(Q-C)N_{k+1,w}+C N_{k+1,w+1}.\)

Dividing by \(RQ^{T-k}\) gives precisely the recurrence in Section 2, proving the claim.

Set \(H=\max_{0\leq w\leq T}|U(w)|\). Every recurrence is a convex combination of its two successor values, because \(0\leq C/Q\leq1\). Inductively,

\(|V_{k,w}|\leq H,\qquad |N_{k,w}|\leq HRQ^{T-k}.\)

The input encoding gives \(\log_2(1+H)=O(L)\). Therefore every numerator used by the algorithm has bit length

\(O\bigl(1+L+TB\bigr).\)

There are \(O(T^2)\) table entries, and each requires a constant number of integer comparisons, additions, and multiplications on polynomial-size integers. The entire table, including \(V_{0,0}\), is therefore computable in polynomial bit time.

5. Polynomial-size strategy circuits

During the backward computation, store the sign of \(d_{k,w}\) for each nonterminal state. This table has \(O(T^2)\) entries.

Use a fixed-length history encoding consisting of its length \(k\) and at most \(T\) padded round records. A circuit computes \(w\) by counting A’s wins among the first \(k\) records. It then looks up the stored sign for \((k,w)\) and outputs:

Represent each probability by its binary numerator and positive denominator, padded to a common polynomial width. Counting, table lookup, and selecting among these constant vectors all admit Boolean circuits of polynomial size, constructible in polynomial time.

The circuits therefore evaluate the exact behavioral distributions at every nonterminal history. Their behavior on terminal or malformed encodings can be assigned arbitrarily.

The explicit utility table contains \(T+1\) rational entries, so \(T=O(L)\). Thus the algorithm is polynomial in the full binary input length as well as in the requested parameters.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

The output resolves the assigned problem in substance: the exact initial SPE value and circuits for one pair of SPE behavioral strategies are computable in polynomial time. The equilibrium argument, denominator bounds, and circuit construction are sound. There is one minor wording error in the justification that representatives remain available.

1. Scope and assumptions

The proof addresses the specified model:

Ignoring the numerical masses is justified by the task’s explicit rules. The proof does not impose monotonicity on the utility table. It also does not use the symmetry condition \(U(w)+U(T-w)=0\); this is acceptable because its argument applies to all utility tables satisfying the task’s hypotheses.

The claimed output includes both the exact initial value and the required strategy circuits.

2. Reduction to two matrix games

The finite zero-sum minimax theorem is stated in an applicable form. Both supports are finite and nonempty, so their probability simplices are nonempty, and the matrix payoffs are finite. Optimal maximizing and minimizing distributions therefore exist.

The definitions \(\alpha=v(P)\) and \(\beta=-v(-P)\) are consistent. Since entries of \(P\) lie in \([0,1]\), \(\alpha\) lies in \([0,1]\). Entries of \(-P\) lie in \([-1,0]\), so \(\beta\) also lies in \([0,1]\).

The formula for \(v(cJ+dP)\) is correct in all three cases:

The negative case correctly uses the equilibrium distributions of \(-P\) with the original maximizing and minimizing roles. There is no erroneous reversal of player roles.

Finding: Correct and rigorous.

3. State reduction and backward recursion

The state domain \(0\leq w\leq k\leq T\) is correct. For every nonterminal state, both successor indices appearing in the recurrence belong to the next row of the table.

The transition expression
\(p_{ij}V_{k+1,w+1}+(1-p_{ij})V_{k+1,w}\)
uses exactly the conditional probabilities specified by the task. Its decomposition as \(c_{k,w}+d_{k,w}p_{ij}\) is algebraically correct.

The proof ultimately justifies the reduction to round count and win count through its induction over all histories. It does not merely assume that histories with those counts have equal values.

Minor issue: counting used representatives

Where: Section 2, “Indeed, fewer than \(T\) representatives have been used in total.”

Read as a statement about both teams together, this is false. For example, when \(T=2\), after one round two representatives have been used altogether, which is not fewer than \(T\).

This does not invalidate availability or the recurrence. The relevant count is within each team, and the surrounding assumptions suffice.

Minimum clarification requested: Replace “in total” with an explicitly per-team statement, and specify that the count bounds the representatives used from any one supported type.

Severity: Minor.

4. Subgame perfection

The induction assertion is sufficiently strong: it quantifies over every history in a state and every opposing behavioral strategy, including history-dependent deviations.

The terminal case is correct because the payoff is already fixed by the win count.

For B’s guarantee, the argument correctly:

The argument for A’s guarantee is the corresponding lower-bound argument. Both inequalities have the correct directions.

At a zero continuation difference, the continuation matrix is constant, so the prescribed pure distributions satisfy both guarantees.

The induction applies at off-equilibrium histories as well as histories reached under the prescribed pair. Consequently, it establishes equilibrium in every subgame. When both prescribed strategies are used, the two guarantees identify the expected payoff with \(V_{k,w}\).

Probabilities equal to zero or one cause no problem: impossible outcomes contribute nothing to the expectation, while the prescriptions remain defined at all relevant histories.

Finding: Correct and rigorous.

5. Exact matrix-game computation

The invoked LP theorem is applicable: rational linear programs can be optimized exactly in polynomial time in their binary encoding length, with polynomial-length rational optimal solutions for feasible problems with finite optimum.

The displayed LPs have rational coefficients, nonempty compact feasible regions, and bounded objectives. The witnesses \(z=-1\) and \(z=1\) establish feasibility because matrix entries lie in \([-1,1]\). The imposed bounds on \(z\) do not exclude a game value.

The maximizing constraints account for every pure column, and the minimizing constraints account for every pure row. These are the correct matrix-game optimization programs. Minimax identifies their common optimum.

Their variable and constraint counts are polynomial in the stated support parameters. Computing four player LPs to obtain two equilibrium pairs is consistent with the claim that two matrix games suffice.

The cited [Goemans notes](https://ocw.mit.edu/courses/6-854j-advanced-algorithms-fall-2008/908fe54d659623efadda2d033b895caf_notes_lp.pdf) discuss rational input encoding, determinant bounds for vertex representations, and polynomial-time linear programming. The theorem used here has the required hypotheses.

Finding: Correct; no unverified theorem application remains.

6. Continuation-value bit complexity

The common-denominator argument is valid.

The product \(R\) of utility denominators has logarithmic size bounded by their total encoded length. The chosen common denominator \(Q\) for \(\alpha,\beta\) likewise has polynomial bit length.

At each level, the successor numerators share a denominator. Comparing their difference therefore gives the exact sign of \(d_{k,w}\), without approximation.

The integer recurrence has the correct denominator scaling. Its zero-difference branch is also correct: choosing \(C=0\) multiplies the successor numerator by \(Q\), matching the additional denominator factor.

Because \(0\leq C\leq Q\), every value recurrence is a convex combination. The bounds \(|V_{k,w}|\leq H\) and \(|N_{k,w}|\leq HRQ^{T-k}\) follow as claimed. They yield polynomial bit lengths, including when utilities are negative or all zero.

There are \(O(T^2)\) states. Integer comparisons, additions, and multiplications on the established operand sizes take polynomial bit time.

Finding: Correct and sufficient for exact computation.

7. Strategy circuits and overall complexity

The fixed-length history encoding is a permissible representation of public histories. Counting wins among the first \(k\) records identifies the required state. Previous type choices need not affect the output because the preceding induction established the guarantees at every history with that state.

The stored sign table has polynomial size. Its lookup and selection among fixed rational probability vectors admit polynomial-size Boolean circuits. The probability numerators and denominators have polynomial widths by the LP bound.

Assigning arbitrary outputs to terminal or malformed encodings is acceptable: behavioral distributions are required at valid nonterminal histories.

Finally, the explicit utility table contains \(T+1\) entries, so \(T=O(L)\). The algorithm is therefore polynomial in the full binary input length, as well as in the requested parameters.

Finding: The required circuit output and complexity classification are established.

Overall adjudication

The argument is sound in substance and needs only a local clarification of the representative count. No additional lemma, computational argument, or equilibrium argument is required.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.