← back to the atlas

d4-conf-sagt-2024-0014 (d4-conf-sagt-2024-0014)

Answer: Polynomial-time solvable in \(m,\tau,L\). All core allocations are exactly the optimal fractional maximal-clique covers with vertex demands \(\bar\rho w_v\); an allocation supported on at most \(m\) maximal cliques can be computed.

The anchor (named result in the paper)

Theorem 2 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateAn imputation y is in the core of the stable set game over a perfect graph if and only if it is an optimal solution to the dual LP(6).

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

The continuous mirror question, as graded

Given a perfect conflict graph \(G=(V,E)\), rational base costs \(w_v\), and a finite-support population with masses \(\mu_t\) and account scales \(\rho_t\), compute and characterize per-unit-mass firm allocations \(y_Q\) with total \(\bar\rho\alpha_w(V)\) that satisfy \(\sum_{Q:Q\cap S\ne\varnothing}y_Q\ge\bar\rho\alpha_w(S)\) for every scenario \(S\subseteq V\), where \(\bar\rho=\sum_t\mu_t\rho_t\) and \(\alpha_w(S)\) is the maximum-cost stable-set value in \(G(S)\).

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

Let \(G=(V,E)\) be a nonempty perfect graph, \(m=|V|\), with positive binary-rational asset costs \(w_v\). The firms are precisely the maximal cliques \(\mathcal M\) of \(G\), specified implicitly by the graph.
A society is given by its support: the list of its \(\tau\) types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\), and positive binary-rational account scales \(\rho_t\). Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Type \(t\) has asset costs \(\rho_t w_v\). Set \(\bar\rho=\sum_t\mu_t\rho_t\), and let \(\alpha_w(S)\) be the maximum-weight stable-set value in the induced graph \(G[S]\), with \(\alpha_w(\varnothing)=0\).
A pooled allocation per unit population mass is a vector \(y\in\mathbb Q_{\geq0}^{\mathcal M}\), represented by its nonzero clique–amount pairs, with \(\sum_{Q\in\mathcal M}y_Q=\bar\rho\alpha_w(V)\). A firm's allocation is available in any scenario containing one of its assets, counted once per firm.
Such an allocation is in the core exactly when \(\sum_{Q\in\mathcal M:\,Q\cap S\ne\varnothing}y_Q\geq\bar\rho\alpha_w(S)\) for every \(S\subseteq V\).

Is finding a core allocation polynomial-time in \(m,\tau,L\), or is it NP-hard? What is an exact characterization of all core allocations?

