← back to the atlas

d4-conf-ecai-2024-0018 (d4-conf-ecai-2024-0018)

Answer: Polynomial-time solvable

The anchor (named result in the paper)

Proposition 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFinding one CXp (Algorithm 1) can be done in Θ(nm2) and finding one iAXp (Algorithm 2) in Θ(nm3).

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 \(\tau\) complete rankings, and a Borda winner \(w\), choose rational masses \(x_{t,p}\ge 0\) for partial rankings \(p\subseteq t\), with \(\sum_{p\subseteq t}x_{t,p}=\mu_t\). Require that for every opponent \(c\), \(\sum_{t,p}x_{t,p}\underline{s}_p(w)\ge\sum_{t,p}x_{t,p}\overline{s}_p(c)\), where the score bounds range over completions of \(p\); ties count as wins. Restrict each partial ballot to have either no hidden entries or at least two, and minimize \(\sum_{t,p}x_{t,p}|p|\), the average number of disclosed ranking entries per person.

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

Let \(C\) contain \(m\ge2\) candidates. A society is given by its support: \(\tau\) distinct strict complete rankings \(t\), each with positive binary rational mass \(\mu_t\), where \(\sum_t\mu_t=1\). The parameter \(\tau\) is the support size, not the number of possible rankings. Let \(w\in C\) be a Borda winner of this society; ties count as wins.
A partial ballot \(p\subseteq t\) discloses selected candidate–position entries of \(t\), retaining their absolute positions. Its other entries are hidden; a completion is any complete ranking agreeing with all disclosed entries. Require either zero or at least two hidden entries, and let \(|p|\) count disclosed entries.
Write \(s_q(c)\) for the Borda score of \(c\) in complete ranking \(q\), and define \(\underline{s}_p(c)=\min_{q\text{ completing }p}s_q(c)\) and \(\overline{s}_p(c)=\max_{q\text{ completing }p}s_q(c)\).
Choose rational masses \(x_{t,p}\ge0\) over admissible partial ballots, satisfying \(\sum_{p\subseteq t}x_{t,p}=\mu_t\) and, for every \(c\in C\setminus\{w\}\), \(\sum_{t,p}x_{t,p}\underline{s}_p(w)\ge\sum_{t,p}x_{t,p}\overline{s}_p(c)\). The disclosure cost is \(\sum_{t,p}x_{t,p}|p|\).
Given a binary rational budget \(B\in[0,m]\), is deciding whether feasible masses of disclosure cost at most \(B\) exist solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), and the total input bit length \(L\), including the budget.
For a finite society of \(n\) voters, one inclusion-minimal contrastive explanation can be found in \(\Theta(nm^2)\), and one inclusion-minimal abductive explanation subject to the same restriction on hidden entries in \(\Theta(nm^3)\). These algorithms find one minimal explanation, without guaranteeing minimum disclosure cost.

Modeling choices made when packaging the task

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

Proven result and running time. The decision problem is polynomial-time solvable. An equivalent rational linear program has \(O(\tau m^3)\) variables and constraints. Its construction and solution take

\( \bigl(L+\tau m^3\log(2\tau m)\bigr)^{O(1)} \)

bit operations. The input length \(L\) includes the budget. The same construction also permits computation of the minimum disclosure cost.

The essential point is that, after fixing the two extreme hidden positions and whether \(w\) is hidden, all remaining hiding choices can be represented exactly by their marginal masses.

1. Score bounds from hidden positions.

Use Borda scores \(m-1,\ldots,0\). For a ranking \(t\), let \(r_t(c)\) be the position of candidate \(c\), and write \(a_t(c)=m-r_t(c)\).

A partial ballot is determined by its hidden candidate set \(H\): every candidate outside \(H\) retains its position from \(t\). If \(H\ne\varnothing\), put

\( i=\min_{c\in H}r_t(c),\qquad j=\max_{c\in H}r_t(c). \)

The admissibility restriction gives \(i<j\). The unfilled positions are precisely the original positions of candidates in \(H\). Any hidden candidate can occupy any unfilled position, because the other hidden candidates can be assigned bijectively to the remaining positions. Consequently,

\( \underline{s}_p(w)= \begin{cases} a_t(w),&w\notin H,\\ m-j,&w\in H, \end{cases} \)

and, for every rival \(c\),

\( \overline{s}_p(c)= \begin{cases} a_t(c),&c\notin H,\\ m-i,&c\in H. \end{cases} \)

