← back to the atlas

d4-conf-ijcai-2016-0330 (d4-conf-ijcai-2016-0330)

Answer: Polynomial-time solvable in \(\tau,L\), with \(m=1\); an optimal rational strategy uses one submass per type.

The anchor (named result in the paper)

Proposition 5 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet V ̸= C. A strategy is weakly dominant for O- rating if and only if it is an O-greedy strategy.

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

The continuous mirror question, as graded

Given rational type masses \(\mu_t\), where each type has either a rating \(a_t\in[0,1]\) or is an abstainer, let \(v\in(0,1)\) be the voter mass and \(A\) the total rating mass, with per-capita budget \(B_0=A/v\). Choose feasible mass-level bribes, including possible bribes to abstainers, with per-capita expenditure \(e\le B_0\). Compute a strategy maximizing post-bribery per-capita utility \(A'/v'-e\), where \(A'\) and \(v'\) are the resulting rating and voter masses.

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

A society is given by its support: a list of the \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. There is one rated service, so \(m=1\). Let \(L\) be the total binary input length.
Each type is either a voter with a binary-rational rating \(a_t\in[0,1]\), or an abstainer. Write \(T_V\) and \(T_\ast\) for these two sets, and define \(v=\sum_{t\in T_V}\mu_t\in(0,1)\), \(A=\sum_{t\in T_V}\mu_ta_t\), and the per-capita budget \(B_0=A/v\).
A strategy may split each type into finitely many rational submasses \(q_{tj}\geq0\), with \(\sum_jq_{tj}=\mu_t\), and assign each submass a rational per-person bribe \(b_{tj}\in[0,1]\). Its expenditure is \(e=\sum_{t,j}q_{tj}b_{tj}\leq B_0\); the zero strategy is allowed.
A voter receiving \(b\) remains a voter and acquires rating \(\min\{1,a_t+b\}\). An abstainer receiving \(b=0\) remains an abstainer; receiving \(b>0\) makes it a voter with rating \(b\). Payments exceeding a voter's remaining rating capacity are still charged.
Thus \(v'=v+\sum_{t\in T_\ast,j:b_{tj}>0}q_{tj}\) and \(A'=\sum_{t\in T_V,j}q_{tj}\min\{1,a_t+b_{tj}\}+\sum_{t\in T_\ast,j}q_{tj}b_{tj}\). Post-bribery per-capita utility is \(A'/v'-e\).

