← back to the atlas

d4-conf-aaai-2017-0902 (d4-conf-aaai-2017-0902)

Answer: Polynomial-time solvable; the maximum is \(\epsilon^*=0\), and the weak least-core value is \(0\).

The anchor (named result in the paper)

Theorem 7 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWe can compute a value division in the strong and weak least cores of a hypergraph G = (V, E, w) in O(|V |2f(|V |, O( e∈E |e|))L) time, where f(n, m) is the time complexity of solving the max flow problem on a graph consisting of n vertices and m edges, and L is the number of times that the separation oracle is called by the ellipsoid method, which is polynomial in |V | and |E|.

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

The continuous mirror question, as graded

Given an atomless population of mass \(1\), divided into \(\tau\) types with rational masses \(\mu_t>0\), and a finite list of interaction schemas \(h=(t_1,\ldots,t_{r(h)})\) with nonnegative rational weights \(w_h\), let a coalition be represented by type masses \(z_t\in[0,\mu_t]\) and have value \(\nu(z)=\sum_h w_h\prod_{j=1}^{r(h)}z_{t_j}\). Find the largest \(\epsilon\) and nonnegative type payment rates \(p_t\) such that \(\sum_t\mu_t p_t=\nu(\mu)\) and \(\sum_t p_tz_t\ge\nu(z)+\epsilon\sum_tz_t\) for every \(z\) with \(0<\sum_tz_t<1\); the weak least-core value is \(-\epsilon\).

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

A society is given by its support: a list of \(\tau\ge 1\) types with positive binary rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). The population is atomless; \(\tau\) is the support size, not the number of possible types.
The input also lists \(m\) interaction schemas \(h=(t_1,\ldots,t_{r(h)})\), with \(r(h)\ge 1\), type indices in \(\{1,\ldots,\tau\}\), and nonnegative binary rational weights \(w_h\). Repeated type indices are allowed. Put \(R=\sum_h r(h)\), and let \(L\) be the total input bit length.
A coalition is any real vector \(z\) with \(0\le z_t\le\mu_t\); its value is \(\nu(z)=\sum_h w_h\prod_{j=1}^{r(h)}z_{t_j}\).
Find the largest real \(\epsilon\) and real payment rates \(p_t\ge 0\) satisfying \(\sum_t\mu_t p_t=\nu(\mu)\) and \(\sum_t p_tz_t\ge\nu(z)+\epsilon\sum_tz_t\) for every coalition with \(0<\sum_tz_t<1\). The weak least-core value is \(-\epsilon\).

Is exact computation of this optimum and an attaining payment vector solvable in time polynomial in \(m,\tau,R,L\), or is it NP-hard?