Thus these bounds depend on the extreme hidden positions and on which individual candidates are hidden.

2. Partitioning partial ballots into polynomially many groups.

Fix \(t\), and let \(c_{t,k}\) denote its candidate at position \(k\). Apart from the fully disclosed ballot, group admissible partial ballots by a triple \(\rho=(i,j,e)\), where \(i<j\) and \(e\in\{0,1\}\) records whether \(w\) is hidden.

Include precisely the triples satisfying the following conditions:

For an included triple, define the mandatory hidden set

\( F_{t,\rho}=\{c_{t,i},c_{t,j}\}\cup \begin{cases} \{w\},&e=1,\\ \varnothing,&e=0, \end{cases} \)

and the optional hidden set

\( U_{t,\rho}=\{c\in C\setminus\{w\}:i<r_t(c)<j\}. \)

The hidden sets in this group are exactly

\( H=F_{t,\rho}\cup K,\qquad K\subseteq U_{t,\rho}. \)

Indeed, the endpoints must be hidden; candidates outside the interval must be disclosed; and the status of \(w\) is fixed by \(e\). Every other interior candidate can independently be hidden or disclosed. Conversely, every such choice has extreme hidden positions \(i,j\), has the prescribed status of \(w\), and hides at least two entries.

Therefore every admissible partial ballot belongs to exactly one group, or is fully disclosed. There are at most \(2\binom m2\) groups per ranking.

Write

\( h_{t,\rho}=m-i,\qquad \ell_{t,\rho}= \begin{cases} a_t(w),&e=0,\\ m-j,&e=1. \end{cases} \)

Within this group, the lower score of \(w\) is always \(\ell_{t,\rho}\).

3. The compact linear program.

Introduce the following variables for each support ranking \(t\):

Impose

\( z_{t,0}\ge0,\qquad z_{t,\rho}\ge0,\qquad 0\le y_{t,\rho,u}\le z_{t,\rho}, \)

and the mass-conservation equations

\( z_{t,0}+\sum_\rho z_{t,\rho}=\mu_t. \)

For each candidate \(c\), define the following linear expression for its hidden mass within a group:

\( v_{t,\rho,c}= \begin{cases} z_{t,\rho},&c\in F_{t,\rho},\\ y_{t,\rho,c},&c\in U_{t,\rho},\\ 0,&\text{otherwise}. \end{cases} \)

The contribution of this group to the aggregate upper score of a rival \(c\) is

\( a_t(c)z_{t,\rho} +\bigl(h_{t,\rho}-a_t(c)\bigr)v_{t,\rho,c}. \)

To verify this expression, the mass \(z_{t,\rho}-v_{t,\rho,c}\) discloses \(c\), giving upper score \(a_t(c)\), while the mass \(v_{t,\rho,c}\) hides \(c\), giving upper score \(h_{t,\rho}\).

For every \(c\ne w\), impose the linear inequality

\( \sum_t\left[ a_t(w)z_{t,0}+\sum_\rho\ell_{t,\rho}z_{t,\rho} \right] \ge \sum_t\left[ a_t(c)z_{t,0} +\sum_\rho\left( a_t(c)z_{t,\rho} +\bigl(h_{t,\rho}-a_t(c)\bigr)v_{t,\rho,c} \right) \right]. \)

Within a group, every ballot hides all of \(F_{t,\rho}\), and each optional candidate contributes one further hidden entry exactly when it is hidden. Hence the aggregate disclosure cost is the linear expression

\( D=\sum_t\left[ m z_{t,0} +\sum_\rho\left( (m-|F_{t,\rho}|)z_{t,\rho} -\sum_{u\in U_{t,\rho}}y_{t,\rho,u} \right) \right]. \)

Finally, impose \(D\le B\).

4. Proof of exact equivalence.

First suppose rational masses \(x_{t,p}\) satisfy the original problem. Set \(z_{t,0}=x_{t,t}\). For every group, let \(z_{t,\rho}\) be the sum of its ballot masses, and let \(y_{t,\rho,u}\) be the sum over its ballots hiding \(u\).

These variables are rational and satisfy the bounds and mass-conservation equations. The formulas above show that their aggregate score bounds and cost equal those of the original masses. Thus they satisfy the compact linear program.

For the converse, suppose the compact program has a rational feasible solution. We explicitly realize every group by admissible partial ballots.

