← back to the atlas

Determining Possible and Necessary Winners under Common Voting Rules Given Partial Orders (d4-conf-aaai-2008-0348)

Answer: polynomial-time solvable

The anchor (named result in the paper)

Corollary 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximatePW and PcW are NP-complete with respect to Borda, even when the number of undetermined pairs in each vote is no more than 4.

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

The continuous mirror question, as graded

Given candidates \(C\), a rational distribution \(\mu\) over partial-order types \(O\) on \(C\), each with at most four undetermined pairs, and target \(c^\star\), decide whether there are masses \(x_{O,V}\ge0\) for linear extensions \(V\supseteq O\) such that \(\sum_{V\supseteq O}x_{O,V}=\mu_O\) for every \(O\), and \(\sum_{O,V}x_{O,V}s_{\mathrm{Borda}}(V,c^\star)\ge\sum_{O,V}x_{O,V}s_{\mathrm{Borda}}(V,a)\) for every \(a\ne c^\star\).

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

Let \(\mathcal L(O)\) be the linear orders extending a partial order \(O\) on candidates \(C\). The input gives rational masses \(\mu_O\) for finitely many \(O\), each with at most four undetermined pairs, and a candidate \(c^\star\).

A completion chooses \(x_{O,V}\ge 0\) for every \(V\in\mathcal L(O)\), with \(\sum_{V\in\mathcal L(O)}x_{O,V}=\mu_O\). It makes \(c^\star\) a Borda co-winner when \(\sum_{O,V}x_{O,V}s_{\mathrm{Borda}}(V,c^\star)\ge\sum_{O,V}x_{O,V}s_{\mathrm{Borda}}(V,a)\) for every \(a\ne c^\star\).

Target. Is this Mass-Borda Possible Co-Winner problem solvable in polynomial time, or is it NP-hard?

Nearest known results. The discrete Borda Possible Winner and Possible Co-Winner problems are NP-complete even when every partial order has at most four undetermined pairs. No verified result is listed here for the exact rational-mass formulation above.

Prover output (gpt-6-astra / medium, Bolzano prover prompt)

Result

Mass-Borda Possible Co-Winner is solvable in polynomial time. The bound on undetermined pairs gives at most \(16\) linear extensions per input partial order. Since masses may be split, the problem is exactly a rational linear-programming feasibility problem of polynomial size.

1. Enumerating the linear extensions

Let \(m=|C|\), and let \(q\) be the number of input partial orders. An undetermined pair of a partial order \(O\) is an unordered pair of distinct candidates that are incomparable in \(O\). Write \(k_O\) for their number; by hypothesis, \(k_O\leq 4\).

Lemma. The set \(\mathcal L(O)\) has at most \(2^{k_O}\leq 16\) elements and can be enumerated in polynomial time.

Proof. Every linear extension specifies one of the two orientations of each undetermined pair. These orientations uniquely determine the extension: all other pairwise comparisons are already fixed by \(O\). Thus the map from extensions to orientation choices is injective, proving the bound.

For enumeration, first compute the transitive closure of the given partial-order representation, so that every determined comparison is available. For each of the \(2^{k_O}\) orientation choices, form the directed graph containing the comparisons of \(O\) and the chosen orientations. This graph contains exactly one directed edge for each unordered pair of distinct candidates.

If the graph contains a directed cycle, no linear order can respect all its edges, so discard that choice. Otherwise, a topological ordering exists. It is unique because the edge between any two candidates fixes their relative order. This ordering extends \(O\).

Conversely, any linear extension supplies an orientation choice whose graph is acyclic, and the procedure recovers that extension. Transitive closure, cycle detection, and topological sorting all take polynomial time; there are at most \(16\) choices. This proves the lemma. ∎

2. The linear program

For each enumerated extension \(V\in\mathcal L(O)\), introduce a real variable \(x_{O,V}\). Let \(\operatorname{pos}_V(a)\) denote the position of candidate \(a\), with the first position numbered \(1\). Define its Borda score by \(s(V,a)=m-\operatorname{pos}_V(a)\).

Construct the following feasibility system:

\(\displaystyle \sum_O\sum_{V\in\mathcal L(O)}\bigl(s(V,c^\star)-s(V,a)\bigr)x_{O,V}\geq 0.\)

Equivalence. A completion making \(c^\star\) a co-winner assigns nonnegative masses satisfying mass conservation. Subtracting each rival’s total score from the total score of \(c^\star\) gives precisely the corresponding co-winner inequality. Hence that completion is feasible for the system.

Conversely, a feasible solution assigns admissible masses to every linear extension and conserves each input mass. Each co-winner inequality says that the total score of \(c^\star\) is at least the corresponding rival’s total score. Thus the feasible solution is a successful completion.