For finite populations with at least two players, nonnegative weighted nonempty hyperedges, and coalition value equal to the total weight of contained hyperedges, strong and weak least-core values and attaining allocations are computable in polynomial time ([Hatano–Yoshida](https://ojs.aaai.org/index.php/AAAI/article/view/10583)).
No result settling the complexity of the exact atomless schema model above was found in the literature search.

Modeling choices made when packaging the task

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

Result

Exact computation is polynomial-time solvable. For every input in the stated model, the maximum is \(\epsilon^*=0\), and hence the weak least-core value is \(0\).

The availability of proper coalitions arbitrarily close to the whole population forces this upper bound. The proof below establishes attainability for arbitrary support size, schema arities, and repeated type indices.

1. Every feasible solution has \(\epsilon\le 0\)

Write \(V=\nu(\mu)\). Suppose \((\epsilon,p)\) satisfies all the constraints.

For each real \(\lambda\in(0,1)\), take the coalition \(z=\lambda\mu\). It is admissible because \(0\le z_t\le\mu_t\) and \(\sum_t z_t=\lambda\in(0,1)\). Efficiency and the coalition constraint give

\(\displaystyle \lambda V=\sum_t p_t\lambda\mu_t\ge \nu(\lambda\mu)+\epsilon\lambda.\)

By the definition of the schema value,

\(\displaystyle \nu(\lambda\mu)=\sum_h w_h\lambda^{r(h)}\prod_{j=1}^{r(h)}\mu_{t_j}.\)

Dividing the inequality by \(\lambda>0\), we obtain

\(\displaystyle \epsilon\le V-\sum_h w_h\lambda^{r(h)-1}\prod_{j=1}^{r(h)}\mu_{t_j}.\)

There are finitely many schemas, and every \(r(h)\ge 1\). Thus, as \(\lambda\) tends to \(1\) from below, the right-hand side tends to \(V-\nu(\mu)=0\). Since the inequality holds for every \(\lambda\in(0,1)\), it follows that \(\epsilon\le 0\).

2. An explicit payment vector attains \(\epsilon=0\)

For each schema \(h=(t_1,\ldots,t_{r(h)})\), assign its entire grand-coalition contribution to its first listed type. Define

\(\displaystyle p_t=\sum_{\substack{h\\t_1=t}}w_h\prod_{j=2}^{r(h)}\mu_{t_j},\)

where an empty product equals \(1\). All these rates are nonnegative.

They satisfy efficiency:

\(\displaystyle \sum_t\mu_t p_t=\sum_h w_h\mu_{t_1}\prod_{j=2}^{r(h)}\mu_{t_j}=\nu(\mu).\)

Now let \(z\) be any vector with \(0\le z_t\le\mu_t\). For each schema, all factors are nonnegative, and \(z_{t_j}\le\mu_{t_j}\) for every occurrence \(j\). Therefore

\(\displaystyle w_h\prod_{j=1}^{r(h)}z_{t_j}\le w_h z_{t_1}\prod_{j=2}^{r(h)}\mu_{t_j}.\)

This remains valid when type indices repeat: only the first occurrence is retained as a coalition factor; each other occurrence is bounded separately by its corresponding population mass.

Summing over schemas gives

\(\displaystyle \nu(z)\le\sum_h w_h z_{t_1}\prod_{j=2}^{r(h)}\mu_{t_j}=\sum_t p_tz_t.\)

Consequently, the constructed vector satisfies every required coalition inequality with \(\epsilon=0\). Together with the upper bound, this proves that the optimum is attained and equals \(0\).

3. Exact computational complexity

The construction requires only rational products and sums. Computing each schema’s contribution takes \(r(h)-1\) multiplications, followed by one multiplication by its weight and one addition to the designated rate. Initializing the rates takes \(\tau\) operations. Thus the number of rational arithmetic operations is \(O(R+m+\tau)\).

These operations also have polynomial bit complexity. To verify this, represent each input rational as a ratio of binary integers. Each numerator and denominator has at most \(L\) bits. A schema contribution contains \(r(h)\) input factors, including its weight, so its numerator and denominator have \(O(r(h)L)\) bits.

For any rate, use the product of its summands’ denominators as a common denominator. Since \(\sum_h r(h)=R\), that denominator has \(O(RL)\) bits. Each numerator term has \(O(RL)\) bits, and summing at most \(m\) such terms adds at most \(O(\log(m+1))\) bits. Thus every output rate has a rational representation of polynomial length. Intermediate arithmetic can use the same bounds, and standard integer arithmetic therefore yields polynomial running time.

If there are no schemas, the construction simply returns all rates equal to \(0\), with the same optimum.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument is correct and fully resolves the stated atomless schema model. The optimum is \(\epsilon^*=0\), and the displayed payment vector attains it with polynomial bit complexity. No major or minor issues were found.

For every \(\lambda\in(0,1)\), the vector \(z=\lambda\mu\) is an admissible proper coalition: its coordinates satisfy the required bounds, and its total mass is exactly \(\lambda\).

Efficiency gives \(\sum_t p_tz_t=\lambda V\). The substitution into the coalition inequality and subsequent division by the positive number \(\lambda\) are valid. Each schema contributes the factor \(\lambda^{r(h)-1}\) after division, including schemas of arity \(1\), where that factor is \(1\).

The finite sum on the right converges to \(V\) as \(\lambda\) approaches \(1\) from below. Consequently, its difference from \(V\) converges to \(0\). A fixed feasible \(\epsilon\) bounded above by this difference for every \(\lambda\in(0,1)\) must satisfy \(\epsilon\le 0\). This argument does not impose a coalition constraint at the excluded whole-population endpoint.

Every schema has a first listed type because \(r(h)\ge 1\), so the proposed assignment is well defined. Nonnegative weights and positive masses make every rate nonnegative. The empty-product convention correctly handles arity \(1\).

In the efficiency calculation, each schema appears exactly once, in the rate indexed by its first type. Multiplication by that type’s mass restores precisely its grand-coalition contribution. Thus \(\sum_t\mu_t p_t=\nu(\mu)\), including when type indices repeat.

For each schema, replacing every factor after the first by its corresponding population mass can only increase the product, because all factors are nonnegative and \(z_t\le\mu_t\). Retaining the first coalition factor therefore gives the claimed upper bound.

Repeated indices do not invalidate this comparison: each occurrence is a factor satisfying the same coordinate bound. Summing the bounds and grouping schemas by their first type gives exactly \(\nu(z)\le\sum_t p_tz_t\).

The comparison holds throughout the closed coordinate box and therefore holds for every required proper coalition. It establishes feasibility at \(\epsilon=0\); combined with the upper bound, it proves attainment and optimality.

The stated arithmetic-operation count is valid. A schema contribution uses at most \(r(h)\) rational input factors, counting its weight. Repeated use of a mass is included in this count, so its numerator and denominator have \(O(r(h)L)\) bits.

For a nonempty collection of summands contributing to one rate, the product of their denominators has \(O(RL)\) bits. Expressing each numerator over that denominator preserves this bound, and summing at most \(m\) numerators adds at most \(O(\log(m+1))\) bits. Sequential rational products and sums can satisfy the same polynomial bounds. Standard exact integer arithmetic therefore gives polynomial running time and polynomial output length.

Rates receiving no contributions are exactly zero. The separately addressed case of no schemas is also correct. No cited theorem or unverified external result is needed.

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