Fix a group and abbreviate its mass by \(z\). List its optional candidates as \(u_1,\ldots,u_k\), ordered so that

\( 0\le y_1\le\cdots\le y_k\le z,\qquad y_a=y_{t,\rho,u_a}. \)

Set \(y_0=0\), \(y_{k+1}=z\), and define

\( \beta_r=y_{r+1}-y_r,\qquad 0\le r\le k. \)

Assign mass \(\beta_r\) to the partial ballot with hidden set

\( F_{t,\rho}\cup\{u_{r+1},\ldots,u_k\}. \)

For \(r=k\), the optional set is empty. For \(k=0\), this construction simply assigns mass \(z\) to the ballot hiding \(F_{t,\rho}\).

All these masses are nonnegative rational numbers. They sum to

\( \sum_{r=0}^{k}\beta_r=y_{k+1}-y_0=z. \)

Moreover, \(u_a\) is hidden precisely in the ballots indexed by \(r<a\). Its total hidden mass is therefore

\( \sum_{r=0}^{a-1}\beta_r=y_a-y_0=y_a. \)

Thus the construction realizes exactly every prescribed optional hidden mass. Every resulting ballot is admissible because its mandatory hidden set contains the two distinct endpoint candidates.

Apply this construction to all groups and assign \(z_{t,0}\) to the fully disclosed ballot. The reconstructed masses sum to \(\mu_t\) for each ranking. Their score bounds and disclosure cost equal the corresponding linear expressions, so all original constraints hold.

This proves equivalence for rational solutions. Standard rational linear-programming algorithms return a rational feasible point whenever this rational system is feasible, so rationality introduces no additional obstacle.

5. Size and bit complexity.

There are \(O(m^2)\) groups per support ranking, each with at most \(m\) optional candidates. Consequently, the program has \(O(\tau m^3)\) variables and constraints.

Its sparse coefficient count is also \(O(\tau m^3)\):

All coefficients introduced by the construction are integers of magnitude at most \(m\). The remaining rational data are the original masses and budget. Including coefficient indices, a sparse encoding therefore has length

\( S=O\bigl(L+\tau m^3\log(2\tau m)\bigr). \)

The program can be constructed in polynomial time in this bound. The polynomial-time theorem for rational linear programming then decides feasibility in \(S^{O(1)}\) bit operations: all its hypotheses hold because the program has finitely many variables and constraints and explicitly encoded rational coefficients. Converting the sparse representation to a dense one, if needed, adds only polynomial overhead.

Since the rankings are explicitly supplied, this is polynomial in the total input length. The reconstruction above uses only \(O(\tau m^3)\) partial ballots and is likewise polynomial-time.

The given inclusion-minimal explanation algorithms do not establish minimum-cost optimality. Here, minimum cost follows by minimizing \(D\) over the compact program. Its feasible region is nonempty before imposing the budget: full disclosure is feasible because the supplied \(w\) is a Borda winner. All variables are bounded by their ranking’s mass, so the minimum is attained.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument establishes that the decision problem is polynomial-time solvable. The compact linear program represents the original rational-mass problem exactly, and its encoding size supports the claimed bit-complexity bound. I found no major or minor issues requiring repair.

1. Score bounds

The identification of a partial ballot with its hidden candidate set \(H\) is valid because every disclosed candidate retains its absolute position from \(t\).

For nonempty admissible \(H\), the restriction on hidden entries ensures \(|H|\ge2\). Since positions are distinct, its extreme positions satisfy \(i<j\).

The completion argument is correct: the available positions are precisely those originally occupied by candidates in \(H\), and any hidden candidate can occupy any one of these positions. The remaining hidden candidates can fill the remaining positions bijectively. Therefore:

These are exactly the bounds appearing in the original task. No assumption that all candidates attain their individual extrema in one common completion is needed: the task itself imposes inequalities using the individual score bounds.

2. Partition into groups

The conditions for including a triple \((i,j,e)\) are necessary and sufficient.

When \(e=1\), \(w\) must lie within the hidden-position interval. Adding \(w\) to the mandatory hidden set enforces its hidden status, whether it occupies an endpoint or an interior position.

When \(e=0\), \(w\) cannot occupy either hidden endpoint. If it lies strictly inside the interval, its exclusion from \(U_{t,\rho}\) correctly forces it to remain disclosed.

