← back to the atlas

d4-conf-atal-2020-0232 (d4-conf-atal-2020-0232)

Answer: Yes: a polynomial-time \(\frac12\)-approximation exists, with one rational team template and a binary encoded multiplicity.

The anchor (named result in the paper)

Theorem 3.3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThere exists an efficient algorithm computing a 1 2 optimal coalition structure for any TTG G.

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

The continuous mirror question, as graded

Given capacity types \(r\) with weights \(w_r\), rational proportions \(\mu_r\), population scale \(N\), and repeatable tasks \(j\) with thresholds \(q_j\) and rewards \(v_j\), partition the atomless mass \(N\mu_r\) into disjoint measurable teams, each assigned a task and having total capacity at least its threshold. Can an algorithm return teams with reward at least \(\frac12\mathrm{OPT}_\infty\) in time polynomial in the input bit length?

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

A society is given by its support: \(\tau\ge1\) capacity types with positive binary rational masses \(N\mu_r\), where \(\mu_r>0\), \(\sum_r\mu_r=1\), and \(N\in\mathbb Z_{>0}\) is binary encoded; \(\tau\) is the support size, not the number of possible types.
Type \(r\) has capacity per unit mass \(w_r\in\mathbb Z_{>0}\). Represent its atomless population by a disjoint interval of length \(N\mu_r\) with Lebesgue measure.
There are \(m\ge1\) repeatable task types with binary encoded thresholds and rewards \(q_j,v_j\in\mathbb Z_{>0}\); require \(q_j\le N\sum_r\mu_rw_r\) and \(q_j\le q_k\Rightarrow v_j\le v_k\).
A solution partitions the population into finitely many disjoint measurable teams, each assigned one task, and an optional idle remainder. A team containing type masses \(a_r\) can perform task \(j\) iff \(\sum_rw_ra_r\ge q_j\), earning \(v_j\) once; the remainder earns zero.
Let \(\mathrm{OPT}_\infty\) be the supremum of total reward over such solutions, allowing arbitrary real team masses. Solutions returned by an algorithm use rational masses and may be represented by repeated team templates: a task index, a type-mass vector, and a positive binary integer multiplicity, with total type usage at most \(N\mu_r\).
Can an algorithm return a solution of reward at least \(\frac12\mathrm{OPT}_\infty\) in time polynomial in \(m\), \(\tau\), and the total input bit length \(L\), including the encoding of \(N\)?
For finite indivisible populations, a polynomial-time \(\frac12\)-approximation is known ([Gal, Nguyen, Tran and Zick](https://comsoc-community.org/assets/proceedings/comsoc-2021/GalEtAl.pdf)).
No result settling this precise atomless formulation was located in the literature search.

Modeling choices made when packaging the task

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

Result

Yes. A polynomial-time algorithm achieves a \(\frac12\)-approximation using a single rational team template with a binary encoded multiplicity.

Write \(M_r=N\mu_r\) for the available mass of type \(r\), and let \(C=\sum_{r=1}^{\tau}w_rM_r\) be the total capacity. By the hypotheses, \(C>0\) and every task satisfies \(q_j\le C\).

1. Atomless feasibility reduces to total capacity

We first prove that nonnegative integer task counts \(z_1,\ldots,z_m\) are realizable if and only if \(\sum_{j=1}^{m}z_jq_j\le C\).

Necessity. For any solution, let \(a_{T,r}\) be the mass of type \(r\) in team \(T\), and let \(j(T)\) be its task. Feasibility and disjointness imply
\(\sum_Tq_{j(T)}\le\sum_T\sum_rw_ra_{T,r}\le\sum_rw_rM_r=C\).
Grouping teams by their assigned task proves the required inequality.

Sufficiency. For every task \(j\), define the rational mass vector \(b^{(j)}\) by \(b^{(j)}_r=q_jM_r/C\). Each copy of this vector has capacity
\(\sum_rw_rb^{(j)}_r=(q_j/C)\sum_rw_rM_r=q_j\),
so it performs task \(j\).

Moreover, the prescribed copies use type \(r\) mass
\(\sum_jz_jb^{(j)}_r=(M_r/C)\sum_jz_jq_j\le M_r\).
Within each type interval, place consecutive disjoint subintervals of these prescribed lengths. A team is the union of its corresponding subintervals across types. These teams are measurable and disjoint; the unused portions form the idle remainder.

Consequently, \(\mathrm{OPT}_\infty\) equals the maximum of \(\sum_jz_jv_j\) over integer vectors satisfying \(z_j\ge0\) and \(\sum_jz_jq_j\le C\). This maximum exists: every coordinate satisfies \(z_j\le\lfloor C/q_j\rfloor\), so there are finitely many feasible vectors. In particular, allowing arbitrary real team masses creates no additional reward beyond these integer task counts.

2. Algorithm and feasibility

Choose a task \(j^\star\) maximizing the reward density \(v_j/q_j\), breaking ties arbitrarily. Define \(q^\star=q_{j^\star}\), \(v^\star=v_{j^\star}\), and \(k=\lfloor C/q^\star\rfloor\).

Return the single template consisting of task \(j^\star\), mass vector \(a_r=q^\star M_r/C\), and multiplicity \(k\).

Since \(q^\star\le C\), the multiplicity is positive. Each copy has capacity exactly \(q^\star\), and its total type usage satisfies \(ka_r=(kq^\star/C)M_r\le M_r\). Thus the template represents a feasible measurable partition, by the interval construction above.

3. Approximation guarantee

Let \(d=v^\star/q^\star=\max_jv_j/q_j\).

For every feasible solution, including one with arbitrary real team masses, its reward satisfies
\(\sum_Tv_{j(T)}\le d\sum_Tq_{j(T)}\le dC\).
Taking the supremum gives \(\mathrm{OPT}_\infty\le dC\).

Set \(x=C/q^\star\). Then \(x\ge1\), and \(k=\lfloor x\rfloor\ge1\). Since \(x<k+1\le2k\), we have \(k\ge x/2\). Therefore the returned reward satisfies
\(kv^\star\ge(x/2)v^\star=\frac12Cd\ge\frac12\mathrm{OPT}_\infty\).

This proves the requested guarantee. The reward-monotonicity hypothesis is not needed for this argument.

4. Polynomial time and output length

All calculations use exact integer and rational arithmetic.

The maximum-density task can be found using integer cross-products: \(v_j/q_j\ge v_\ell/q_\ell\) exactly when \(v_jq_\ell\ge v_\ell q_j\).

The rational numbers \(M_r\), \(C\), and \(a_r=q^\star M_r/C\) have bit lengths polynomial in the input length \(L\). Indeed, a common denominator for the sum defining \(C\) can be obtained by multiplying the input denominators; its bit length is at most the sum of their bit lengths. Multiplication, addition, division, and exact comparisons therefore require polynomial time.

Finally, \(\sum_r\mu_r=1\) gives \(C\le N\max_rw_r\). Because \(q^\star\ge1\), we have \(k\le C\le N\max_rw_r\), so the binary encoding of \(k\) also has polynomial length.

The algorithm outputs only one task index, \(\tau\) rational masses, and one binary integer multiplicity. It never enumerates the individual teams. Its running time and output length are polynomial in \(m\), \(\tau\), and \(L\), including the encoding of \(N\).

⟨structured verdict parsed — rendered above⟩

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

Verification report

The prover resolves the requested task. The feasibility reduction, approximation guarantee, and polynomial encoding claims are correct. No major or minor mathematical issues were found.

1. Reduction to integer task counts

The necessity argument is valid. Each team earns a reward once and therefore contributes one integer task count. Summing its capacity requirement over the finitely many disjoint teams gives
\[ \sum_j z_jq_j\le C. \]
Disjointness ensures that the total mass used from type \(r\) is at most \(M_r\).

The sufficiency construction is also valid. Since \(C>0\), the vector
\[ b^{(j)}_r=\frac{q_jM_r}{C} \]
is well-defined, nonnegative, and rational. Its capacity is exactly \(q_j\). For any feasible integer count vector, the aggregate usage of each type is at most its available mass.

There are finitely many prescribed teams, so the interval construction realizes these masses by disjoint measurable subsets. Endpoints can be assigned using half-open subintervals, with any remaining endpoints included in the idle remainder; this is a routine interpretation of the stated construction.

Thus both directions of the claimed equivalence hold. The feasible integer count vectors form a finite, nonempty set, because each coordinate is bounded and the zero vector is feasible. Consequently, the maximum exists and equals the original supremum.

2. Algorithm and output feasibility

A maximum-density task exists because there are finitely many tasks and all thresholds are positive.

The hypothesis \(q^\star\le C\) gives \(k=\lfloor C/q^\star\rfloor\ge1\), satisfying the requirement that the multiplicity be positive.

Each template copy has capacity exactly \(q^\star\), and
\[ ka_r=\frac{kq^\star}{C}M_r\le M_r. \]
The returned template therefore satisfies every type-usage constraint and represents a feasible measurable solution. The permitted representation does not require enumerating its copies.

3. Approximation bound

For every task, maximum density gives \(v_j\le dq_j\). Combining this with the capacity bound yields
\[ \mathrm{OPT}_\infty\le dC. \]
This applies to all allowed solutions, including those using irrational team masses.

For \(x=C/q^\star\ge1\) and \(k=\lfloor x\rfloor\), the inequalities
\[ x<k+1\le2k \]
are correct, including the boundary case \(k=1\). Hence \(k\ge x/2\), and the displayed reward bound follows:
\[ kv^\star\ge\frac12Cd\ge\frac12\mathrm{OPT}_\infty. \]

There is no reversed inequality or unsupported rounding step. The reward-monotonicity hypothesis is indeed unnecessary for this argument.

4. Polynomial time and encoding length

The density comparisons use integer cross-products of polynomial bit length.

The common-denominator argument correctly bounds the bit length of \(C\): multiplying the input denominators adds their bit lengths. Numerator multiplication and summation introduce only polynomially many additional bits. The same reasoning applies to \(M_r\) and \(a_r=q^\star M_r/C\). Exact floor division computes \(k\) in polynomial time.

The bound
\[ k\le C\le N\max_r w_r \]
is valid because \(q^\star\ge1\) and the positive \(\mu_r\) sum to one. Thus the multiplicity has polynomial binary length even when its numerical value is large.

The output contains one task index, \(\tau\) rational coordinates, and one binary multiplicity. Both its length and the computation time meet the requested bounds.

5. Adjudication and feedback

No additional clarification or mathematical repair is needed. The proof establishes the requested polynomial-time approximation algorithm. It does not claim or establish polynomial-time exact optimization; under the supplied classification, its approximation guarantee is recorded as "other".

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