← back to the atlas

d4-conf-ijcai-2017-0331 (d4-conf-ijcai-2017-0331)

Answer: Polynomial-time solvable; an admissible order can also be constructed in polynomial time.

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet A be a set of alternatives, N be a set of agents, and ≽be a preference profile over A. The problem of determining whether a top-monotonic order of ≽exists (and computing it) is polynomial-time solvable.

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

The continuous mirror question, as graded

Given a finite candidate set \(C\) and a rational distribution \(\mu\) over complete weak rankings, let \(R=\operatorname{supp}(\mu)\) and \(U_\mu=\bigcup_{r\in R}\operatorname{top}_r(C)\). Determine whether there is a linear order \(>\) of \(C\) satisfying the paper’s top-monotonicity conditions for every pair \(r,q\in R\) and every \(S\in\{C\}\cup\binom{U_\mu}{3}\), and construct such an order if one exists.

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

Let \(C\) be a nonempty finite candidate set, with \(m=|C|\). A society is given by its support: a list \(R\) of \(\tau\) distinct complete weak rankings, each with positive binary-rational mass \(\mu(r)\), where \(\sum_{r\in R}\mu(r)=1\). Here \(\tau\) is the support size, not the number of possible rankings; \(L\) is the total input bit length. Ties are permitted.
For nonempty \(S\subseteq C\), define \(t_r(S)=\{x\in S:x\succeq_r a\text{ for every }a\in S\}\), \(U_\mu=\bigcup_{r\in R}t_r(C)\), and \(\mathcal S=\{C\}\cup\binom{U_\mu}{3}\).
A strict linear order \(>\) is admissible if, for every \(S\in\mathcal S\), every \(r,q\in R\), including \(r=q\), and every \(x\in t_r(S)\), \(y\in t_q(S)\), \(z\in S\), the condition \(x>y>z\) or \(z>y>x\) implies \(y\succeq_r z\) when \(z\in t_r(S)\cup t_q(S)\), and \(y\succ_r z\) otherwise.
The additional requirement that every \(t_r(C)\) be a finite union of closed axis intervals is automatic for finite \(C\).

Is deciding whether an admissible order exists polynomial-time solvable in \(m,\tau,L\), or is it NP-hard? In the polynomial-time case, can an admissible order also be constructed in polynomial time?

For finite lists of \(n\) agents with complete weak rankings, recognition and construction of a top-monotonic order are polynomial-time solvable, with an \(O(m^4n^2)\) running-time bound (Magiera and Faliszewski, 2019).
This discrete result allows ties and does not require every candidate to be ranked globally on top by some agent.

Modeling choices made when packaging the task

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

Result. Recognition is polynomial-time solvable, and an admissible order can also be constructed in polynomial time. The reduction uses one agent per support ranking; the masses do not affect admissibility.

Reduction to a finite preference profile. Enumerate the support as \(R=\{r_1,\ldots,r_\tau\}\). Construct a profile \(P\) on candidate set \(C\), with agent set \(N=\{1,\ldots,\tau\}\), by defining

\(\displaystyle x\succeq_i y\quad\Longleftrightarrow\quad x\succeq_{r_i}y.\)

These are complete weak rankings, including precisely the original ties. For every nonempty \(S\subseteq C\), the definition of a top choice gives

\(\displaystyle t_i^P(S)=\{x\in S:x\succeq_i a\text{ for every }a\in S\}=t_{r_i}(S).\)

Consequently, the globally top-ranked candidates in \(P\) are exactly

\(\displaystyle T(P)=\bigcup_{i\in N}t_i^P(C)=\bigcup_{r\in R}t_r(C)=U_\mu.\)

