← back to the atlas

d4-conf-aaai-2018-0759 (d4-conf-aaai-2018-0759)

Answer: Polynomial-time solvable in \(m,\tau,L\), with exact probabilities represented by binary-encoded integer numerators and denominators.

The anchor (named result in the paper)

Proposition 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateRMEC is anonymous and neutral. The RMEC outcome can be computed in polynomial time O(m2n) and consists of rational probabilities. Next we note that if preferences are strict, then RMEC is equivalent to random dictatorship. As a corollary, RMEC satisfies both SD-efficiency and very strong SD-participation under strict preferences.

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\) and \(\tau\) complete weak-order types \(t\), each with positive binary-rational mass \(\mu_t\) summing to \(1\), compute the exact RMEC lottery. For each \(a\in A\) and rank \(j\), set \(r_{\mu,j}(a)=\sum_t\mu_t\mathbf{1}[a\in E_j(t)]\), where \(E_j(t)\) is type \(t\)’s \(j\)-th indifference class. For each type \(t\), let \(F_\mu(t)\) be the alternatives in its top class whose rank vectors are lexicographically maximal within that class; output \(p_\mu(a)=\sum_{t:a\in F_\mu(t)}\mu_t/|F_\mu(t)|\) for every \(a\in A\).

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

Let \(A\) be a nonempty alternative set with \(m=|A|\). A society is given by its support: a list of \(\tau\) distinct complete weak-order types on \(A\), each with positive binary-rational mass \(\mu_t\), with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; let \(L\) be the total input bit length.
Represent each type explicitly by its indifference classes \(E_1(t),\ldots,E_{k_t}(t)\), ordered from best to worst, and put \(E_j(t)=\varnothing\) for \(k_t<j\le m\).
Define \(r_\mu(a)=(r_{\mu,1}(a),\ldots,r_{\mu,m}(a))\), where \(r_{\mu,j}(a)=\sum_{t:a\in E_j(t)}\mu_t\). Let \(F_\mu(t)\) contain all alternatives in \(E_1(t)\) whose rank vectors are lexicographically maximal within \(E_1(t)\).
The RMEC lottery is \(p_\mu(a)=\sum_{t:a\in F_\mu(t)}\mu_t/|F_\mu(t)|\); all tied maximizers receive equal shares. The computational problem is to output every \(p_\mu(a)\) exactly as a binary rational.

Is exact computation of this RMEC lottery polynomial-time solvable in \(m,\tau,L\), or is it NP-hard?

