← back to the atlas

d4-conf-ijcai-2020-0047 (d4-conf-ijcai-2020-0047)

Answer: Polynomial-time solvable in the binary input length.

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe CSG-UCT algorithm is complete given a sufficient amount of time.

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

The continuous mirror question, as graded

Given a finite type set \(T\), rational type masses \(N\mu_t\), and an explicit value \(w(q)\) for each feasible integral team composition \(q\in\mathbb{Z}_{\ge 0}^{T}\setminus\{0\}\), find a maximum-welfare allocation \(x_q\ge 0\) satisfying \(\sum_q q_t x_q=N\mu_t\) for every \(t\in T\).

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive masses \(b_t\), each encoded as a binary rational. Here \(\tau=|T|\) is the support size, not the number of possible types. Require \(N=\sum_{t\in T}b_t\) to be a positive integer, and write \(\mu_t=b_t/N\), so \(\sum_t\mu_t=1\).
The feasible integral team compositions are \(Q=\{q\in\mathbb Z_{\ge0}^{T}\setminus\{0\}:q_t\le b_t\text{ for every }t\in T\}\). The input explicitly lists every \(q\in Q\) and its nonnegative binary-rational value \(w(q)\); values depend only on composition.
An allocation assigns a real mass \(x_q\ge0\) to each composition and exhausts the society: \(\sum_{q\in Q}q_t x_q=b_t\) for every \(t\in T\). Its welfare is \(\sum_{q\in Q}w(q)x_q\). Find an allocation of maximum welfare, or report infeasibility; any maximizing allocation is acceptable.
Let \(m=N\) be the maximum permitted team size, \(K=|Q|\), and \(L\) the total binary input length, including the explicit value table. State running times in \(m,\tau,K,L\), with polynomial time measured in the encoded input length.

Is this exact rational-mass welfare-maximization problem solvable in polynomial time, or is it \(\mathrm{NP}\)-hard?

