← back to the atlas

d4-conf-aaai-2014-0127 (d4-conf-aaai-2014-0127)

Answer: Both rules are polynomial-time computable in \(m,\tau,L\). Every winner satisfies \(D_\mu(b)\le 2\mathrm{OPT}_\mu\), strictly when \(\mathrm{OPT}_\mu>0\). Every AVR winner also satisfies the sharp bound \(D_\mu(b)\le \frac{2(m-1)}m\mathrm{OPT}_\mu\).

The anchor (named result in the paper)

Theorem 9 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateBoth the AVR and the MVR are strict 2- approximations of the DBRIC for any integrity constraint IC.

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

The continuous mirror question, as graded

Given an integrity constraint \(IC\) and a finite support \(S\subseteq\operatorname{Mod}(IC)\) with positive binary-rational masses \(\mu_t\) summing to \(1\), compute an AVR or MVR winner \(b\in S\) and establish that \(D_\mu(b)\le 2\min_{x\in\operatorname{Mod}(IC)}D_\mu(x)\), strictly when the minimum is positive, where \(D_\mu(x)=\sum_{t\in S}\mu_t H(x,t)\). For fixed \(m\), establish the stronger AVR bound \(D_\mu(b)\le \frac{2(m-1)}{m}\min_{x\in\operatorname{Mod}(IC)}D_\mu(x)\).

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

Let \(m\ge2\), and let \(IC\) be a consistent propositional formula over \(m\) binary issues; feasible ballots are \(\operatorname{Mod}(IC)\subseteq\{0,1\}^m\).
A society is given by its support: a nonempty list \(S\subseteq\operatorname{Mod}(IC)\) of \(\tau\) distinct types with positive binary-rational masses \(\mu_t\) summing to \(1\). Here \(\tau=|S|\) is the support size, not the number of possible types. Let \(L\) be the total input bit length, including \(IC\); state running times in \(m,\tau,L\).
Write \(H\) for Hamming distance, \(D_\mu(x)=\sum_{t\in S}\mu_tH(x,t)\), and \(\mathrm{OPT}_\mu=\min_{x\in\operatorname{Mod}(IC)}D_\mu(x)\). Define \(\mathrm{AVR}_\mu=\arg\min_{b\in S}D_\mu(b)\).
For \(q_j=\sum_{t\in S}\mu_tt_j\), define \(a^w_j=\mathbf1[q_j\ge\tfrac12]\), \(a^s_j=\mathbf1[q_j>\tfrac12]\), and \(\mathrm{Maj}_\mu=\{a^w,a^s\}\). Define \(\mathrm{MVR}_\mu=\arg\min_{b\in S}\min_{a\in\mathrm{Maj}_\mu}H(b,a)\). All minimizer ties are retained; majority ballots need not satisfy \(IC\).

Can a winner of each rule be computed in time polynomial in \(m,\tau,L\), with every \(b\in\mathrm{AVR}_\mu\cup\mathrm{MVR}_\mu\) satisfying \(D_\mu(b)\le2\mathrm{OPT}_\mu\), strictly whenever \(\mathrm{OPT}_\mu>0\)?
For each fixed \(m\ge2\), does every \(b\in\mathrm{AVR}_\mu\) additionally satisfy \(D_\mu(b)\le\frac{2(m-1)}m\mathrm{OPT}_\mu\)?