This equivalence is exact; it does not use any rounding or approximation.

3. Encoding size and polynomial-time feasibility

The number of variables is \(N=\sum_O|\mathcal L(O)|\leq 16q\). There are \(N\) nonnegativity inequalities, \(q\) mass equalities, and \(m-1\) co-winner inequalities. Each equality can be replaced by two inequalities.

Every coefficient on the left is an integer of absolute value at most \(\max\{1,m-1\}\), requiring \(O(\log(m+1))\) bits. The right-hand sides are zero or input rational masses, up to sign. Consequently, the complete rational system has encoding length polynomial in the original input length.

We now apply the standard rational linear-programming theorem: feasibility of an explicitly given system of rational linear inequalities can be decided in time polynomial in its total binary encoding length. This is exact feasibility, including systems with equality constraints; see [Trevisan’s linear-programming notes](https://theory.stanford.edu/~trevisan/books/cs261.pdf).

The hypotheses hold here: the system is explicit, every coefficient is rational, and its encoding length is polynomial. Enumerating the extensions, constructing the system, and deciding feasibility therefore all take polynomial time.

4. Why the discrete hardness result does not transfer

A discrete voter must choose a single extension. Here, the mass associated with a partial order may be distributed among several extensions. Consequently, the displayed system has continuous variables and requires no integrality constraints. The cited discrete hardness result concerns a different feasible set and does not establish hardness for this formulation.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6-astra / low, Bolzano verifier prompt)

Verdict: proved. The output resolves the assigned rational-mass problem in polynomial time. I found no major or minor gaps requiring repair.

The prover explicitly defines undetermined pairs as incomparable pairs, so the bound applies after taking transitive closure. Each linear extension determines an orientation of every incomparable pair. Two extensions with identical orientations agree on every pair of distinct candidates and therefore are identical. Thus \(|\mathcal L(O)|\leq 2^{k_O}\leq 16\). The argument only requires injectivity; it does not incorrectly assume every orientation choice is realizable.

After closure, the fixed comparisons and chosen orientations specify exactly one direction for every pair of distinct candidates. A cycle prevents any compatible linear order. An acyclic choice has a topological ordering, and the fixed direction between every two distinct candidates makes that ordering unique. Every extension supplies an acyclic orientation choice and is recovered. The closure and graph operations are polynomial, and there are at most \(16\) choices per partial order. Comparisons here are naturally the strict comparisons between distinct candidates.

There is a variable for every permitted extension, and the nonnegativity and conservation constraints match the completion definition. The score convention \(s(V,a)=m-\operatorname{pos}_V(a)\) is standard Borda scoring. Each rival inequality is exactly the designated candidate’s total score minus that rival’s total score, required to be nonnegative. Consequently, both directions of the claimed equivalence hold. Ties are correctly allowed, and no normalization of total mass is needed.

The task specifies rational input masses but imposes no integrality restriction on completion variables. Real LP variables therefore match the stated completion model. The argument does not substitute an approximate or discrete feasibility problem.

The variable count \(N\leq 16q\) and constraint counts are accurate. Borda-score differences have absolute value at most \(m-1\); conservation and nonnegativity introduce coefficients of magnitude at most \(1\). Hence the stated bound \(\max\{1,m-1\}\) covers all coefficients, including \(m=1\). Replacing equalities by two inequalities preserves feasibility and increases size only polynomially. Rational right-hand sides retain the input masses’ bit lengths. Under the ordinary explicit representation of candidates and partial orders, the complete system has polynomial binary encoding length.

The prover states the required theorem for explicit rational linear inequalities and verifies its hypotheses. The cited notes confirm polynomial-time feasibility determination and explicitly measure input size using the binary representation of rational coefficients; see Sections 5.2.4–5.2.5 of [Trevisan’s notes](https://theory.stanford.edu/~trevisan/books/cs261.pdf#page=42). Equality constraints and feasible sets with empty interior do not invalidate the stated theorem. Thus exact feasibility, rather than numerical approximation, supports the conclusion.

With \(k_O=0\), the enumeration considers the sole empty orientation choice. Zero input masses are handled by conservation and nonnegativity. With \(m=1\), there are no rival inequalities. With no input orders, all total scores are zero and the empty system is feasible. These cases are already covered by the formulation. The designated candidate’s membership in \(C\) excludes an empty candidate set.

The prover correctly identifies the difference between selecting one extension for each discrete voter and splitting mass among extensions. It claims only that the cited discrete hardness result does not establish hardness for this continuous formulation. That statement is justified.

No additional lemma, computation, or clarification is needed to verify the claimed result.

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