← back to the atlas

d4-conf-atal-2015-0267 (d4-conf-atal-2015-0267)

Answer: Polynomial-time solvable: the decision problem is in \(\mathrm{P}\).

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet D ∈D be a set containing one factor from each Goodω. For arbitrary n, the probability that we generate (by drawing from a distribution F) an optimal team of size n converges to 0 as |Ω| →∞. However, if n = c Q d∈D d, then the probability that the team is optimal tends to 1 as c →∞.

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

The continuous mirror question, as graded

Given finite contexts \(\Omega\), action sets \(A_\omega\), optimal subsets \(Good_\omega\), and agent types \(t\) with rational vote probabilities \(q_{t,\omega}(a)\), decide whether a rational mass distribution \(\mu\) over types exists such that, at every context, all actions in \(Good_\omega\) have equal vote mass and strictly exceed every action outside \(Good_\omega\), where \(v_{\mu,\omega}(a)=\sum_t\mu_tq_{t,\omega}(a)\). With uniform tie-breaking, this makes each optimal action equally likely at each context and each combination of optimal actions equally likely across independent contexts.

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

Input consists of a nonempty finite context set \(\Omega\), explicitly listed finite action sets \(A_\omega\), nonempty subsets \(Good_\omega\subseteq A_\omega\), and a nonempty explicit catalogue \(T\) of \(k\) available agent types. Each type supplies binary rational probabilities \(q_{t,\omega}(a)\geq0\) satisfying \(\sum_{a\in A_\omega}q_{t,\omega}(a)=1\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types. The sought society may use any subset of \(T\), with \(\mu_t\geq0\) and \(\sum_{t\in T}\mu_t=1\); there is no prescribed support bound.
Define \(v_{\mu,\omega}(a)=\sum_{t\in T}\mu_tq_{t,\omega}(a)\). Feasibility requires \(v_{\mu,\omega}(a)=v_{\mu,\omega}(a')\) for all \(a,a'\in Good_\omega\), and \(v_{\mu,\omega}(a)>v_{\mu,\omega}(b)\) for all \(a\in Good_\omega\), \(b\in A_\omega\setminus Good_\omega\), at every context.
Plurality uses these vote masses directly, with uniform tie-breaking independently across contexts; optimal solutions are exactly \(\prod_{\omega\in\Omega}Good_\omega\). Thus a feasible society selects each optimal solution with probability \(1/\prod_{\omega\in\Omega}|Good_\omega|\).
Write running times in \(m=\sum_{\omega\in\Omega}|A_\omega|\), \(k\), \(\tau\), \(|\Omega|\), and the total input bit length \(L\).

Is deciding whether such a rational society exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

The [discrete asymptotic result](https://eprints.lancs.ac.uk/id/eprint/81442/1/COIN2015Book.pdf) claims that, under symmetric diverse-agent assumptions, sampled teams become optimal with probability tending to one along sizes \(n=c\prod_{d\in D}d\), where \(D\) contains a divisor greater than one of each \(|Good_\omega|\), as \(c\to\infty\); it supplies no polynomial-time decision algorithm.
No result settling this exact continuous feasibility problem was located in the literature search.

Modeling choices made when packaging the task

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

Result

The decision problem is in \(\mathrm{P}\). A feasible rational society, when one exists, can also be constructed in polynomial time.

Here “binary rational” means a rational number whose numerator and denominator are encoded in binary. The proof uses the explicit catalogue of all \(k\) types and imposes no support bound.

1. Reduce the number of comparisons

For each context \(\omega\), choose a reference action \(g_\omega\in Good_\omega\). Define the rational coefficients

\(e_{\omega,a,t}=q_{t,\omega}(a)-q_{t,\omega}(g_\omega)\), for \(a\in Good_\omega\setminus\{g_\omega\}\),

and

\(d_{\omega,b,t}=q_{t,\omega}(g_\omega)-q_{t,\omega}(b)\), for \(b\in A_\omega\setminus Good_\omega\).

The original requirements are equivalent to

\(\sum_{t\in T}e_{\omega,a,t}\mu_t=0\) for every indicated good action, and

\(\sum_{t\in T}d_{\omega,b,t}\mu_t>0\) for every indicated bad action.

Indeed, the equalities make every good action’s vote mass equal to that of \(g_\omega\). Consequently, comparing \(g_\omega\) with every bad action suffices.

There are

\(\sum_{\omega\in\Omega}(|Good_\omega|-1)\)

equality rows and

\(\sum_{\omega\in\Omega}(|A_\omega|-|Good_\omega|)\)

strict inequality rows. Their total is \(m-|\Omega|\).

2. Remove strict inequalities by scaling

Consider the following ordinary rational linear feasibility problem, with variables \(x_t\), one for each type:

Call its feasible polyhedron \(Q\).

Claim. A feasible rational society exists if and only if \(Q\) contains a rational point.

Forward direction. Suppose \(\mu\) is a feasible rational society. If there are good–bad comparison rows, define

\(\delta=\min_{\omega,\;b\in A_\omega\setminus Good_\omega}\sum_{t\in T}d_{\omega,b,t}\mu_t\).

This is the minimum of a nonempty finite collection of positive rational numbers, so \(\delta>0\) and \(\delta\) is rational. Set

\(\alpha=\max\{1,\delta^{-1}\}\), and \(x_t=\alpha\mu_t\).

Nonnegativity and all homogeneous equalities are preserved. Moreover,

\(\sum_t x_t=\alpha\geq 1\)

and every comparison satisfies

\(\sum_t d_{\omega,b,t}x_t\geq\alpha\delta\geq 1\).

Thus \(x\in Q\).

If there are no comparison rows, take \(x=\mu\). The equalities still have to hold; they are retained in \(Q\).

Reverse direction. Suppose \(x\in Q\) is rational. Let

\(S=\sum_{t\in T}x_t\geq 1\), and \(\mu_t=x_t/S\).

These are nonnegative rational masses summing to one. Every equality is preserved, and every good–bad comparison satisfies

\(\sum_t d_{\omega,b,t}\mu_t=\frac{\sum_t d_{\omega,b,t}x_t}{S}\geq\frac1S>0\).

Therefore \(\mu\) is a feasible society. This proves the claim.

3. Rational witnesses have polynomial bit length

We verify that real feasibility of \(Q\) also supplies a rational witness of manageable size.

Suppose \(Q\neq\varnothing\), and choose \(x^0\in Q\). The set

\(Q\cap\{x:\sum_t x_t\leq\sum_t x_t^0\}\)

is nonempty, closed, and bounded: every coordinate lies between zero and \(\sum_t x_t^0\). Consequently, minimizing \(\sum_t x_t\) over \(Q\) attains a minimum \(S_*\).

The minimizing set

\(F=\{x\in Q:\sum_t x_t=S_*\}\)

is a nonempty bounded polytope and hence has a vertex \(x^*\). This is also a vertex of \(Q\): if \(x^*\) were a nontrivial convex combination of two points of \(Q\), minimality would force both points to have coordinate sum \(S_*\), contradicting extremality in \(F\).

At a vertex, the equality rows and active inequality rows span the full \(k\)-dimensional space. Otherwise, a nonzero direction orthogonal to all these rows would permit sufficiently small perturbations in both directions. All inactive inequalities have positive slack, so both perturbations would remain feasible, contradicting extremality.

Thus \(x^*\) is uniquely determined by \(k\) independent tight rows. Clear denominators in these rows to obtain an integer system

\(Mx^*=h\), with \(\det M\neq 0\).

Each original coefficient is a difference of probabilities and has absolute value at most one. In any row, multiplying by the product of the denominators of the probabilities appearing in that row clears denominators. Those probabilities are entries of the original input, so this product is at most \(2^L\). Therefore every entry of \(M\) and \(h\) has absolute value at most \(2^L\).

By Cramer’s rule and the determinant expansion,

\(|\det M|\leq k!\,2^{kL}\),

and the same bound holds for each determinant obtained by replacing a column of \(M\) with \(h\). Hence we can write

\(x_t^*=p_t/D\),

where \(D\) is a positive integer and each \(p_t\) is a nonnegative integer, all with \(O(k(L+\log(k+1)))\) bits.

Normalizing cancels the common denominator:

\(\mu_t=\frac{p_t}{\sum_{s\in T}p_s}\).

The denominator is positive because \(\sum_t x_t^*\geq 1\), and it has the same polynomial bit bound. Thus a feasible real instance always has a feasible rational society of polynomial encoding length.

4. Polynomial-time algorithm and running times

Use the standard rational linear-programming theorem: feasibility of an explicitly given system of rational linear equalities and non-strict inequalities can be decided in polynomial time in its encoding length, and a rational feasible point can be constructed when one exists. This is polynomial time in the binary encoding model; see the [MIT notes on linear programming, Sections 11–13](https://ocw.mit.edu/courses/6-854j-advanced-algorithms-fall-2008/908fe54d659623efadda2d033b895caf_notes_lp.pdf).

The algorithm is:

The system has \(k\) variables and

\(k+1+m-|\Omega|\)

rows when an equality counts as one row. Replacing each equality by two inequalities still gives \(O(k+m)\) rows. Its construction uses \(O(km)\) rational subtractions, and its encoding length is polynomial in \(m,k,|\Omega|,L\).

The decision and construction running times are therefore

\(\operatorname{poly}(m,k,|\Omega|,L)\).

Because the catalogue and action sets are explicit, these parameters are bounded by the input length, so the running time is also \(\operatorname{poly}(L)\).

For a supplied society of support size \(\tau\), all vote masses can be computed and checked using \(O(\tau m)\) rational arithmetic operations. The bit running time is polynomial in the combined encoding length of the instance and society. For a polynomial-length society constructed above, this is \(O(\tau m\,\operatorname{poly}(L))\).

5. A support bound follows without imposing one

The vertex witness above additionally satisfies

\(\tau\leq\min\{k,\;m-|\Omega|+1\}\).

To prove this, let \(\tau\) be the number of positive coordinates of \(x^*\). Exactly \(k-\tau\) nonnegativity constraints are active. Besides these, \(Q\) has only \(m-|\Omega|+1\) rows: the action-comparison rows and the row \(\sum_t x_t\geq 1\).

Since the active rows must have rank \(k\),

\(k\leq(k-\tau)+(m-|\Omega|+1)\),

which gives the bound. Normalization preserves the support.

This is an existence bound on a witness; the algorithm does not enumerate supports.

6. Relation to the asymptotic result

The [cited discrete result](https://eprints.lancs.ac.uk/id/eprint/81442/1/COIN2015Book.pdf), Theorem 1, concerns asymptotic sampling under additional assumptions. The decision algorithm proved here follows directly from the finite explicit rational input and does not require that theorem.

Under the stipulated independent uniform tie-breaking, a feasible society makes the maximizing actions exactly \(Good_\omega\) at each context. Hence each solution in \(\prod_{\omega\in\Omega}Good_\omega\) receives probability \(1/\prod_{\omega\in\Omega}|Good_\omega|\), as required.

The exact continuous feasibility problem is therefore polynomial-time solvable. NP-hardness under polynomial-time many-one reductions would imply \(\mathrm{P}=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

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

The output proves the claimed polynomial-time result for the exact input model in USER_TASK. The reduction preserves strict feasibility, handles the absence of bad actions, and produces a rational linear program of polynomial encoding length. No major or minor mathematical issues were found.

The proof uses all \(k\) explicitly available types as variables and permits zero masses. This matches the unrestricted choice of support in the task. It correctly distinguishes the catalogue size \(k\) from the support size \(\tau\).

Its explicit interpretation of “binary rational” as a rational with binary-encoded numerator and denominator matches the intended rational input model.

A reference action \(g_\omega\) exists because every \(Good_\omega\) is nonempty. The coefficients \(e_{\omega,a,t}\) and \(d_{\omega,b,t}\) have the correct signs.

The equality rows impose precisely that all good actions have the same vote mass as \(g_\omega\). Subject to those equalities, the strict comparison of \(g_\omega\) with each bad action implies every required good–bad comparison. Conversely, the original constraints imply all the displayed rows.

The row count is correct: each context contributes \(|Good_\omega|-1\) equalities and \(|A_\omega|-|Good_\omega|\) strict inequalities, totaling \(m-|\Omega|\).

The forward direction is valid. When comparison rows exist, their number is finite and each margin is a positive rational. Their minimum \(\delta\) is therefore a positive rational. The specified rational scaling factor \(\alpha\) preserves nonnegativity and homogeneous equalities, makes the coordinate sum at least one, and makes every comparison margin at least one.

When no comparison rows exist, the separate choice \(x=\mu\) is valid. The proof correctly retains the good-action equality constraints in this case.

The reverse direction is also valid. The constraint \(S=\sum_t x_t\geq1\) ensures normalization is defined. Every comparison becomes at least \(1/S>0\), and normalization preserves all homogeneous equalities. Thus the equivalence holds for rational witnesses in both directions.

The compactness argument is sound. Nonnegativity and the upper bound on the coordinate sum bound every coordinate in the displayed sublevel set. This nonempty closed bounded set is compact, so the continuous coordinate-sum objective attains its minimum there. Points outside it have a larger objective than \(x^0\), so this also establishes a global minimum over \(Q\).

The minimizing set \(F\) is a nonempty bounded polyhedron, hence a polytope with a vertex. No rationality assumption on \(S_*\) is needed here.

The argument that a vertex of \(F\) is a vertex of \(Q\) is correct: any nontrivial convex decomposition in \(Q\) must have both constituent objective values equal to the minimum.

The active-row rank argument is valid even when \(Q\) has lower dimension. If the equality and active inequality normals fail to span the ambient space, the specified nonzero orthogonal direction preserves all tight rows. Finitely many inactive inequalities have positive slack, allowing sufficiently small perturbations in both directions.

Selecting \(k\) independent tight rows therefore gives a nonsingular square rational system determining \(x^*\).

The denominator-clearing estimate is valid. In each comparison row, the relevant probability entries are entries of the original input. The product of their denominators has binary logarithm at most \(L\). Multiplying by that product clears each difference coefficient. Nonnegativity and coordinate-sum rows already have integer coefficients. Since original row coefficients and right-hand sides have absolute value at most one, the resulting integer entries have absolute value at most \(2^L\).

The determinant-expansion bounds \(k!2^{kL}\) apply both to \(M\) and to its column-replacement matrices. Cramer’s rule consequently supplies the asserted common-denominator representation with polynomial bit length. Nonnegativity of \(x^*\) permits nonnegative numerators after choosing a positive denominator.

Normalization cancels that common denominator. The sum of the numerators is positive, and summing \(k\) bounded integers adds at most \(O(\log(k+1))\) bits. The claimed normalized witness bound follows.

The invoked theorem is stated sufficiently precisely: explicit rational linear feasibility can be decided, and a rational feasible point constructed, in polynomial binary running time. The cited [MIT linear-programming notes](https://ocw.mit.edu/courses/6-854j-advanced-algorithms-fall-2008/908fe54d659623efadda2d033b895caf_notes_lp.pdf) discuss encoding size, rational output bounds, and polynomial-time LP algorithms in Sections 11–13.

Its hypotheses are satisfied: \(Q\) is an explicit finite rational system using only equalities and non-strict inequalities. Neither boundedness nor an interior point is required by the stated theorem.

The variable and row counts are correct. Constructing the differences requires \(O(km)\) rational subtractions, each with polynomial bit cost. Duplicating equality rows preserves polynomial encoding size. Obtaining and normalizing the LP output also takes polynomial time.

Thus \(\operatorname{poly}(m,k,|\Omega|,L)\), and consequently \(\operatorname{poly}(L)\), is justified. The supplied-society verification bounds correctly account for \(\tau\) and for the society’s encoding length.

Exactly \(k-\tau\) nonnegativity rows are active at the chosen vertex. There are only \(m-|\Omega|+1\) other rows available. Full active-row rank therefore implies the displayed support bound.

This proves existence of a suitably sparse witness. The output does not incorrectly assert that an arbitrary feasible point returned by the stated algorithm must satisfy that bound.

The constraints make the maximizing actions exactly \(Good_\omega\). Independent uniform tie-breaking therefore gives the stated product probability.

The discrete asymptotic theorem is identified only as background and is not used as a premise; its additional hypotheses need not hold for this argument. The polynomial-time conclusion and the conditional statement about NP-hardness are correct.

No repair or additional clarification 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.