Is computing a feasible strategy maximizing \(A'/v'-e\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finite societies with abstainers, optimal objective-rating strategies are characterized, and an accompanying polynomial-time algorithm computes one. [Grandi–Turrini](https://www.ijcai.org/Proceedings/16/Papers/050.pdf)
No result settling this exact divisible-mass problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result. Computing an optimal feasible strategy is polynomial-time solvable in \(\tau,L\), with \(m=1\). An optimum requires only one submass per type.

The proof below establishes this directly for divisible masses. The related finite-society result appears in Section 3.2 of [Grandi–Turrini](https://www.ijcai.org/Proceedings/16/Papers/050.pdf).

1. Aggregate bounds

Define the original voters’ total remaining rating capacity by \(\displaystyle C=\sum_{t\in T_V}\mu_t(1-a_t)=v-A\), and put \(\displaystyle E=\min\{B_0,C\}=\min\{A/v,v-A\}\).

Consider any feasible strategy, with expenditure \(e\), and let \(x\) denote the abstaining mass it converts into voters. Thus \(v'=v+x\).

For every original voter, \(\min\{1,a_t+b_{tj}\}\leq a_t+b_{tj}\). Each converted abstainer contributes exactly its payment to the rating numerator. Summing these inequalities gives \(A'\leq A+e\).

Furthermore, every post-bribery rating lies in \([0,1]\), so \(A'\leq v'\). Consequently, its utility \(U\) satisfies both
\(\displaystyle U\leq\frac{A+e}{v+x}-e\)
and \(U\leq1-e\).

These bounds apply even when payments exceed voters’ remaining rating capacities.

2. A universal upper bound

We prove that every feasible strategy has utility at most
\(\displaystyle U^\star=\frac{A+E}{v}-E\).

If \(e\leq C\), feasibility also gives \(e\leq B_0\), hence \(e\leq E\). Since \(A+e\geq0\) and \(x\geq0\),
\(\displaystyle U\leq\frac{A+e}{v+x}-e\leq\frac{A+e}{v}-e=\frac Av+\left(\frac1v-1\right)e\).
The coefficient \(\frac1v-1\) is positive because \(0<v<1\). Therefore \(U\leq U^\star\).

If \(e>C\), feasibility implies \(B_0>C\), so \(E=C\). Using \(A'\leq v'\), we obtain
\(\displaystyle U\leq1-e<1-C=\frac{A+C}{v}-C=U^\star\),
where the equality uses \(A+C=v\).

Thus the upper bound holds for every strategy, regardless of its splitting pattern or payments to abstainers.

3. A rational strategy attaining the bound

If \(C=0\), then \(A=v\) and \(E=0\). The zero strategy has utility \(1=U^\star\), and is optimal by the preceding bound.

Suppose \(C>0\). Define the rational number \(\lambda=E/C\), which lies in \([0,1]\). Use one submass \(q_t=\mu_t\) for each type, and assign
\(\displaystyle b_t=\lambda(1-a_t)\) to each voter and \(b_t=0\) to each abstainer.

These bribes are rational and lie in \([0,1]\). Since \(b_t\leq1-a_t\), no payment is wasted through saturation. The expenditure is
\(\displaystyle e=\sum_{t\in T_V}\mu_t\lambda(1-a_t)=\lambda C=E\leq B_0\).

No abstainer is converted, so \(v'=v\). The rating numerator becomes
\(\displaystyle A'=\sum_{t\in T_V}\mu_t\bigl(a_t+\lambda(1-a_t)\bigr)=A+E\).

Hence the strategy attains \(\displaystyle A'/v'-e=(A+E)/v-E=U^\star\). This proves existence and optimality, including when \(A=0\), in which case the construction gives the zero strategy.

4. Exact polynomial-time computation

Compute \(v,A,C,B_0,E\) by rational arithmetic. If \(C>0\), compute \(\lambda=E/C\) and output the bribes above; otherwise output the zero strategy.

To verify the bit complexity, let \(D\) be the product of all denominators appearing in the input masses and ratings. Its binary length is at most a constant multiple of \(L\). Each denominator of a mass or a product \(\mu_ta_t\) divides \(D\). Therefore \(v\) and \(A\) can be represented over \(D\) with numerators of \(O(L)\) bits: both quantities belong to \([0,1]\).

Subtraction, comparison, and the constant number of multiplications and divisions defining \(C,B_0,E,\lambda\) preserve polynomial bit length. Each output bribe also has polynomial bit length. The algorithm uses \(O(\tau)\) rational arithmetic operations on polynomial-length integers and outputs exactly \(\tau\) submasses. Standard exact integer arithmetic therefore gives polynomial running time in \(\tau,L\).

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The argument establishes an attainable global optimum and an exact polynomial-time algorithm for the stated divisible-mass problem. No major or minor mathematical issues were found.

All voting submasses have ratings at most \(1\), so \(A'\leq v'\). Since \(v'=v+x\geq v>0\), both stated utility bounds follow legitimately.

When \(C>0\), \(\lambda=E/C\) is rational and belongs to \([0,1]\). The proposed bribes satisfy \(0\leq b_t\leq1-a_t\leq1\), preserve each type’s full mass, and leave abstainers unconverted. The expenditure calculation gives \(e=E\leq B_0\); the numerator calculation gives \(A'=A+E\). Thus the construction attains the universal upper bound exactly.

If \(A=0\), then \(B_0=E=\lambda=0\), so the construction correctly returns the zero strategy. No limiting argument or unattained supremum is involved.

The remaining aggregate computations involve only a constant number of rational operations, and each output bribe involves a constant number more. Their bit lengths remain polynomial. Computing the aggregates and producing one submass per listed type uses \(O(\tau)\) rational operations on polynomial-length integers. This establishes polynomial running time and polynomial output length under the task’s explicit rational encoding.

No additional clarification or repair is required.

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