← back to the atlas

d4-conf-aaai-2016-0573 (d4-conf-aaai-2016-0573)

Answer: The decision problem is in \(\mathrm{P}\). An exact optimal rational mechanism and margin can also be computed in time polynomial in \(m,\tau,L\).

The anchor (named result in the paper)

Theorem 4 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven any mechanism M : [m] × [m] →R, the induced belief model constraint DM is a power diagram. Conversely, for every power diagram given by sites vs and weights w(s), there is a mechanism M whose induced belief model constraint DM satisfies DM s = cell(vs) for all s.

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

The continuous mirror question, as graded

Given a finite-support distribution \(\mu\) over \(\tau\) complete rational belief-matrix types \(P^t\) on signal alphabet \([m]\), compute a shared payment matrix \(M\in[0,1]^{m\times m}\) maximizing \(\delta\ge 0\), subject to \(\sum_j P^t_{s,j}(M(s,j)-M(x,j))\ge\delta\) for every \(t\) with \(\mu_t>0\), signal \(s\), and alternative report \(x\ne s\). Return whether the optimum is positive, which is exactly whether one strictly truthful mechanism serves every type in the society.

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

Let \(m\ge2\). A society is given by its support: a list of \(\tau\ge1\) types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total binary input length.
Each type supplies a complete rational matrix \(P^t\in\mathbb{Q}_{\ge0}^{m\times m}\), with \(\sum_jP^t_{s,j}=1\): its subjective distribution of a distinct peer's signal conditional on observing \(s\). Every own signal has positive probability; each matrix has pairwise distinct rows and no identically zero column, ensuring stochastic relevance and positive peer-signal priors. No common prior or consistency between types is required.
A shared mechanism pays \(M(x,j)\) when an agent reports \(x\) and its peer reports \(j\). Strict truthfulness means that, conditional on every signal, truthful reporting uniquely maximizes expected payment when the peer reports truthfully; ties do not qualify.
Compute \(M\in[0,1]^{m\times m}\) maximizing \(\delta\ge0\), subject to \(\sum_{j=1}^mP^t_{s,j}(M(s,j)-M(x,j))\ge\delta\) for every \(t\in[\tau]\), \(s\in[m]\), and \(x\in[m]\setminus\{s\}\). The decision problem asks whether the optimum is positive.

Is this decision problem in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

Known results: For finite agents, minimal mechanisms' regions of unique optimal reports are precisely strict power-diagram cells, with explicit conversions in both directions ([Frongillo–Witkowski](https://home.cs.colorado.edu/~raf/media/papers/geometry.pdf)); this is a characterization, not a complexity classification of the decision problem above.
Power-diagram detection for an explicitly supplied polyhedral decomposition, including a restricted domain, is polynomial-time ([Borgwardt–Frongillo](https://arxiv.org/html/1711.06207)); that input model differs from a finite support of belief matrices. No exact continuous-support complexity classification was verified.

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}\). Moreover, an optimal rational mechanism \(\,M^\star\in[0,1]^{m\times m}\,\) and its exact optimal margin \(\delta^\star\) can be computed in time polynomial in \(\,m,\tau,L\,\).

The proof uses the explicitly listed incentive constraints directly.

1. Strict truthfulness and a positive margin

Write \([k]=\{1,\ldots,k\}\). For each \(\,t\in[\tau]\), \(\,s\in[m]\), and \(\,x\in[m]\setminus\{s\}\), define

\(\displaystyle D_{t,s,x}(M)=\sum_{j=1}^{m}P^t_{s,j}\bigl(M(s,j)-M(x,j)\bigr).\)

This is the difference between the expected payment for truthful reporting and that for reporting \(\,x\,\), conditional on type \(\,t\,\) and signal \(\,s\,\).

Consequently, \(\,M\,\) is strictly truthful exactly when every \(\,D_{t,s,x}(M)>0\,\). There are finitely many such comparisons, so strict truthfulness implies

\(\displaystyle \varepsilon=\min_{t,s,x:\,x\ne s}D_{t,s,x}(M)>0.\)

Thus \(\,(M,\varepsilon)\,\) is feasible for the stated optimization problem. Conversely, feasibility with \(\,\delta>0\,\) implies strict truthfulness for every comparison. Therefore,

\(\displaystyle \delta^\star>0\quad\Longleftrightarrow\quad\text{a strictly truthful mechanism in }[0,1]^{m\times m}\text{ exists}.\)