For the single-account version, the core is nonempty and consists exactly of optimal fractional maximal-clique covers with vertex demands \(w_v\); polynomial-time core computation is also claimed. [Vazirani](https://arxiv.org/html/2302.00608v5)
No separate result specifically addressing this support-encoded population formulation was located.

Modeling choices made when packaging the task

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

1. Result and exact characterization

Finding a core allocation is polynomial-time solvable in \(m,\tau,L\). The core is nonempty, and an allocation with at most \(m\) nonzero clique–amount pairs can be computed.

Precisely, write \(a=\bar\rho=\sum_{t=1}^{\tau}\mu_t\rho_t>0\). Then all core allocations are exactly
\[ \left\{ y\in\mathbb Q_{\geq0}^{\mathcal M}: \sum_{Q\in\mathcal M}y_Q=a\alpha_w(V),\quad \sum_{\substack{Q\in\mathcal M\\v\in Q}}y_Q\geq aw_v \ \text{for every }v\in V \right\}. \]
Equivalently, they are exactly the optimal fractional maximal-clique covers with vertex demands \(aw_v\).

Here and below, displayed expressions use the same mathematical notation as the inline expressions.

2. The scenario inequalities reduce to singleton inequalities

Define the amount covering a vertex \(v\) by
\[ c_y(v)=\sum_{\substack{Q\in\mathcal M\\v\in Q}}y_Q. \]

We first prove an equivalence that does not require perfection: for any nonnegative \(y\), all scenario inequalities hold if and only if \(c_y(v)\geq aw_v\) for every vertex \(v\).

Necessity follows by taking the scenario \(S=\{v\}\), since \(\alpha_w(\{v\})=w_v\).

For sufficiency, suppose every singleton inequality holds. Fix \(S\subseteq V\), and choose a maximum-weight stable set \(I\subseteq S\), so that \(\sum_{v\in I}w_v=\alpha_w(S)\). Each clique contains at most one vertex of \(I\). Consequently,
\[ \sum_{v\in I}c_y(v) = \sum_{Q\in\mathcal M}|Q\cap I|y_Q = \sum_{\substack{Q\in\mathcal M\\Q\cap I\ne\varnothing}}y_Q. \]
Because \(I\subseteq S\) and every \(y_Q\) is nonnegative,
\[ \sum_{\substack{Q\in\mathcal M\\Q\cap S\ne\varnothing}}y_Q \geq \sum_{v\in I}c_y(v) \geq a\sum_{v\in I}w_v = a\alpha_w(S). \]
This also covers \(S=\varnothing\), when both sides are zero.

Thus the singleton inequalities, together with the prescribed budget, give the stated exact characterization.

3. Perfection ensures nonemptiness and optimality

Consider the fractional maximal-clique cover problem
\[ \min\left\{ \sum_{Q\in\mathcal M}z_Q: z_Q\geq0,\quad \sum_{\substack{Q\in\mathcal M\\v\in Q}}z_Q\geq w_v \ \text{for every }v\in V \right\}. \]
Its linear-programming dual is
\[ \max\left\{ \sum_{v\in V}w_vx_v: x_v\geq0,\quad \sum_{v\in Q}x_v\leq1 \ \text{for every }Q\in\mathcal M \right\}. \]

The perfect-graph stable-set polytope theorem states that, for a perfect graph, the nonnegativity and clique inequalities describe the convex hull of incidence vectors of stable sets. Maximal-clique inequalities suffice: every clique is contained in a maximal clique, and \(x\) is nonnegative. This is the polyhedral fact used in [Vazirani’s single-account characterization](https://arxiv.org/html/2302.00608v5).

The theorem applies because the input graph is perfect. Therefore the dual optimum is exactly \(\alpha_w(V)\): maximizing a linear function over the convex hull of stable-set incidence vectors is equivalent to maximizing it over those incidence vectors.

Both programs are feasible and have finite optima. For the cover program, select a maximal clique containing each vertex \(v\) and assign it amount \(w_v\), adding amounts when selected cliques coincide. For the dual, \(x=0\) is feasible, and every coordinate satisfies \(x_v\leq1\), because each vertex belongs to a maximal clique. Linear-programming strong duality therefore gives
\[ \min\left\{\sum_{Q\in\mathcal M}z_Q:z\text{ covers }w\right\} =\alpha_w(V). \]
The programs have rational coefficients, so a rational optimal cover exists.

Multiplication by \(a>0\) establishes that the minimum cover cost for demands \(aw_v\) is \(a\alpha_w(V)\). By Section 2, every such optimal cover is a core allocation, and every core allocation is such an optimal cover.

In particular, if \(\mathcal C(G,w)\) denotes the single-account core, the pooled core is exactly \(a\mathcal C(G,w)\). The support-encoded population affects the answer only through \(a\).

4. Polynomial-time construction with implicit cliques

We use the following established algorithmic result.

For a perfect graph and nonnegative integer vertex weights \(W_v\) encoded in binary, an optimal fractional clique cover can be computed in time polynomial in the graph size and weight encoding length. It can be returned as at most \(m\) cliques \(C_i\), with nonnegative rational amounts \(\lambda_i\), satisfying
\[ \sum_{i:\,v\in C_i}\lambda_i\geq W_v \quad\text{for every }v,\qquad \sum_i\lambda_i=\alpha_W(V). \]
This follows from the dual-solution theorem and its perfect-graph application in [Grötschel–Lovász–Schrijver, Theorem 3.10 and Section 6, particularly page 194](https://ir.cwi.nl/pub/10046/10046D.pdf). It computes the clique list itself; it does not require an enumeration of all cliques.

The rational input weights can be handled without expanding the graph. Write \(w_v=p_v/q_v\), where \(p_v,q_v\) are positive integers, and set
\[ D=\prod_{v\in V}q_v,\qquad W_v=Dw_v. \]
Every \(W_v\) is a positive integer. Moreover, \(\log_2D=\sum_v\log_2q_v\), so \(D\) and the entire vector \(W\) have encoding lengths polynomial in \(m,L\). The graph remains the original perfect graph on \(m\) vertices.

Apply the quoted algorithm to \(G,W\). For each returned clique \(C_i\), construct a maximal clique \(Q_i\supseteq C_i\) by repeatedly adding a vertex adjacent to every current member until none remains. This takes polynomial time. Replacing \(C_i\) by \(Q_i\) preserves the total amount and can only increase vertex coverage.

Merge repeated maximal cliques and define
\[ y_Q=\frac{a}{D}\sum_{i:\,Q_i=Q}\lambda_i. \]
For every vertex \(v\),
\[ \sum_{Q\ni v}y_Q = \frac{a}{D}\sum_{i:\,v\in Q_i}\lambda_i \geq \frac{a}{D}W_v = aw_v. \]
Also, scaling weights scales every stable-set value, so \(\alpha_W(V)=D\alpha_w(V)\). Hence
\[ \sum_Qy_Q = \frac{a}{D}\sum_i\lambda_i = a\alpha_w(V). \]
Section 2 now proves that \(y\) is in the core. Extension and merging leave at most \(m\) nonzero pairs.

Finally, \(a\) is computable by exact rational arithmetic in polynomial time: products of the input denominators provide a common denominator with polynomial bit length. The clique-cover algorithm returns rational amounts with polynomial encoding length, and multiplication by \(a/D\) preserves that property. Thus both runtime and output length are polynomial in \(m,\tau,L\).

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The output establishes both the exact characterization of all core allocations and polynomial-time construction under the specified support encoding. No major or minor mathematical issues were found.

The definition \(a=\sum_{t=1}^{\tau}\mu_t\rho_t\) matches \(\bar\rho\) in the task. Positivity of the masses and account scales gives \(a>0\), so all subsequent scaling operations are valid.

The proof uses precisely the budget and scenario inequalities supplied in USER_TASK. No additional assumptions about types or individual accounts enter the argument.

Taking \(S=\{v\}\) gives \(\alpha_w(S)=w_v\). The firms counted in that scenario are exactly the maximal cliques containing \(v\). Thus every core allocation satisfies \(c_y(v)\geq aw_v\).

This step is correct for every vertex, including isolated vertices.

For each \(S\subseteq V\), a maximum-weight stable set \(I\subseteq S\) exists because the graph is finite. Since a clique meets a stable set in at most one vertex, the displayed double-counting identity is valid: each firm meeting \(I\) contributes its amount exactly once.

The inclusion \(I\subseteq S\), together with nonnegativity of every \(y_Q\), justifies the comparison between the amounts available in the two scenarios. Summing the singleton lower bounds over \(I\) then gives the required bound \(a\alpha_w(S)\).

The empty scenario is explicitly handled correctly. This establishes the claimed equivalence without using perfection.

The stated dual is the correct linear-programming dual of the fractional maximal-clique cover program.

The perfect-graph stable-set polytope theorem is stated precisely enough for its use: nonnegativity and clique inequalities describe the convex hull of stable-set incidence vectors. The input satisfies its hypothesis because \(G\) is perfect. Restricting to maximal cliques is justified by clique containment and coordinate nonnegativity.

Consequently, the dual objective has optimum \(\alpha_w(V)\). This conclusion is valid for the given rational weights.

The proposed primal feasible solution covers each vertex by assigning its weight to a selected maximal clique containing it. Coincident selections are correctly combined.

The dual is feasible at zero and bounded because every coordinate lies between zero and one. The primal objective is bounded below by zero and has a finite feasible value. Thus strong duality applies to these finite linear programs, even though the number of clique variables can be exponential.

Rational coefficients ensure a rational optimal solution. Scaling by \(a>0\) therefore proves nonemptiness and the equivalence between core allocations and optimal covers with demands \(aw_v\). The asserted equality with the scaled single-account core follows.

The cited result supports the construction claimed in Section 4. Theorem 3.10 supplies rational optimal dual coefficients with support bounded by the dimension. Section 6, printed page 194, explicitly applies it to perfect graphs to compute a fractional cover supported on at most the number of vertices. Its weighted running-time guarantee depends on binary weight length, rather than the numerical sum of the weights. See [Grötschel–Lovász–Schrijver, Theorem 3.10 and Section 6](https://ir.cwi.nl/pub/10046/10046D.pdf).

Thus the citation establishes the required algorithm that returns clique identities and amounts; the proof does not confuse computing an optimum value with constructing an allocation.

For \(w_v=p_v/q_v\), the product \(D=\prod_vq_v\) is a valid common denominator, and every \(W_v=Dw_v\) is a positive integer.

The bit-length claim is correct: \(\log_2D=\sum_v\log_2q_v\), and the total encoding length of the resulting integer weights is polynomial in \(m,L\). This conversion changes weights without increasing the graph’s vertex count.

Greedy extension preserves the clique property. Termination with no addable vertex gives an inclusion-maximal clique, as required by the task. The procedure takes polynomial time for each returned clique.

Extension can only increase coverage and preserves the sum of amounts. Merging repeated maximal cliques preserves both quantities and cannot increase support size.

The displayed calculation for \(y_Q\) correctly establishes every singleton demand. The budget calculation is also correct because \(\alpha_W(V)=D\alpha_w(V)\). Therefore the output is a core allocation with at most \(m\) nonzero pairs.

Exact computation of \(a\) has polynomial bit complexity under the listed-support encoding. The returned coefficients have polynomial encoding length, and the final rational scaling and merging preserve a polynomial output bound.

Both requested conclusions are established. No additional clarification or repair is needed.

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