Thus the family of subsets used in discrete top monotonicity is exactly \(\mathcal S\): the whole candidate set together with all three-element subsets of \(U_\mu\). This is the family in Definition 3 of Magiera and Faliszewski’s [conference paper](https://www.ijcai.org/proceedings/2017/0046.pdf).

Proof of equivalence. Fix any strict linear order \(>\) on \(C\). We show that it is admissible for the given society if and only if it is a top-monotonic order for \(P\).

The correspondence \(i\mapsto r_i\) is a bijection. Therefore, quantification over all ordered pairs of agents \(i,j\in N\) is exactly quantification over all ordered pairs of support rankings \(r,q\in R\), including equal pairs. For every such pair and every \(S\in\mathcal S\):

Hence every required implication is the same in the two problems. The remaining interval condition holds for every axis: each finite top set is the finite union of its singleton closed intervals \([x,x]\). This proves both directions of the equivalence.

In particular, the actual values of the positive masses impose no further conditions. Replacing them by any other positive masses summing to one preserves every admissible order.

Algorithm and complexity. Apply the discrete recognition-and-construction theorem supplied in the question to \(P\). Its hypotheses hold: the candidate set and agent list are finite, and every preference is a complete weak ranking. No hypothesis requires \(U_\mu=C\). The unrestricted recognition-and-construction conclusion also appears as Theorem 3 in the [conference paper](https://www.ijcai.org/proceedings/2017/0046.pdf).

If the algorithm rejects, the proved equivalence implies that no admissible order exists. If it returns an axis, that same axis is admissible for the original society.

The constructed profile has \(n=\tau\) agents. Therefore the supplied running-time bound becomes \(O(m^4\tau^2)\), with polynomial-time input processing in \(L\). Standard binary encodings of candidate indices and ranking positions give polynomial bit complexity in \(m,\tau,L\).

No replication according to the rational masses is necessary. Thus large binary-encoded denominators do not cause an expansion of the agent list.

⟨structured verdict parsed — rendered above⟩

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

Verdict: proved. The output correctly resolves both recognition and construction in polynomial time. The reduction preserves the admissibility conditions exactly, and the supplied discrete theorem applies. No major or minor mathematical issues were found.

Step-by-step verification

The prover introduces exactly one agent for each listed support ranking. Because every support ranking is a complete weak ranking, the resulting profile consists of complete weak rankings with precisely the same ties.

The correspondence between agents and support rankings is bijective. The positive masses summing to one also ensure that the support is nonempty. No multiplicity or rational-weight expansion is required.

The identity \(t_i^P(S)=t_{r_i}(S)\) follows directly from the stated definition of the copied preference relation, for every nonempty \(S\subseteq C\). It does not depend on whether preferences contain ties.

Consequently, \(T(P)=U_\mu\). This establishes equality of the globally top-ranked candidate sets, rather than merely an inclusion.

The discrete definition uses the full candidate set together with every three-element subset whose candidates are globally top-ranked by some agent. Thus the equality \(T(P)=U_\mu\) establishes exactly the required equality of subset families.

This description matches Definition 3 and its preceding notation in the [linked conference paper](https://www.ijcai.org/proceedings/2017/0046.pdf). There is no requirement that all candidates belong to \(T(P)\).

The prover checks the conditions for a fixed arbitrary strict linear order. Its correspondence preserves:

Preservation of the strict preference relation follows from copying the entire weak ranking: its strict part is unchanged.

Therefore, the argument proves equivalence for each individual axis. This is sufficient both for recognition and for transferring a constructed axis.

The singleton-interval argument is valid on a finite axis. Each finite top-choice set is a finite union of its singleton closed intervals. The cited paper also explicitly identifies this requirement as automatic for finite candidate sets.

No connectedness requirement has been substituted for the stated finite-union requirement.

The theorem supplied in USER_TASK covers finite profiles of complete weak rankings, permits ties, and provides both recognition and construction. The constructed profile satisfies these hypotheses.

The prover’s additional citation is accurate: Theorem 3 of the [conference paper](https://www.ijcai.org/proceedings/2017/0046.pdf) states unrestricted polynomial-time recognition and construction. The prover does not mistakenly invoke the earlier theorem that assumes every candidate is globally top-ranked.

Since the algorithmic theorem is explicitly supplied in the task, invoking it does not leave an obligation to reproduce its internal algorithm or proof.

Substituting \(n=\tau\) into the supplied bound gives \(O(m^4\tau^2)\) for the discrete algorithm. The prover separately accounts for polynomial-time input processing in \(L\), so it does not claim that reading arbitrarily long rational encodings takes time independent of their length.

Copying explicit rankings into a finite profile has polynomial encoding size. Candidate identifiers and ranking positions likewise have polynomial bit length. Thus the stated polynomial bit-complexity conclusion follows.

The masses occur in no admissibility comparison or threshold. With the support fixed, changing their positive values does not alter any tested condition. Large denominators therefore cause no expansion of the agent list.

Edge cases and repair feedback

The equivalence remains valid when fewer than three candidates are globally top-ranked, because both subset families then contain no three-element subsets. When there are fewer than three candidates altogether, the strict betweenness antecedent cannot hold; nothing in the reduction excludes these inputs. If the full candidate set is itself one of the listed triples, set-family duplication has no effect.

No repair or additional clarification is needed. The output establishes the claimed polynomial-time classification and polynomial-time construction.

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