The positive masses ensure that every listed type belongs to the support. Their numerical values do not enter these pointwise incentive constraints.

2. Exact computation by rational linear programming

There are \(\,n=m^2+1\,\) variables: the payment entries and \(\,\delta\,\). The incentive constraints are linear because every coefficient \(\,P^t_{s,j}\,\) is supplied in the input.

The program is feasible: \(\,M=0\,\) and \(\,\delta=0\,\) satisfy every constraint. Also, for any allowed payment matrix,

\(\displaystyle D_{t,s,x}(M)\le \sum_{j=1}^{m}P^t_{s,j}=1,\)

since \(\,M(s,j)-M(x,j)\le1\,\) and the probabilities are nonnegative. Because \(\,m\ge2\,\) and \(\,\tau\ge1\,\), there is at least one incentive constraint, so every feasible solution has \(\,0\le\delta\le1\,\).

We may therefore include the redundant bound \(\,\delta\le1\,\). The feasible set is then a nonempty closed subset of \(\,[0,1]^{m^2+1}\,\), hence compact. The objective \(\,\delta\,\) is continuous, so its maximum is attained.

The resulting rational linear program has

\(\displaystyle \tau m(m-1)+2m^2+2\)

inequalities. Each incentive row contains at most \(\,2m+1\,\) nonzero coefficients, consisting of input probabilities, their negatives, and the coefficient of \(\,\delta\,\). Even a dense encoding has length polynomial in \(\,m,\tau,L\,\): its dimensions are polynomial, and each coefficient requires at most \(\,O(L+1)\,\) bits.

