← back to the atlas

d4-conf-atal-2014-0344 (d4-conf-atal-2014-0344)

Answer: Polynomial-time solvable

The anchor (named result in the paper)

Corollary 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateIn the global empathetic model, (global) social welfare of alternative a is given by sw g(a, uI) = ω⊤uI where ω⊤= e⊤(I −W + D)−1D. Once again, in (scoring-rule based) voting contexts one can view the global empathetic model as trading offone’s own satisfaction for a winning alternative with the “overall” sat- isfaction of one’s neighbors (not merely their intrinsic pref- erence). Fig. 1(c) illustrates the distinctions: when either Borda or plurality is used as scoring rule in this example, alternative c wins under the global model, a wins in the in- trinsic model, and b wins in the local model.

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

The continuous mirror question, as graded

Given a finite alternative set \(A\), a fixed scoring rule, ranking-and-influence-role types \(T\), rational masses \(\mu_t>0\) summing to \(1\), and rational parameters \(\alpha_t>0\) and \(p_{tt'}\geq 0\) with \(\alpha_t+\sum_{t'\in T}p_{tt'}=1\), let \(v_t(a)\) be type \(t\)'s score for \(a\). Define type utilities by \(u_t(a)=\alpha_t v_t(a)+\sum_{t'\in T}p_{tt'}u_{t'}(a)\). Return any alternative maximizing \(\mathrm{SW}_\mu(a)=\sum_{t\in T}\mu_tu_t(a)\), with running time measured in \(m\), \(\tau=|T|\), and the input bit length \(L\).

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

Let \(A\) be a nonempty set of \(m\) alternatives. Fix a positional scoring rule whose nonnegative rational scoring vector is computable in polynomial time in \(m\); each type has a strict complete ranking, giving intrinsic scores \(v_t(a)\).
A society is given by its support: a list \(T\) of \(\tau\) ranking-and-influence-role types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). The support size \(\tau\) counts listed types, not possible rankings; types with identical rankings may have different influence roles.
Each type's influence role specifies binary-rational coefficients \(\alpha_t>0\) and \(p_{tt'}\geq0\), with \(\alpha_t+\sum_{t'}p_{tt'}=1\). Here \(p_{tt'}\) is total influence assigned to type \(t'\), without an additional mass factor; \(p_{tt}\) may represent influence from other members of the same type.
For each \(a\in A\), utilities are the unique solution of \(u_t(a)=\alpha_tv_t(a)+\sum_{t'}p_{tt'}u_{t'}(a)\). Return any alternative maximizing \(\mathrm{SW}_\mu(a)=\sum_t\mu_tu_t(a)\); ties permit any maximizer. Let \(L\) be the total binary input length, and measure running time in \(m,\tau,L\).

Is this winner-computation problem solvable in time polynomial in \(m,\tau,L\), or is it NP-hard?

For finite agents, global empathetic welfare is a weighted sum of intrinsic scores under nonnegative normalized influence weights and positive intrinsic weights; winner computation is polynomial, with a stated arithmetic-operation bound of \(O(n^3+nm)\) for \(n\) agents. [Source](https://www.cs.toronto.edu/~abari/papers/emp-aamas2014-wApp.pdf)
No result explicitly treating this support-encoded mass problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result

The winner-computation problem is solvable in time polynomial in \(m,\tau,L\). After computing the scoring vector, an algorithm uses \(O(\tau^3+\tau m)\) rational arithmetic operations, with polynomially bounded operand lengths.

The algorithm operates directly on the listed types; it requires no expansion into individual agents.

1. The utility system is invertible

Index the types by \(1,\ldots,\tau\). Define \(P=(p_{tt'})\), \(D=\operatorname{diag}(\alpha_1,\ldots,\alpha_\tau)\), and let \(\mu\) be the column vector of masses. For each alternative \(a\), let \(v(a)\) and \(u(a)\) be its intrinsic-score and utility column vectors.

The defining equations are exactly

\((I-P)u(a)=Dv(a).\)

Set \(\varepsilon=\min_t\alpha_t\). Because the support is finite and every \(\alpha_t\) is positive, \(\varepsilon>0\). Nonnegativity and the row-normalization hypothesis give

\(\|P\|_\infty=\max_t\sum_{t'}p_{tt'}=\max_t(1-\alpha_t)=1-\varepsilon<1.\)

Consequently, the matrix series \(\sum_{k=0}^{\infty}P^k\) converges: its terms have norms at most \((1-\varepsilon)^k\). Moreover,

\((I-P)\sum_{k=0}^{N}P^k=I-P^{N+1},\)

and the same identity holds with the factors reversed. Taking limits proves

\((I-P)^{-1}=\sum_{k=0}^{\infty}P^k.\)

Thus the utilities exist uniquely, and

\(u(a)=(I-P)^{-1}Dv(a).\)

This series establishes invertibility and positivity. The algorithm below solves the system exactly rather than approximating it by truncating the series.

2. Welfare is a weighted positional score

Solve the single transposed system

\((I-P)^T y=\mu,\)

and define \(w=Dy\). For every alternative,

\(\mathrm{SW}_\mu(a)=\mu^T(I-P)^{-1}Dv(a)=y^TDv(a)=\sum_{t=1}^{\tau}w_tv_t(a).\)

These effective weights are positive and sum to one.

Indeed, the inverse representation gives

\(y=\sum_{k=0}^{\infty}(P^T)^k\mu.\)

Every summand is entrywise nonnegative, and the term with \(k=0\) is \(\mu\). Therefore \(y_t\geq\mu_t>0\), so

\(w_t=\alpha_ty_t\geq\alpha_t\mu_t>0.\)

For normalization, write \(\mathbf{1}\) for the all-ones column vector. The row-normalization hypothesis states that

\((I-P)\mathbf{1}=D\mathbf{1}.\)

Using \(y^T(I-P)=\mu^T\), we obtain

\(\sum_t w_t=y^TD\mathbf{1}=y^T(I-P)\mathbf{1}=\mu^T\mathbf{1}=1.\)

Thus winner computation reduces to evaluating a weighted positional score for every alternative. The masses enter through the right-hand side \(\mu\); the coefficients \(p_{tt'}\) are used exactly as given.

3. Algorithm and correctness

The algorithm is:

Section 2 proves \(S(a)=\mathrm{SW}_\mu(a)\) for every alternative. Since \(A\) is finite and nonempty, a maximum exists, and every alternative returned by step 5 satisfies the requested condition.

A dense linear solve takes \(O(\tau^3)\) arithmetic operations. Computing the weights and evaluating all alternatives takes \(O(\tau m)\) additional operations. Exact comparisons also handle ties.

It remains to verify that these operations have polynomial bit cost.

4. Exact arithmetic has polynomial bit complexity

Integer representation and determinant bounds

Let \(Q\) be the product of the positive denominators appearing in \(P\) and \(\mu\). Their total encoding length is at most \(L\), so the binary length of \(Q\) is \(O(L)\).

The transposed system is equivalent to the integer system

\(By=b,\qquad B=Q(I-P)^T,\qquad b=Q\mu.\)

Every entry of \(B\) and \(b\) has absolute value at most \(Q\): the coefficients \(p_{tt'}\) and masses \(\mu_t\) lie in \([0,1]\).

Let \(C=[B\mid b]\). For any square submatrix \(M\) of \(C\) of order \(k\), Hadamard’s inequality gives

\(|\det M|\leq(\sqrt{k}\,Q)^k.\)

Here the hypothesis of Hadamard’s inequality is satisfied because each row has \(k\) entries of absolute value at most \(Q\), and hence Euclidean norm at most \(\sqrt{k}\,Q\).

Since \(k\leq\tau\), every such determinant has binary length bounded by

\(H=O\bigl(\tau(L+\log(\tau+1))\bigr).\)

Gaussian elimination

Every principal submatrix of \(I-P\) is invertible. To see this, take a nonempty index set \(J\). The principal submatrix \(P_J\) satisfies

\(\|P_J\|_\infty\leq1-\varepsilon<1,\)

because restricting its columns cannot increase a row sum. The argument of Section 1 therefore applies to \(I-P_J\).

It follows that every leading principal submatrix of \(B\) is invertible. Gaussian elimination can consequently proceed without row exchanges and without zero pivots.

We can bound its intermediate entries explicitly. After eliminating the first \(k\) variables, let \(K=\{1,\ldots,k\}\). For an active row \(i>k\) and active column \(j>k\), including the augmented column, its entry is the Schur-complement entry

\(S^{(k)}_{ij}=C_{ij}-B_{iK}(B_{KK})^{-1}C_{Kj}.\)

The block determinant identity gives

\(S^{(k)}_{ij}=\dfrac{\det C_{K\cup\{i\},\,K\cup\{j\}}}{\det B_{KK}},\)

where the denominator for \(k=0\) is interpreted as \(1\). This identity follows by eliminating the lower-left block of the bordered matrix; the elimination has determinant one and leaves diagonal blocks \(B_{KK}\) and \(S^{(k)}_{ij}\).

Both determinants have binary length \(O(H)\), and the denominator is nonzero. Hence each active entry, represented as a reduced fraction, has numerator and denominator of length \(O(H)\). Elimination multipliers are ratios of such entries, so their lengths are also \(O(H)\). The products and differences used in one update have polynomial length before reduction.

Thus all elimination operations have polynomial bit cost.

Back substitution and score evaluation

Cramer’s rule gives

\(y_t=\dfrac{\det B^{(t)}}{\det B},\)

where \(B^{(t)}\) replaces column \(t\) of \(B\) by \(b\). Its entries also have absolute value at most \(Q\), so the determinant bounds above show that every reduced \(y_t\) has numerator and denominator length \(O(H)\).

In back substitution, each partial sum contains at most \(\tau\) products of triangular-system coefficients and already computed solution entries. Each product has length \(O(H)\). Even using the product of their denominators as a common denominator gives length \(O(\tau H)\). Therefore back substitution also has polynomial bit cost.

Multiplying \(y_t\) by the input rational \(\alpha_t\) preserves a polynomial length bound for \(w_t\).

Finally, polynomial-time computability of the fixed scoring vector implies that its rational entries have binary lengths bounded by some polynomial \(q(m)\). Each welfare value is a sum of \(\tau\) rational products \(w_tv_t(a)\). Using a common denominator formed from their denominators gives a polynomial bound in \(\tau,L,q(m)\) on every intermediate value. Exact comparison by cross multiplication therefore has polynomial bit cost as well.

Combining the polynomial number of operations with these operand-length bounds proves polynomial running time in \(m,\tau,L\).

5. Scope of the conclusion

The proof permits positive intrinsic coefficients of arbitrarily small binary-rational magnitude, influence within the same type, and distinct influence roles for identical rankings.

The weighted-score reduction is consistent with the finite-agent approach in [Salehi-Abari and Boutilier’s cited paper](https://www.cs.toronto.edu/~abari/papers/emp-aamas2014-wApp.pdf). The argument above independently establishes the result for the support-and-mass encoding, including exact bit complexity.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The argument establishes a polynomial-time algorithm for the exact support-and-mass encoding in USER_TASK. I found no major or minor issues requiring repair.

The matrix equation \((I-P)u(a)=Dv(a)\) correctly represents the stated utilities, including influence within a type. It introduces no additional mass factor.

The support is nonempty because its positive masses sum to one. Thus \(\varepsilon=\min_t\alpha_t\) exists and is positive. Nonnegativity and row normalization correctly imply
\[ \|P\|_\infty=1-\varepsilon<1. \]
The geometric norm bound establishes convergence of the matrix series. The finite telescoping identities, on both sides, establish that its limit is the inverse of \(I-P\). Existence and uniqueness therefore follow as claimed.

Entrywise nonnegativity of this inverse is established; strict positivity of every inverse entry is neither established nor needed. The subsequent strict positivity claim concerns the effective weights and is justified separately.

Invertibility justifies the unique solution of \((I-P)^Ty=\mu\). Transposition gives \(y^T=\mu^T(I-P)^{-1}\), so the displayed welfare identity and the definition \(w=Dy\) are correct.

The transposed inverse series consists of nonnegative terms and includes \(\mu\). Consequently \(y_t\geq\mu_t>0\), and multiplication by \(\alpha_t>0\) establishes \(w_t>0\).

The normalization calculation correctly uses \((I-P)\mathbf{1}=D\mathbf{1}\) and \(\mu^T\mathbf{1}=1\). Hence the effective weights sum to one.

The algorithm evaluates exactly the welfare of every alternative and returns a maximizer using exact comparisons. The finite, nonempty alternative set guarantees existence, and ties are handled correctly.

One dense rational solve requires \(O(\tau^3)\) arithmetic operations. Computing weights and evaluating all scores requires \(O(\tau m)\); selecting a maximum requires only \(O(m)\) comparisons, absorbed because \(\tau\geq1\). The stated bound explicitly excludes computation of the scoring vector, whose cost is separately polynomial by assumption.

The product \(Q\) of input denominators has binary length \(O(L)\), and it clears all denominators in \(B\) and \(b\). Omitting denominators of \(\alpha_t\) here is correct: those coefficients do not occur in this transposed system.

Every entry of \(B\) and \(b\) has absolute value at most \(Q\). The stated form of Hadamard’s inequality applies because each row of an order-\(k\) submatrix has Euclidean norm at most \(\sqrt{k}Q\). Its resulting determinant-length bound
\[ H=O\bigl(\tau(L+\log(\tau+1))\bigr) \]
is valid.

Restricting a nonnegative matrix to a principal submatrix cannot increase the relevant row sums. The invertibility argument therefore applies to every principal submatrix of \(I-P\). Transposition and multiplication by nonzero \(Q\) preserve invertibility, so all leading principal submatrices of \(B\) are invertible. This justifies elimination without row exchanges or zero pivots.

The Schur-complement formula correctly describes the active coefficients and augmented entries. The bordered determinant identity has a nonzero denominator, and both determinants fall under the preceding bounds. Reduced active fractions and elimination multipliers therefore have lengths \(O(H)\). Individual updates have polynomial intermediate lengths. Reducing fractions requires only routine polynomial-time integer arithmetic.

Cramer’s rule applies because \(B\) is invertible. Each replacement-column matrix satisfies the same entry bound, establishing polynomial lengths for the exact solution entries.

The partial-sum denominator bound in back substitution is valid: at most \(\tau\) products are combined, giving length \(O(\tau H)\) even without denominator sharing. Multiplication by input coefficients preserves polynomial lengths.

Polynomial-time computation of the rational scoring vector entails polynomial output lengths. The stated bounds on score sums and cross-multiplication comparisons therefore establish polynomial bit cost, not merely polynomial arithmetic-operation count.

The argument covers \(m=1\), \(\tau=1\), zero or tied scoring entries, arbitrarily small positive intrinsic coefficients, diagonal influence, and repeated rankings with distinct roles. It requires no population expansion.

The cited paper describes reduction of global empathetic welfare to weighted preference aggregation through a linear system, consistent with the attribution. The support-encoded result and its bit-complexity proof are established independently here. [Salehi-Abari and Boutilier](https://www.cs.toronto.edu/~abari/papers/emp-aamas2014-wApp.pdf)

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.