For finite agents, CSG-UCT eventually finds an optimal exhaustive, disjoint coalition partition given sufficient time; this guarantee supplies no polynomial running-time bound ([Wu and Ramchurn](https://www.ijcai.org/proceedings/2020/0057.pdf)). Discrete coalition structure generation also has a polynomial-time algorithm when known player types are bounded in number by a constant ([Aziz and de Keijzer](https://arxiv.org/abs/1101.1007)).
No result settling precisely the rational-mass problem with this explicit composition table was identified in the literature search.

Modeling choices made when packaging the task

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

Exact welfare maximization is polynomial-time solvable

1. Statement and interpretation

Theorem. Under the stated explicit-table encoding, the problem is solvable exactly in time polynomial in \(L\), for arbitrary support size \(\tau\). An algorithm can report infeasibility or return an optimal allocation with rational coordinates.

We use the allocation definition in the question: the composition vectors \(q\) are integral, while their allocation masses \(x_q\) may be real. No integrality condition is imposed on \(x_q\).

2. Feasibility and existence of an optimum

First, feasibility has a direct characterization:

\(\displaystyle \text{An allocation exists}\quad\Longleftrightarrow\quad b_t\geq 1\text{ for every }t\in T.\)

To prove necessity, suppose \(0<b_t<1\) for some type \(t\). Every feasible composition has an integer coordinate satisfying \(0\leq q_t\leq b_t<1\), so \(q_t=0\). Consequently, every allocation satisfies \(\sum_{q\in Q}q_tx_q=0\), contradicting exhaustion of the positive mass \(b_t\).

For sufficiency, suppose every \(b_t\geq1\). Let \(e_t\) denote the unit composition containing one member of type \(t\). Then \(e_t\in Q\). Setting \(x_{e_t}=b_t\) and all other allocation masses to zero exhausts the society.

Now assume feasibility. Write \(|q|=\sum_{t\in T}q_t\). Every listed composition satisfies \(1\leq |q|\leq m\): the lower bound follows from \(q\neq0\), and the upper bound follows from \(q_t\leq b_t\) and \(\sum_tb_t=m\). Summing the exhaustion equations gives

\(\displaystyle \sum_{q\in Q}|q|x_q=m.\)

Because all allocation masses are nonnegative, this implies \(\sum_qx_q\leq m\), and hence \(0\leq x_q\leq m\) for every \(q\).

The feasible region is therefore nonempty, closed, and bounded in the finite-dimensional space \(\mathbb R^K\). It is compact. Welfare is a continuous linear function, so a maximum is attained.

3. An exact linear-programming formulation

Index the listed compositions as \(q^{(1)},\ldots,q^{(K)}\). Define the matrix \(A\in\mathbb Z^{\tau\times K}\) and objective vector \(c\in\mathbb Q^K\) by

\(\displaystyle A_{t,j}=q_t^{(j)},\qquad c_j=w(q^{(j)}).\)

The optimization problem is exactly

\(\displaystyle \max\{c^\mathsf T x:Ax=b,\ x\in\mathbb R_{\geq0}^K\}.\)

Indeed, each equation of \(Ax=b\) is precisely one exhaustion equation, and the objective is precisely the specified welfare. Thus every feasible allocation yields a feasible LP solution of the same welfare, and conversely.

We apply the standard polynomial-time theorem for rational linear programming: given an explicitly encoded rational constraint matrix, right-hand side, and objective, one can detect infeasibility or unboundedness and, when a finite optimum exists, compute an exact rational optimizer in time polynomial in their total binary encoding length. This theorem permits equality constraints and lower-dimensional feasible regions; equalities may also be represented by pairs of inequalities. See [University of Washington’s linear-programming notes, Theorem 17.1 and Section 17.4](https://courses.cs.washington.edu/courses/cse521/22au/521-lecture-16.pdf).

All hypotheses hold here: the matrix is explicitly available and integral, the remaining data are explicitly encoded rationals, and Section 2 proves attainment and boundedness whenever feasible.

4. Encoding size and running time

Let \(S\) be the binary encoding length of the constructed LP. Since \(0\leq A_{t,j}\leq m\), every matrix entry requires \(O(\log(m+1))\) bits. The masses and values already belong to the input. Therefore

\(\displaystyle S=O\!\left(L+\tau K\log(m+1)\right).\)

Replacing equalities by pairs of inequalities and adding nonnegativity inequalities changes this bound only by a constant factor and an additional \(O(K)\) term, which is absorbed because \(K=O(L)\).

Consequently, for some fixed polynomial \(p\), the complete algorithm has a bit-operation running time bounded by

\(\displaystyle p\!\left(K+\tau+L+\tau K\log(m+1)\right).\)

This is polynomial in \(L\). To check that conclusion explicitly:

Thus \(S=O(L^3)\) is a sufficient, conservative bound, and the running time is \(L^{O(1)}\).

The composition count also has the exact expression

\(\displaystyle K=\prod_{t\in T}\left(\lfloor b_t\rfloor+1\right)-1\leq(m+1)^\tau-1.\)

The equality follows because each coordinate independently ranges from zero through \(\lfloor b_t\rfloor\), with only the all-zero vector excluded. The table can therefore be large as a function of \(m\) and \(\tau\), but its length is already counted in \(L\). The algorithm does not enumerate an unlisted family of compositions.

5. Exact optimizers have polynomial-size rational representations

Here is an explicit verification that exact output does not require irrational coordinates or exponentially many output bits.

Among all optimal allocations, choose \(x^*\) with the smallest number of positive coordinates, and let \(J\) be its support. The columns \(A_{\cdot,j}\), for \(j\in J\), are linearly independent.

Otherwise, there would exist a nonzero vector \(d\), supported on \(J\), with \(Ad=0\). For sufficiently small \(\varepsilon>0\), both \(x^*+\varepsilon d\) and \(x^*-\varepsilon d\) remain nonnegative and satisfy the exhaustion equations. Optimality in both directions implies \(c^\mathsf Td=0\).

Moreover, \(d\) has both positive and negative entries. Indeed,

\(\displaystyle 0=\sum_t(Ad)_t=\sum_{j\in J}|q^{(j)}|d_j,\)

where every coefficient \(|q^{(j)}|\) is positive. Set

\(\displaystyle \alpha=\min_{j\in J:\,d_j<0}\frac{x_j^*}{-d_j}>0.\)

Then \(x^*+\alpha d\) is feasible, has the same welfare, and has strictly smaller support—a contradiction.

Write \(s=|J|\). Independence gives \(s\leq\tau\). Select \(s\) rows for which the corresponding square matrix \(B\) is nonsingular. The positive allocation coordinates are the unique solution of

\(\displaystyle Bx_J^*=b_I.\)

Write each mass as \(b_t=p_t/r_t\), with positive integer denominator, and set \(D=\prod_tr_t\). The bit length of \(D\) is \(O(L)\). Cramer’s rule gives

\(\displaystyle x_j^*=\frac{\det B_j(Db_I)}{D\det B},\)

where \(B_j(Db_I)\) replaces column \(j\) of \(B\) by \(Db_I\).

Every entry of \(B\) is at most \(m\), and every entry of \(Db_I\) is at most \(Dm\). Expanding the determinants over permutations therefore yields

\(\displaystyle |\det B|\leq s!m^s,\qquad |\det B_j(Db_I)|\leq s!Dm^s.\)

Thus each positive coordinate has numerator and denominator bit lengths

\(\displaystyle O\!\left(L+s\log(m+1)+s\log(s+1)\right),\)

which are polynomial in \(L\). There exists an exact rational optimum using at most \(\tau\) compositions.

6. Relation to discrete coalition partitions

Fractional allocation masses can change the optimum even when all type masses are integers. For example, take one type with \(b=3\), so the explicitly listed compositions are \(1,2,3\). Set \(w(2)=1\) and \(w(1)=w(3)=0\).

The allocation \(x_2=3/2\) has welfare \(3/2\), which is optimal because exhaustion implies \(2x_2\leq3\). An integral coalition partition can contain at most one team of size two, giving maximum welfare \(1\).

Accordingly, the discrete results supplied in the question concern a different feasible set. [Wu and Ramchurn](https://www.ijcai.org/proceedings/2020/0057.pdf) study exhaustive, disjoint partitions of finite agents; [Aziz and de Keijzer](https://arxiv.org/abs/1101.1007) give a discrete polynomial-time result under a constant bound on known player types. The present result needs no constant bound on \(\tau\): rational allocation masses and the explicit composition table give an exact rational LP.

Conclusion: the stated problem is polynomial-time solvable in its binary input length. NP-hardness under standard polynomial-time reductions would therefore imply \(\mathrm P=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

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

The output settles the intended problem in substance: exact welfare maximization is polynomial-time solvable under the explicit composition-table encoding. I found no major mathematical gap. There is one minor encoding issue in the optional conversion to inequality form.

The prover correctly distinguishes integral composition coordinates from real allocation masses. The task imposes no integrality restriction on \(x_q\), so the linear-programming formulation addresses exactly the requested feasible set. No restriction to constant support size is introduced.

If \(0<b_t<1\), every permitted integral composition has \(q_t=0\). Thus the exhaustion equation for that type cannot hold. This argument applies regardless of whether other types have permitted compositions.

Conversely, if every \(b_t\geq1\), every unit composition \(e_t\) belongs to the explicitly listed set \(Q\). The assignment \(x_{e_t}=b_t\), with other coordinates zero, satisfies every exhaustion equation.

The potentially empty composition table is covered: if \(Q\) is empty, the positive, nonempty society cannot be exhausted. The necessity argument detects this situation.

Each composition satisfies \(1\leq |q|\leq m\). Summing the exhaustion equations gives
\[ \sum_{q\in Q}|q|x_q=m. \]
Nonnegativity then implies \(\sum_qx_q\leq m\), and consequently \(x_q\leq m\) for every coordinate.

The feasible region is defined by finitely many linear equalities and closed nonnegativity constraints. Whenever feasible, it is nonempty and bounded. Compactness and continuity therefore establish attainment of a finite maximum. This argument also covers zero welfare values.

The matrix equation \(Ax=b\), nonnegativity constraints, and objective \(c^\mathsf{T}x\) reproduce the allocation definition exactly, in both directions.

The prover states the required rational-LP theorem sufficiently precisely: polynomial time in binary encoding length, exact rational output, and allowance for equality constraints and lower-dimensional feasible regions. Its hypotheses are satisfied here because all coefficients are explicitly available rationals, the dimensions are finite, and the preceding argument establishes boundedness whenever feasible.

The cited notes state the polynomial-time LP theorem and discuss removal of the full-dimensionality assumption. Their exposition omits technical details, but the prover invokes the general rational-LP theorem, rather than applying only the full-dimensional geometric subroutine. This is a legitimate use of a standard theorem. [University of Washington notes, Theorem 17.1 and Section 17.4](https://courses.cs.washington.edu/courses/cse521/22au/521-lecture-16.pdf).

For the displayed standard-form LP, the bound
\[ S=O\!\left(L+\tau K\log(m+1)\right) \]
is valid. All matrix entries are integers between zero and \(m\), while the masses and objective coefficients are already included in the input.

The bounds \(\tau=O(L)\), \(K=O(L)\), and \(\log(m+1)=O(L)\) follow from the explicit support and table and the binary-rational encoding. Hence the conservative \(O(L^3)\) size bound and polynomial-time conclusion are valid.

Minor issue: the claim that adding explicit nonnegativity inequalities incurs only an additional \(O(K)\) encoding term needs a representation convention. In a dense inequality matrix, these inequalities contribute a \(K\)-by-\(K\) coefficient block, including its zero entries. Counting inequalities is not the same as counting encoded coefficients.

Minimum clarification: specify the representation used for those bounds, or correct the encoding bookkeeping for the optional conversion. This does not undermine the standard-form formulation or the polynomial-time conclusion.

The composition-count identity
\[ K=\prod_{t\in T}\left(\lfloor b_t\rfloor+1\right)-1 \]
is correct, including when \(K=0\). Its upper bound is also valid. The prover correctly measures complexity against the supplied table rather than an implicitly represented family.

Choosing an optimal allocation of minimum support is legitimate because an optimum exists and support cardinalities range over a finite set.

If its supported columns were dependent, the stated kernel direction allows sufficiently small perturbations in both signs while retaining feasibility. Optimality forces \(c^\mathsf{T}d=0\). The positive column sums force that nonzero direction to have both positive and negative coordinates. The specified \(\alpha\) then removes at least one positive coordinate without introducing coordinates outside the support or changing welfare. This contradicts minimal support.

Thus \(s\leq\tau\), and selecting a nonsingular square row submatrix is justified. Clearing denominators with \(D\) and applying Cramer’s rule gives the displayed formula correctly.

Both determinant bounds are correct: a numerator determinant contains exactly one replaced column. The resulting numerator and denominator bit-length bounds are polynomial in \(L\). This establishes existence of a polynomial-size rational optimum; the cited exact LP theorem supplies its algorithmic computation.

In the one-type example, welfare equals \(x_2\), exhaustion bounds it by \(3/2\), and the stated fractional allocation attains that bound. An integral partition can contain at most one size-two coalition and achieves welfare \(1\).

The cited discrete results concern exhaustive, disjoint partitions of finite players; the constant-type statement is supported by the cited paper. They do not impose a constant-type hypothesis on this LP argument. [Wu and Ramchurn](https://www.ijcai.org/proceedings/2020/0057.pdf), [Aziz and de Keijzer](https://arxiv.org/abs/1101.1007).

The polynomial-time classification follows. The conditional statement concerning NP-hardness and \(\mathrm P=\mathrm{NP}\) is appropriately qualified.

⟨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.