For an explicitly listed society of \(n\) agents with complete weak orders, RMEC has rational outcomes and is computable in \(O(m^2n)\) time. [Aziz, Luo, and Rizkallah](https://cgi.cse.unsw.edu.au/~haziz/equal_contribution.pdf).
No published complexity result for exactly the support-encoded rational-mass problem was located in the literature search.

Modeling choices made when packaging the task

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

Result and encoding convention

Exact computation of the support-encoded RMEC lottery is polynomial-time solvable in \(m,\tau,L\). The proof below controls both arithmetic bit complexity and output length.

Here “binary rational” means a fraction whose integer numerator and positive integer denominator are written in binary. If it instead means a terminating binary expansion, the requested output need not exist: with three alternatives and one completely indifferent type of mass \(1\), every probability is \(1/3\). We therefore use the fraction encoding intended for exact rational computation.

The explicit-agent result appears in Proposition 1 of [Aziz, Luo, and Rizkallah](https://cgi.cse.unsw.edu.au/~haziz/equal_contribution.pdf). The following argument directly handles the support encoding, without expanding masses into agents.

1. Compute integer rank vectors

Write each input mass as \(\mu_t=u_t/v_t\), where \(u_t,v_t\) are positive integers encoded in binary. Define \(D=\prod_{t=1}^{\tau}v_t\) and \(w_t=u_t(D/v_t)\).

Every division here is exact, and \(w_t=D\mu_t\). Consequently, \(\sum_{t=1}^{\tau}w_t=D\).

Initialize an integer table \(R_j(a)=0\) for every alternative \(a\) and every \(j\in\{1,\ldots,m\}\). For each type \(t\), each class \(E_j(t)\), and each \(a\in E_j(t)\), add \(w_t\) to \(R_j(a)\). Upon completion,

\(R_j(a)=\sum_{t:a\in E_j(t)}w_t=D\,r_{\mu,j}(a)\).

Because every type partitions the alternatives into its indifference classes, this construction uses exactly \(m\tau\) additions, besides initialization.

Multiplication of every vector coordinate by the same positive number \(D\) preserves lexicographic comparisons and equality. Thus the integer vectors \(R(a)=(R_1(a),\ldots,R_m(a))\) identify exactly the maximizers specified in the question.

2. Find every maximizer, including ties

For each type \(t\), scan its nonempty top class \(E_1(t)\), retaining an alternative with lexicographically largest integer rank vector. Then scan that class again and collect every alternative whose vector equals the retained vector.

Lexicographic order is a total order on these vectors, so the first scan finds a maximum. The second scan returns precisely \(F_\mu(t)\), including all tied maximizers.

Each comparison examines at most \(m\) integer coordinates. Each top class contains at most \(m\) alternatives, so all types together require \(O(m^2\tau)\) coordinate comparisons.

Put \(s_t=|F_\mu(t)|\). Nonemptiness of the top classes gives \(1\le s_t\le m\).

3. Accumulate the lottery with a common denominator

Define \(Q=\prod_{t=1}^{\tau}s_t\). Initialize \(P_a=0\) for every alternative. For each type \(t\), compute the integer \(c_t=w_t(Q/s_t)\), and add \(c_t\) to \(P_a\) for every \(a\in F_\mu(t)\).

These divisions are exact because every \(s_t\) divides \(Q\). The resulting numerator satisfies

\(P_a=\sum_{t:a\in F_\mu(t)}w_tQ/s_t\).

Therefore,

\(\displaystyle \frac{P_a}{DQ}=\sum_{t:a\in F_\mu(t)}\frac{w_t}{Ds_t}=\sum_{t:a\in F_\mu(t)}\frac{\mu_t}{|F_\mu(t)|}=p_\mu(a)\).

Outputting \(P_a/(DQ)\) thus gives every probability exactly.

Moreover, all numerators are nonnegative, and

\(\displaystyle \sum_{a\in A}P_a=\sum_{t=1}^{\tau}s_t\frac{w_tQ}{s_t}=Q\sum_{t=1}^{\tau}w_t=DQ\).

In particular, \(0\le P_a\le DQ\).

4. Bit complexity and output length

The total binary length of the input denominators is at most \(L\), so \(\log_2 D\le L\). Also, \(Q\le m^\tau\), giving \(\log_2 Q\le\tau\log_2 m\).

Set \(B=L+\tau\lceil\log_2(m+1)\rceil+2\). Every integer used above has at most \(B\) bits:

The algorithm performs \(O(m^2\tau)\) integer operations and coordinate comparisons. Ordinary binary addition, comparison, multiplication, and division on integers of at most \(B\) bits each take \(O(B^2)\) time or less. Thus an explicit bit-time bound for unreduced fraction output is \(O(m^2\tau B^2)\), which is polynomial in \(m,\tau,L\).

The total output length is \(O(mB)\). If reduced fractions are required, divide each numerator and denominator by their greatest common divisor; the Euclidean algorithm adds only polynomial time.

This proves the claimed polynomial-time solvability for arbitrary explicitly binary-encoded rational masses, and hence also for dyadic input masses.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved under the explicitly stated convention that an exact binary rational is represented by a binary-encoded integer numerator and denominator. The argument computes the specified lottery, preserves all ties, and establishes polynomial bit complexity and output length. No major or minor mathematical issues were found.

1. Encoding and scope

The encoding convention is appropriate for the intended exact rational computation problem. The prover explicitly distinguishes fraction encoding from terminating binary expansions.

The stated counterexample to the latter interpretation is correct: with three alternatives and one completely indifferent type of mass \(1\), all rank vectors coincide, so each alternative receives probability \(1/3\), which has no terminating binary expansion.

The argument covers arbitrary rational masses given as explicit numerator-denominator pairs, including dyadic masses. It does not rely on expanding the support into individual agents.

The bibliographic attribution is also correct: Proposition 1 of [Aziz, Luo, and Rizkallah](https://cgi.cse.unsw.edu.au/~haziz/equal_contribution.pdf) states polynomial-time computation in \(O(m^2n)\) and rational probabilities for the explicitly listed agent setting. That proposition is background here; the support-encoded conclusion is established independently.

2. Integer rank vectors

Since every denominator is positive, \(D=\prod_t v_t\) is positive and every \(v_t\) divides \(D\). Thus every \(w_t=u_t(D/v_t)\) is an integer and satisfies \(w_t=D\mu_t\).

The identity \(\sum_t w_t=D\) follows directly from the promised normalization \(\sum_t\mu_t=1\).

The table construction matches the task’s rank definition exactly: an alternative contributes to coordinate \(j\) precisely when it belongs to the \(j\)-th indifference class. Empty padded classes contribute nothing. Because each type partitions the alternatives, the claimed \(m\tau\) additions are correct.

Consequently, \(R_j(a)=D r_{\mu,j}(a)\). Scaling all coordinates by the same positive integer preserves both lexicographic comparisons and vector equality. This step correctly transfers the maximizer computation to integer arithmetic.

3. Maximizers and ties

Every top class is nonempty because the alternatives form a nonempty set and each type is a complete weak order.

Lexicographic order is a total order on the finite collection of rank vectors. The first scan therefore obtains a maximum vector, and the second scan collects exactly the alternatives attaining that vector. It neither omits tied maximizers nor includes alternatives with smaller vectors.

The bound \(1\le s_t\le m\) is valid. Each scan uses at most \(O(m)\) vector comparisons per type, with at most \(m\) coordinate comparisons per vector comparison. The resulting \(O(m^2\tau)\) bound is correct.

4. Lottery accumulation

Each \(s_t\) divides \(Q=\prod_t s_t\), so the divisions used to form \(c_t=w_t(Q/s_t)\) are exact.

The accumulated numerator satisfies the displayed formula for \(P_a\). Dividing by \(DQ\) produces precisely the contribution \(\mu_t/|F_\mu(t)|\) from every relevant type, as required by the task.

The normalization calculation correctly counts each type’s contribution \(s_t\) times. Hence \(\sum_a P_a=DQ\), and nonnegativity gives \(0\le P_a\le DQ\). Alternatives receiving no contribution are correctly output with numerator zero.

5. Bit complexity and output length

The denominator bound \(\log_2 D\le L\) follows from summing the binary lengths of the explicitly encoded denominators. The bound \(Q\le m^\tau\) follows from \(s_t\le m\).

The stated \(B=L+\tau\lceil\log_2(m+1)\rceil+2\) safely bounds the bit lengths of the arithmetic values:

Thus the proof controls intermediate values as well as final outputs. Ordinary binary arithmetic on these values has the claimed quadratic upper bound per operation. Initialization, preprocessing, comparisons, and accumulation fit within \(O(m^2\tau)\) operations, since \(m,\tau\ge1\).

The resulting \(O(m^2\tau B^2)\) bit-time bound and \(O(mB)\) output-length bound are polynomial in the requested parameters. Optional reduction by greatest common divisors also takes polynomial time.

6. Edge cases and repair feedback

The construction handles \(m=1\), \(\tau=1\), singleton maximizer sets, complete indifference, and zero output probabilities. Products equal to one cause no difficulty, and no division by zero occurs.

No additional clarification, missing lemma, or mathematical repair is needed. The polynomial-time classification is established.

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