← back to the atlas

d4-conf-atal-2011-0057 (d4-conf-atal-2011-0057)

Answer: Polynomial-time solvable: both equalities hold for every valid instance.

The anchor (named result in the paper)

Theorem 10 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet P be an incomplete profile. Assume we consider voting trees. Then • PossCond(P) = PossCond(M(P)); • NecCond(P) = NecCond(M(P)).

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

The continuous mirror question, as graded

Given candidates, rational masses over partial-order types, and a fixed priority for pairwise ties, determine whether the profile-based possible and necessary Condorcet-winner sets equal the corresponding sets computed from the incomplete weighted majority graph. For the profile-based sets, feasible completions allocate each type’s mass among its compatible linear orders; the incomplete graph records pairwise majorities forced by the type masses.

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

Let \(C\) be a set of \(m\geq 1\) candidates, with a fixed strict total priority order for resolving pairwise ties.
A society \(P\) is given by its support: a list of \(\tau\) distinct strict partial orders \(P_i\) on \(C\), each with positive binary-rational mass \(w_i\), with \(\sum_i w_i=1\). Here \(\tau\) is the support size, not the number of possible types; let \(L\) be the total input bit length.
A feasible completion assigns nonnegative real masses \(x_{i,r}\) to the linear extensions \(r\) of each \(P_i\), satisfying \(\sum_r x_{i,r}=w_i\).
In a completion, \(a\) defeats \(b\) when the mass ranking \(a\) above \(b\) exceeds \(1/2\), or equals \(1/2\) and the priority favors \(a\). A Condorcet winner defeats every other candidate under this convention.
Define \(\operatorname{PossC}(P)\) and \(\operatorname{NecC}(P)\) using, respectively, existence of a feasible completion and every feasible completion.
The incomplete majority graph \(G(P)\) retains only forced pairwise outcomes: writing \(q_{ab}=\sum_{i:a\,P_i\,b}w_i\), include \(a\to b\) exactly when \(q_{ab}>1/2\), or \(q_{ab}=1/2\) and priority favors \(a\).
A graph completion independently orients every missing pair to obtain a tournament, with no further realizability or margin constraints. Define \(\operatorname{PossC}(G(P))\) and \(\operatorname{NecC}(G(P))\) by existence and universality over these graph completions.