For finite electorates, both rules are polynomial-time computable and strict \(2\)-approximations of the feasible minimum-distance rule; AVR additionally has the fixed-dimension bound \(2(m-1)/m\). [Endriss and Grandi (2014)](https://cdn.aaai.org/ojs/8798/8798-13-12326-1-2-20201228.pdf).
No separate result explicitly treating this rational-mass input model was located in the literature search.

Modeling choices made when packaging the task

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

Yes. Both rules are polynomial-time computable in the rational-mass model, every winner satisfies the strict approximation guarantee, and AVR satisfies the stated fixed-dimension bound. The latter bound is sharp.

The proofs below establish these claims directly for weighted support, extending the finite-electorate bounds of [Endriss and Grandi (2014)](https://cdn.aaai.org/ojs/8798/8798-13-12326-1-2-20201228.pdf).

1. Exact computation and running time

Write each mass as \(\mu_t=u_t/v_t\), with positive integers encoded in binary. Define
\(Q=\prod_{t\in S}v_t\) and \(w_t=u_t(Q/v_t)\).
Then every \(w_t\) is a positive integer, \(\sum_t w_t=Q\), and \(\mu_t=w_t/Q\).

Because the denominator encodings are included in \(L\), the bit length of \(Q\), and hence of every \(w_t\), is \(O(L)\). Using schoolbook integer arithmetic, these integers can be computed in \(O(\tau L^2)\) bit operations.

For each issue, compute \(N_j=\sum_{t\in S}w_tt_j\), so \(q_j=N_j/Q\). For every \(b\in S\), its AVR score can then be computed as the integer
\[ Q D_\mu(b)=\sum_{j:b_j=0}N_j+\sum_{j:b_j=1}(Q-N_j). \]
These scores have \(O(L+\log m)\) bits. Comparing them returns an AVR winner, or all AVR winners.

The majority ballots are computed by the exact comparisons \(2N_j\ge Q\) and \(2N_j>Q\). Computing the two Hamming distances for each support type and comparing their minima returns an MVR winner, or all MVR winners.

Thus a sufficient bound for computing either rule, including all its winners, is
\[ O\!\left(L+\tau L^2+m\tau(L+\log m)\right) \]
bit operations. Every returned ballot is feasible because it belongs to the supplied support.

2. The unconstrained minimum

Define
\[ C=\sum_{j=1}^m\min\{q_j,1-q_j\}. \]
For any ballot \(x\), exchanging the two finite sums in the definition of \(D_\mu\) gives
\[ D_\mu(x)=\sum_{j:x_j=0}q_j+\sum_{j:x_j=1}(1-q_j). \]
Each coordinate contributes at least \(\min\{q_j,1-q_j\}\). Both specified majority ballots attain this minimum on every coordinate, including tied coordinates. Consequently,
\[ D_\mu(a)=C\quad\text{for every }a\in\mathrm{Maj}_\mu, \qquad C\le\mathrm{OPT}_\mu. \]

If \(C=0\), each coordinate is unanimous. Positivity of all masses therefore implies that every support type is the same ballot \(a\). This ballot is feasible, so both rules return \(a\), with \(D_\mu(a)=\mathrm{OPT}_\mu=0\). In particular, \(\mathrm{OPT}_\mu>0\) implies \(C>0\).

3. Every MVR winner satisfies the strict bound

Fix an arbitrary \(b\in\mathrm{MVR}_\mu\). Choose \(a\in\mathrm{Maj}_\mu\) attaining \(r=\min_{a'\in\mathrm{Maj}_\mu}H(b,a')\).

For every \(t\in S\), the definition of an MVR winner gives
\[ r\le\min_{a'\in\mathrm{Maj}_\mu}H(t,a')\le H(t,a). \]
By the triangle inequality,
\[ H(b,t)\le H(b,a)+H(a,t)=r+H(a,t)\le2H(a,t). \]

If \(r>0\), retain the exact zero contribution from \(t=b\). Since \(\mu_b>0\),
\[ D_\mu(b) =\sum_{t\ne b}\mu_tH(b,t) \le2\sum_{t\ne b}\mu_tH(a,t) =2C-2\mu_b r <2C \le2\mathrm{OPT}_\mu. \]

If \(r=0\), then \(b=a\), so \(D_\mu(b)=C\le\mathrm{OPT}_\mu\). Whenever \(\mathrm{OPT}_\mu>0\), this also implies \(D_\mu(b)<2\mathrm{OPT}_\mu\).

This proves the required bound for every MVR winner, without breaking any minimizer ties.

For every \(b\in\mathrm{AVR}_\mu\) and every \(c\in\mathrm{MVR}_\mu\), we have \(D_\mu(b)\le D_\mu(c)\), because \(c\in S\). Hence every AVR winner inherits the same guarantee.

4. The fixed-dimension AVR bound

Fix any \(a\in\mathrm{Maj}_\mu\), and define
\[ p_j=\sum_{t\in S}\mu_t\mathbf1[t_j\ne a_j]. \]
Then \(p_j=\min\{q_j,1-q_j\}\) and \(\sum_jp_j=C\).

Let \(V=\min_{b\in S}D_\mu(b)\), the common objective value of all AVR winners.

If \(a\in S\), then \(V=C\): the inequality \(V\le C\) follows by selecting \(a\), and \(V\ge C\) follows from the unconstrained lower bound. Since \(m\ge2\),
\[ V=C\le\frac{2(m-1)}m\,C. \]

Suppose instead that \(a\notin S\). Every support ballot differs from \(a\) on at least one coordinate, so
\[ C=\sum_{t\in S}\mu_tH(a,t)\ge\sum_{t\in S}\mu_t=1. \]

The minimum support objective is at most its weighted average:
\[ V\le\sum_{t\in S}\mu_tD_\mu(t) =\sum_{t,u\in S}\mu_t\mu_uH(t,u). \]
For coordinate \(j\), disagreement occurs when exactly one of the two ballots differs from \(a_j\). Its contribution to this double sum is therefore
\(p_j(1-p_j)+(1-p_j)p_j=2p_j(1-p_j)\).
Thus
\[ V\le2\sum_{j=1}^mp_j(1-p_j) =2C-2\sum_{j=1}^mp_j^2. \]
Cauchy–Schwarz gives \(\sum_jp_j^2\ge C^2/m\). Using \(C\ge1\), we obtain
\[ V\le2C-\frac{2C^2}{m} \le2C-\frac{2C}{m} =\frac{2(m-1)}m\,C. \]

Both cases yield, for every \(b\in\mathrm{AVR}_\mu\),
\[ D_\mu(b)\le\frac{2(m-1)}m\,C \le\frac{2(m-1)}m\,\mathrm{OPT}_\mu. \]
The proof holds uniformly for every \(m\ge2\); fixing \(m\) is unnecessary.

5. Sharpness of the AVR constant

Take a tautological integrity constraint and support consisting of the \(m\) unit vectors \(e_1,\ldots,e_m\), each with mass \(1/m\). Every coordinate has marginal \(1/m\), so \(C=1\), and the feasible all-zero ballot attains \(\mathrm{OPT}_\mu=1\).

Distinct unit vectors have Hamming distance \(2\). Hence every support ballot has objective
\[ D_\mu(e_i)=\frac{2(m-1)}m. \]
All are AVR winners, proving that the fixed-dimension constant cannot be improved.

⟨structured verdict parsed — rendered above⟩

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

The output resolves the task correctly under the intended interpretation of “binary-rational” as rational numbers encoded in binary. Both winner-computation algorithms are polynomial, and both approximation arguments hold for every retained winner. I found no major or minor mathematical gaps.

The common-denominator construction is valid. Each \(v_t\) divides \(Q=\prod_{t\in S}v_t\), so \(w_t=u_t(Q/v_t)\) is a positive integer. Normalization gives
\[ \sum_{t\in S}w_t=Q\sum_{t\in S}\mu_t=Q. \]
In particular, \(w_t\le Q\).

The bit length of \(Q\) is bounded by the sum of the denominator bit lengths, hence is \(O(L)\). Intermediate products in its construction also have \(O(L)\) bits. The claimed \(O(\tau L^2)\) bound accommodates the products, exact divisions, and multiplications using schoolbook arithmetic.

Each \(N_j\) lies between \(0\) and \(Q\). The displayed integer AVR score correctly assigns contribution \(N_j\) when \(b_j=0\), and \(Q-N_j\) when \(b_j=1\). Its value is at most \(mQ\), giving the stated \(O(L+\log m)\) bit length.

Computing marginals and all support scores, comparing scores, and retaining ties fit within
\[ O\!\left(L+\tau L^2+m\tau(L+\log m)\right) \]
bit operations. Exact comparisons with \(Q\) correctly distinguish weak and strict majorities, including equality. Computing the two Hamming distances per support ballot correctly implements the specified MVR definition.

The algorithms operate on the supplied support rather than enumerating feasible ballots or expanding masses into an electorate. Feasibility follows from the input promise \(S\subseteq\operatorname{Mod}(IC)\); no optimization over models of \(IC\) is required. Outputting every winner also fits the bound.

Exchanging the two finite sums correctly yields
\[ D_\mu(x)=\sum_{j:x_j=0}q_j+\sum_{j:x_j=1}(1-q_j). \]
Minimizing each coordinate independently gives \(C\). Both specified majority ballots attain this coordinatewise minimum, even when some marginals equal \(\tfrac12\). The argument requires only that these two ballots attain the minimum; it does not mistakenly claim that they exhaust all unconstrained minimizers.

Therefore \(D_\mu(a)=C\) for each \(a\in\mathrm{Maj}_\mu\), and \(C\le\mathrm{OPT}_\mu\).

When \(C=0\), every marginal is either \(0\) or \(1\). Positivity of every support mass forces agreement on every coordinate. Since support types are distinct, the support then contains exactly one ballot. It is feasible and has zero cost. Thus the zero-cost case is correctly handled, and \(\mathrm{OPT}_\mu>0\) implies \(C>0\).

Fixing an arbitrary MVR winner \(b\) preserves the required universal quantifier over winners. A majority ballot \(a\) attaining its minimum distance exists because the majority set is finite and nonempty.

The MVR definition gives, for every \(t\in S\),
\[ r\le\min_{a'\in\mathrm{Maj}_\mu}H(t,a')\le H(t,a). \]
The triangle inequality consequently gives
\[ H(b,t)\le r+H(a,t)\le2H(a,t). \]
This comparison uses the same chosen \(a\) throughout and is valid even if another majority ballot is closer to \(t\).

For \(r>0\), omitting the exact zero contribution at \(t=b\) produces
\[ D_\mu(b)\le2C-2\mu_b r<2C\le2\mathrm{OPT}_\mu. \]
Strictness is justified precisely by \(\mu_b>0\) and \(r>0\).

For \(r=0\), \(b=a\), so \(D_\mu(b)=C\le\mathrm{OPT}_\mu\). If \(\mathrm{OPT}_\mu>0\), this is strictly below \(2\mathrm{OPT}_\mu\).

MVR winners exist because \(S\) is finite and nonempty. Every AVR winner minimizes \(D_\mu\) over that same support, so its cost is at most the cost of any MVR winner. The approximation guarantee therefore transfers to every AVR winner, with strictness preserved whenever required.

For either choice of majority ballot \(a\), the disagreement marginal satisfies
\[ p_j=\min\{q_j,1-q_j\}, \qquad \sum_jp_j=C. \]
This remains correct on tied coordinates.

If \(a\in S\), the unrestricted lower bound and selection of \(a\) give \(V=C\). Since \(m\ge2\), the factor \(\frac{2(m-1)}m\) is at least \(1\), validating this case.

If \(a\notin S\), every support ballot has integer Hamming distance at least \(1\) from \(a\). Averaging with normalized positive masses correctly gives \(C\ge1\).

The minimum support cost is at most its weighted average. Expanding that average into the double sum is valid, including its diagonal terms. The coordinate contribution is exactly \(2p_j(1-p_j)\), hence
\[ V\le2C-2\sum_jp_j^2. \]
The stated Cauchy–Schwarz inequality \(\sum_jp_j^2\ge C^2/m\) applies to these \(m\) real numbers. Since \(C\ge1\), replacing \(C^2\) by \(C\) in the subtracted term has the correct inequality direction.

Both cases establish
\[ D_\mu(b)\le\frac{2(m-1)}m\,C \le\frac{2(m-1)}m\,\mathrm{OPT}_\mu \]
for every AVR winner. The argument also covers \(m=2\), where the factor equals \(1\), and does not require treating \(m\) as fixed.

The unit-vector support contains \(m\) distinct feasible ballots with positive rational masses summing to \(1\). Each marginal is \(1/m\), so \(C=1\) for every \(m\ge2\). The feasible zero ballot has cost \(1\), establishing \(\mathrm{OPT}_\mu=1\).

Each unit vector has distance \(2\) from every other unit vector and distance \(0\) from itself. Its cost is therefore exactly \(\frac{2(m-1)}m\), and all support ballots are AVR winners.

For \(m=2\), the marginals are tied, but the calculation remains valid. Thus sharpness is established in the binary-encoded rational model.

No repair or additional mathematical clarification is needed. The polynomial-time claim concerns computing these support-based rules; the output does not claim a polynomial-time algorithm for computing \(\mathrm{OPT}_\mu\).

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