We now apply the standard polynomial-time theorem for rational linear programming: feasibility can be decided, and a finite attained optimum and a rational optimizer can be computed exactly, in time polynomial in the binary encoding length. Polynomial time here is in the bit-complexity model; see the introduction of [Dadush–Huiberts–Natura–Végh](https://link.springer.com/article/10.1007/s10107-023-01956-2).

All hypotheses have been checked: the program is explicitly represented, rational, feasible, and has an attained finite optimum. Hence it yields \(\,(M^\star,\delta^\star)\,\) in the required polynomial time. Comparing the exact rational number \(\,\delta^\star\,\) with zero decides the question.

3. A direct feasibility reduction handling strictness

There is also a decision procedure that avoids comparing an optimum with zero. Introduce unrestricted real variables \(\,W(s,j)\,\) and ask whether the following ordinary, non-strict rational linear system is feasible:

\(\displaystyle D_{t,s,x}(W)\ge1\qquad\text{for every }t,s,x\ne s.\)

We prove that this system is feasible exactly when the original optimum is positive.

If \(\,(M,\delta)\,\) is feasible with \(\,\delta>0\,\), set \(\,W=M/\delta\,\). Linearity gives \(\,D_{t,s,x}(W)\ge1\,\).

Conversely, suppose \(\,W\,\) satisfies this system. Set

\(\displaystyle a=\min_{s,j}W(s,j),\qquad b=\max_{s,j}W(s,j),\qquad r=b-a.\)

We have \(\,r>0\,\): otherwise all entries of \(\,W\,\) would coincide and every incentive difference would be zero. Define

\(\displaystyle M(s,j)=\frac{W(s,j)-a}{r}.\)

Then \(\,M\in[0,1]^{m\times m}\,\), and subtracting the same constant from every entry cancels in each report comparison. Therefore,

\(\displaystyle D_{t,s,x}(M)=\frac{D_{t,s,x}(W)}{r}\ge\frac1r>0.\)

Thus \(\,(M,1/r)\,\) is feasible for the original problem. This proves the equivalence and gives a polynomial-time decision procedure using rational linear feasibility alone.

The stochastic-relevance promises impose no additional difficulty for these algorithms. The finite list of beliefs already supplies every required inequality, so a geometric detection theorem is unnecessary.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the stated problem correctly: the decision problem is in \(\mathrm{P}\), and an exact rational optimal mechanism and margin can be computed in polynomial time. No major or minor mathematical issues were found.

The conclusion concerns the explicitly listed finite support in USER_TASK. It does not establish a complexity classification for an arbitrary continuously supported society.

Step-by-step verification

1. Incentive differences and strict truthfulness

The expression
\[ D_{t,s,x}(M)=\sum_{j=1}^{m}P^t_{s,j}\bigl(M(s,j)-M(x,j)\bigr) \]
correctly represents the conditional expected payment advantage of reporting truthfully over reporting \(x\), assuming the peer reports truthfully.

The equivalence between strict truthfulness and \(D_{t,s,x}(M)>0\) for every specified comparison is correct. The report set is finite, so strict superiority over every alternative is exactly unique maximization.

There are \(\tau m(m-1)\) comparisons. This number is positive because \(\tau\ge1\) and \(m\ge2\). Consequently, when all comparisons are positive, their minimum exists and is strictly positive. Choosing this minimum as the margin gives a feasible solution. Conversely, a feasible positive margin makes every comparison strictly positive.

The asserted equivalence
\[ \delta^\star>0 \quad\Longleftrightarrow\quad \text{a strictly truthful mechanism in }[0,1]^{m\times m}\text{ exists} \]
is therefore valid, with attainment of the optimum established subsequently.

The masses correctly play no numerical role in these constraints: the task requires incentives for every supported type and signal, rather than an average over types.

2. Feasibility, boundedness, and attainment

The zero payment matrix with zero margin satisfies all constraints, so the program is nonempty.

For every allowed payment matrix, each difference \(M(s,j)-M(x,j)\) is at most \(1\). Nonnegativity and row normalization of \(P^t\) therefore give
\[ D_{t,s,x}(M)\le1. \]
Since at least one incentive constraint exists, any feasible margin satisfies \(0\le\delta\le1\).

Adding \(\delta\le1\) is thus redundant. The feasible set is closed, bounded, and nonempty, and the objective is continuous. The maximum is attained. This reasoning remains valid when the optimum is zero or the feasible set has lower dimension.

3. Program dimensions and encoding length

The variable count \(m^2+1\) is correct.

The inequality count
\[ \tau m(m-1)+2m^2+2 \]
is also correct: it includes the incentive inequalities, two bounds for each payment entry, and two bounds for the margin.

For each incentive inequality, \(s\ne x\), so the two payment rows involve distinct variables. There are at most \(2m\) nonzero payment coefficients and one margin coefficient. The stated upper bound of \(2m+1\) is correct.

The coefficients are supplied rational probabilities, their negatives, or fixed small integers. Their bit lengths are bounded by \(O(L+1)\). Repeating input coefficients across a polynomial number of rows increases the encoding length only polynomially. Both dense and sparse representations therefore meet the claimed polynomial bound.

No enumeration of unlisted possible types is needed.

4. Application of rational linear programming

The prover states the relevant theorem with the necessary scope: explicitly encoded rational linear programs admit polynomial-time feasibility decisions and exact rational optimization in the bit-complexity model when the optimum is finite and attained.

Its hypotheses are satisfied here:

The cited paper’s introduction confirms the standard polynomial-time LP result in the bit-complexity model. See [Dadush–Huiberts–Natura–Végh, introduction](https://link.springer.com/article/10.1007/s10107-023-01956-2).

The prover invokes the general rational LP theorem, rather than assuming that the specialized algorithm studied in that paper applies directly. No additional specialized hypotheses are needed.

Exact rational output makes comparison of \(\delta^\star\) with zero valid. The argument does not substitute numerical approximation for strict positivity.

5. Independent feasibility reduction

The auxiliary system \(D_{t,s,x}(W)\ge1\) is an explicitly represented rational linear feasibility problem with unrestricted variables.

The forward implication is correct: division by a feasible positive margin gives
\[ D_{t,s,x}(M/\delta)\ge1. \]

For the reverse implication, the minimum and maximum of the finitely many real entries of \(W\) exist. If their difference \(r\) were zero, all entries would coincide and every incentive difference would vanish, contradicting the auxiliary constraints. Thus \(r>0\).

The normalization
\[ M(s,j)=\frac{W(s,j)-a}{r} \]
places every payment in \([0,1]\). The common additive constant cancels in every report comparison, and division by \(r>0\) preserves the inequality:
\[ D_{t,s,x}(M)=\frac{D_{t,s,x}(W)}{r}\ge\frac1r>0. \]
Hence \((M,1/r)\) is feasible for the original program. Both directions of the claimed equivalence are established.

6. Scope and repair feedback

The stochastic-relevance promises and positive own-signal probabilities introduce no omitted algorithmic constraints. The proof works for the promised inputs without using those additional structural properties.

The geometric results mentioned in the task are unnecessary because the finite support directly supplies every required incentive inequality.

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.