The mandatory and optional sets are disjoint. Every hidden set in the group has exactly the stated form \(F_{t,\rho}\cup K\), where \(K\subseteq U_{t,\rho}\). Conversely, each such set has the prescribed endpoints and the prescribed status of \(w\), and contains at least two candidates.

Uniqueness follows because every nonempty admissible hidden set determines its endpoints and the hidden status of \(w\) uniquely. Full disclosure is handled separately. The bound of at most \(2\binom m2\) groups per ranking is correct.

3. Compact linear program

The variables have the stated interpretations, and the bounds \(0\le y_{t,\rho,u}\le z_{t,\rho}\) are necessary for optional hidden masses.

For each rival \(c\), the expression
\[ a_t(c)z_{t,\rho} +\bigl(h_{t,\rho}-a_t(c)\bigr)v_{t,\rho,c} \]
correctly combines the disclosed mass, with upper score \(a_t(c)\), and hidden mass, with upper score \(h_{t,\rho}\).

The lower score of \(w\) is constant within each group because its hidden status and the largest hidden position are fixed. Thus the winner inequalities reproduce the original inequalities exactly.

The disclosure-cost expression is also correct. Every ballot in a group hides \(|F_{t,\rho}|\) mandatory entries, and the aggregate number of optional hidden entries is \(\sum_{u\in U_{t,\rho}}y_{t,\rho,u}\). Subtracting these from the total entry mass gives the stated cost.

4. Exact equivalence and rationality

The forward direction correctly aggregates original ballot masses into group masses and optional hidden masses. It preserves each ranking’s total mass, every score-bound sum, and the disclosure cost.

The converse construction is valid. After sorting the optional masses, each difference \(\beta_r=y_{r+1}-y_r\) is nonnegative and rational. The differences sum to \(z\).

For optional candidate \(u_a\), the assigned hidden sets contain it exactly when \(r<a\). Consequently, its reconstructed hidden mass is exactly
\[ \sum_{r=0}^{a-1}\beta_r=y_a. \]
This verifies all prescribed marginals simultaneously. Because the constraints and objective depend only on these marginals and group masses, the reconstruction preserves everything required by the original problem.

The construction also covers the relevant boundary cases:

All reconstructed ballots meet the hidden-entry restriction. Assignments from different groups cannot conflict because the group partition is unique.

The rational linear-programming assertion is applicable: the system has explicitly encoded rational coefficients, and rational LP feasibility admits polynomial-time decision and rational feasible-point output. Therefore the use of real LP feasibility does not enlarge the original rational-feasibility problem.

5. Size and bit complexity

There are \(O(m^2)\) groups per ranking and at most \(m\) optional variables per group. Hence the claimed \(O(\tau m^3)\) bounds on variables and constraints are valid.

The sparse coefficient count is also \(O(\tau m^3)\). Group variables can occur across the rival inequalities and optional-variable bounds, while each optional variable contributes to only its bounds, its own rival’s inequality, and the cost constraint.

The coefficient-magnitude assertion withstands inspection. Scores, score differences, and disclosure counts have magnitude at most \(m\); the other structural coefficients are \(0\), \(1\), or \(-1\). The original rational masses and budget supply the remaining numerical data.

Accordingly, the sparse encoding bound
\[ S=O\bigl(L+\tau m^3\log(2\tau m)\bigr) \]
is justified. Applying polynomial-time rational LP feasibility gives the claimed
\[ \bigl(L+\tau m^3\log(2\tau m)\bigr)^{O(1)} \]
bit-operation bound. A dense representation would increase the size only polynomially.

Because each support ranking is explicitly supplied, this bound is polynomial in the input length. The argument uses \(\tau\) as the actual support size, not as the number of possible rankings.

The reconstruction uses at most \(m+1\) ballots per group, so its \(O(\tau m^3)\) ballot-count bound is valid. Sorting rational marginals and taking their differences also takes polynomial time in the LP output size.

6. Minimum cost and scope

The minimum-cost claim is supported. Before imposing the budget, full disclosure is feasible because \(w\) is a Borda winner, including when tied. Mass conservation and nonnegativity bound every group mass by its ranking’s mass, and the marginal bounds bound every optional variable. The feasible region is therefore nonempty and compact, so the linear objective attains its minimum. Rational linear-programming optimization computes it in polynomial time.

The supplied finite-society inclusion-minimal algorithms are correctly distinguished from minimum-cost optimization. Their running times are not used to justify the continuous result.

No additional clarification or missing lemma 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.