Is deciding whether both \(\operatorname{PossC}(P)=\operatorname{PossC}(G(P))\) and \(\operatorname{NecC}(P)=\operatorname{NecC}(G(P))\) hold solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finite profiles with an odd number of unweighted voters, both equalities always hold, including when voting trees permit repeated candidates ([Pini et al., 2011](https://www.ifaamas.org/Proceedings/aamas2011/papers/C2_G52.pdf)).
No result settling the exact divisible-mass decision problem above was located in the literature search.

Modeling choices made when packaging the task

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

Result

Both equalities hold for every valid instance. Consequently, the decision problem is polynomial-time solvable: on the promised input domain, the answer is always “yes.”

The proof handles arbitrary positive rational masses and the stated priority rule directly. It extends the profile–graph equality discussed by [Pini et al. (2011)](https://www.ifaamas.org/Proceedings/aamas2011/papers/C2_G52.pdf).

1. A completion simultaneously maximizes a candidate’s pairwise support

Write \(a\succ_\pi b\) when the fixed priority order favors \(a\) over \(b\). For a feasible completion \(x\), let \(s_{ab}(x)\) be the total mass ranking \(a\) above \(b\).

Lemma. For any candidate \(a\), there is a feasible completion \(x^{(a)}\) satisfying
\(s_{ab}(x^{(a)})=1-q_{ba}\) for every \(b\ne a\). Moreover, every feasible completion satisfies \(s_{ab}(x)\leq 1-q_{ba}\).

Proof. Fix a support order \(P_i\), and partition the other candidates into
\(A_i=\{b\in C:b\,P_i\,a\}\) and \(B_i=C\setminus(A_i\cup\{a\})\).

Construct a total order \(r_i^{(a)}\) by concatenating:

The two restricted linear extensions exist because finite strict partial orders are acyclic.

To verify that the concatenation extends \(P_i\), it suffices to exclude relations directed from a later block to an earlier block:

Thus \(r_i^{(a)}\) is a linear extension. In this extension, \(a\) is above \(b\) exactly when \(b\,P_i\,a\) does not hold.

Assign all mass \(w_i\) to \(r_i^{(a)}\), separately for each support order. This is a feasible completion, and its support for \(a\) against \(b\) is
\(s_{ab}(x^{(a)})=\sum_{i:\,\neg(b\,P_i\,a)}w_i=1-q_{ba}\).

Conversely, the mass \(q_{ba}\) must rank \(b\) above \(a\) in every completion, so \(s_{ab}(x)\leq 1-q_{ba}\). This proves the lemma.

The essential point is that these maxima are attained simultaneously for all opponents of \(a\).

2. Possible Condorcet winners coincide

The lemma implies the following exact characterization:
\(a\in\operatorname{PossC}(P)\) if and only if, for every \(b\ne a\), either \(q_{ba}<1/2\), or \(q_{ba}=1/2\) and \(a\succ_\pi b\).

For necessity, if this condition fails for some \(b\), then either \(q_{ba}>1/2\), or \(q_{ba}=1/2\) and priority favors \(b\). Since every completion has \(s_{ab}(x)\leq 1-q_{ba}\), candidate \(a\) cannot defeat that \(b\).

For sufficiency, use \(x^{(a)}\) from the lemma. Against every opponent \(b\), its support is \(1-q_{ba}\). The stated condition makes this support either strictly greater than \(1/2\), or equal to \(1/2\) with priority favoring \(a\). Hence \(a\) defeats every opponent in this one completion.

Now consider graph completions. A candidate \(a\) can be a Condorcet winner in a graph completion exactly when \(G(P)\) has no incoming arc to \(a\):

By the definition of \(G(P)\), the absence of \(b\to a\) means precisely that \(q_{ba}<1/2\), or \(q_{ba}=1/2\) and \(a\succ_\pi b\). Thus the society and graph characterizations agree, proving
\(\operatorname{PossC}(P)=\operatorname{PossC}(G(P))\).

3. Necessary Condorcet winners coincide

For any distinct \(a,b\), every feasible completion satisfies \(s_{ab}(x)\geq q_{ab}\), because every extension of a support order containing \(a\,P_i\,b\) ranks \(a\) above \(b\).

This lower bound is attainable. Apply the lemma with distinguished candidate \(b\): in \(x^{(b)}\),
\(s_{ba}(x^{(b)})=1-q_{ab}\).
Every linear order ranks exactly one of \(a,b\) above the other, and the total mass is \(1\), so
\(s_{ab}(x^{(b)})=1-s_{ba}(x^{(b)})=q_{ab}\).

Consequently, \(a\) defeats \(b\) in every feasible completion if and only if
\(q_{ab}>1/2\), or \(q_{ab}=1/2\) and \(a\succ_\pi b\).

Indeed, this condition makes even the minimum support sufficient for victory. If it fails, the completion attaining that minimum makes \(a\) lose to \(b\).

A candidate is a necessary Condorcet winner exactly when it necessarily defeats each opponent. Therefore,
\(a\in\operatorname{NecC}(P)\) if and only if \(a\to b\) belongs to \(G(P)\) for every \(b\ne a\).

The same condition characterizes necessary Condorcet winners of the graph:

Hence
\(\operatorname{NecC}(P)=\operatorname{NecC}(G(P))\).

4. Complexity and boundary cases

These arguments prove both equalities universally, so the requested decision algorithm returns “yes” on every valid input.

The winner sets themselves can also be computed in polynomial time. Compute all \(q_{ab}\) by exact rational addition, construct \(G(P)\), and select candidates with no incoming arcs for the possible set and candidates with outgoing arcs to every opponent for the necessary set. The number of arithmetic operations is polynomial in \(m,\tau\), and exact rational arithmetic has polynomial bit complexity in \(L\). If the partial orders are represented by generating relations, their transitive closures can first be computed in polynomial time.

For \(m=1\), all opponent conditions are vacuous, and the sole candidate belongs to all four sets.

Although divisible completions are allowed, the possible-winner witness constructed above assigns each support order’s entire mass to a single linear extension. Thus no fractional splitting or realizability assumption about arbitrary graph completions is needed.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The prover resolves the assigned problem correctly. Both equalities hold for every valid instance, so the decision problem has the constant-answer algorithm stated in the output. I found no major or minor mathematical issues.

1. Simultaneous-support lemma

The construction and its verification are correct.

The computation
\(s_{ab}(x^{(a)})=\sum_{i:\neg(b\,P_i\,a)}w_i=1-q_{ba}\)
uses the stipulated normalization and is correct.

The upper bound also holds for arbitrary real-valued feasible completions: all mass belonging to a support order containing \(b\,P_i\,a\) must rank \(b\) above \(a\). Crucially, the constructed completion attains every upper bound for a fixed \(a\) simultaneously. There is no interchange of separate pairwise witnesses with a common witness.

2. Possible Condorcet winners

The characterization is correct, including its equality cases.

If \(q_{ba}>1/2\), the upper bound prevents \(a\) from defeating \(b\). If \(q_{ba}=1/2\) and priority favors \(b\), support for \(a\) is at most \(1/2\), and neither a smaller support nor an exact tie gives \(a\) victory.

Conversely, the single completion \(x^{(a)}\) gives \(a\) support \(1-q_{ba}\) against every opponent. Each stated condition therefore gives a victory under the prescribed tie rule.

The graph characterization is also exact. An incoming fixed arc excludes a Condorcet victory. Without an incoming arc, every missing incident pair can independently be oriented outward. The remaining pairs have no effect on whether \(a\) defeats every opponent.

Because the priority order is strict and total, negating the condition defining \(b\to a\) gives precisely the prover’s pairwise condition. Hence the possible-winner equality follows.

3. Necessary Condorcet winners

Both the lower bound and its attainment are verified.

Every completion has \(s_{ab}(x)\geq q_{ab}\). Applying the established lemma to \(b\) gives \(s_{ba}(x^{(b)})=1-q_{ab}\). Since each linear order ranks exactly one of the two candidates first and total mass is \(1\), the claimed identity \(s_{ab}(x^{(b)})=q_{ab}\) is correct.

Thus the stated condition on \(q_{ab}\) is necessary and sufficient for \(a\) to defeat \(b\) in every completion. When the condition fails, the minimum-attaining completion indeed makes \(a\) lose, including a tie resolved against \(a\).

The quantifiers are handled correctly: being a Condorcet winner in every completion is equivalent to defeating every opponent in every completion. To disprove necessity, one losing opponent in one completion suffices; simultaneous attainment of all pairwise minima is unnecessary.

The graph argument covers every incident pair: fixed outward, fixed inward, or missing. Its characterization therefore matches the society characterization exactly.

4. Complexity, boundaries, and scope

The constant-answer algorithm is valid on the expressly promised input domain. It need not enumerate linear extensions, construct a completion, or compute the winner sets.

The supplementary polynomial-time claim for computing those sets is also sound. There are polynomially many pairwise sums and comparisons. Exact addition of the explicitly encoded rational masses has polynomial bit complexity in \(L\); computing transitive closures, when needed, is polynomial as stated.

The \(m=1\) case is explicitly and correctly handled. Positive masses and strict partial orders ensure that feasible completions exist. Allowing real mass splitting creates no obstacle because the extremal witnesses used in the proof are themselves feasible.

The cited [Pini et al. paper](https://www.ifaamas.org/Proceedings/aamas2011/papers/C2_G52.pdf) supports the contextual profile–graph comparison. The submitted argument is self-contained and does not rely on that reference to establish the divisible-mass result.

Required repair or clarification: None.

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