← back to the atlas

d4-conf-wine-2015-0011 (d4-conf-wine-2015-0011)

Answer: \(\mathrm{NP}\text{-hard}\), even with no parents per issue; polynomial-time winner determination would imply \(\mathrm{P}=\mathrm{NP}\).

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateIt is \NP-hard to determine the winner of a given profile when using the voting rule One-Step-$k$-Approval with arbitrary $k$ of polynomial size in $n$ and $m$ (i.e., exponential value).

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

The continuous mirror question, as graded

Given \(m\) binary issues, a binary-encoded approval size \(k\), and a support of \(\tau\) compact acyclic CP-net types with issue-order information and rational masses \(\mu_t\) summing to \(1\), find a candidate maximizing the total mass of types that rank it among their top \(k\) candidates.

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

Given \(m\geq 1\) binary issues, the candidates are all assignments in \(\{0,1\}^m\). Each type supplies an acyclic CP-net with explicit conditional preference tables giving strict preferences, at most \(d\) parents per issue for a fixed constant \(d\), and a strict issue order placing every parent before its children; different types may use different orders.
The induced candidate ranking is lexicographic: compare two assignments at their first differing issue in that type's order, using the conditional preference for their common parent assignment. Let \(r_t(c)\) denote the position of \(c\), starting at \(1\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total input bit length.
Given a binary-encoded integer \(1\leq k\leq 2^m\), find any candidate maximizing \(s(c)=\sum_{t:r_t(c)\leq k}\mu_t\); any maximizer is acceptable when scores tie.

Is this mass-based winner determination problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finite unweighted profiles with individual issue orders, winner determination under One-Step-\(k\)-Approval is NP-hard when \(k\) is binary encoded; polynomial-time cases include polynomially bounded \(k\), and power-of-two \(k\) with a common compatible issue order ([Dorn, Krüger and Scharpfenecker](https://arxiv.org/pdf/1509.08628)). No result explicitly treating the normalized rational-support formulation was located.

Modeling choices made when packaging the task

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

Result

The problem is \(\mathrm{NP}\)-hard, even when every issue has no parents. Normalizing voter counts into rational masses does not remove the hardness, and allowing any tied maximizer does not help.

The following gives a self-contained reduction, making explicit the normalization and parent bound in the construction underlying [Dorn, Krüger and Scharpfenecker, Theorem 1](https://arxiv.org/pdf/1509.08628).

1. Construction from satisfiability

Use the standard \(\mathrm{NP}\)-complete restriction of \(\mathrm{3SAT}\) in which every clause contains exactly three distinct variables. Let the input formula be \(\varphi=C_1\land\cdots\land C_q\), on variables \(x_1,\ldots,x_m\), with \(q\geq1\) and \(m\geq3\). Delete duplicate clauses; this preserves satisfiability.

Create one binary issue \(X_i\) for each variable \(x_i\). Interpret a candidate \(c\in\{0,1\}^m\) as the truth assignment \(x_i=c_i\).

For each clause \(C_a\), construct a type \(t_a\) as follows:

All dependency graphs are empty. Consequently, every CP-net is acyclic, every table consists of one strict preference, and every issue order is compatible. The construction satisfies any nonnegative parent bound \(d\).

Give each type mass \(\mu_{t_a}=1/q\), and set \(k=7\cdot2^{m-3}\).

The types are distinct. Indeed, different sets of clause variables give different first-three-issue sets; for the same variable set, different clauses give different preferences on at least one of those issues. Thus the support size is \(\tau=q\).

2. Each type approves exactly its clause’s satisfying assignments

Fix a clause \(C_a\) and its type \(t_a\).

Because its preferences are unconditional, the lexicographic ranking partitions all candidates into eight consecutive blocks according to their assignments on the first three issues. Each block contains exactly \(2^{m-3}\) candidates: the remaining issues can take every possible assignment.

The last block assigns each of the first three issues its less-preferred value. To verify this, compare that triple with any other triple. At their first differing issue, the other triple uses the preferred value and therefore ranks ahead of it.

By construction, this last triple makes all three literals of \(C_a\) false. It is the unique falsifying assignment on those three variables.

The first \(k=7\cdot2^{m-3}\) positions are precisely the other seven blocks. Hence, for every candidate \(c\),

\(\displaystyle r_{t_a}(c)\leq k\quad\Longleftrightarrow\quad c\models C_a.\)

It follows that

\(\displaystyle s(c)=\frac{|\{a:c\models C_a\}|}{q}.\)

In particular,

\(\displaystyle \max_{c\in\{0,1\}^m}s(c)=1\quad\Longleftrightarrow\quad\varphi\text{ is satisfiable}.\)

3. Polynomial size and arbitrary tie-breaking

Each type contains an order of \(m\) issue indices and \(m\) constant-size preference tables. Its encoding therefore uses \(O(m\log m)\) bits. Each mass \(1/q\) has an \(O(\log q)\)-bit numerator-and-denominator encoding.

The binary representation of \(k=7\cdot2^{m-3}\) is the string \(111\) followed by \(m-3\) zeros, so it has exactly \(m\) bits. Also, \(1\leq k\leq2^m\). The complete construction has polynomial bit length and can be produced in polynomial time.

Suppose a polynomial-time algorithm returned any maximizing candidate \(c^\star\). Run it on the constructed society and test whether \(c^\star\models\varphi\).

If \(\varphi\) is satisfiable, the maximum score is \(1\), so every maximizer satisfies every clause. If \(\varphi\) is unsatisfiable, no returned candidate can satisfy every clause. This decides \(\mathrm{3SAT}\) in polynomial time.

Thus finding any maximizer is \(\mathrm{NP}\)-hard in the optimization/search sense: a polynomial-time winner algorithm would imply \(\mathrm P=\mathrm{NP}\).

If “binary rational” is intended to mean a rational with a finite binary expansion, the reduction still works. Let \(Q\) be the smallest power of two with \(Q\geq q\). Give the first type mass \((Q-q+1)/Q\) and every other type mass \(1/Q\). These masses are positive, sum to \(1\), and have polynomial-size binary expansions. Since every mass is positive, score \(1\) still holds exactly when every clause is satisfied.

4. Verification of scores

For completeness, a candidate’s score is polynomial-time computable even for the general conditional model.

Write a type’s order as \(X_{i_1},\ldots,X_{i_m}\). Define \(b_j(c)=0\) when \(c_{i_j}\) is the preferred value under the parent assignment supplied by \(c\), and \(b_j(c)=1\) otherwise. Then

\(\displaystyle r_t(c)=1+\sum_{j=1}^{m}b_j(c)\,2^{m-j}.\)

To justify the formula, the map \(c\mapsto(b_1(c),\ldots,b_m(c))\) is a bijection: reconstruct \(c\) in issue order, using the already assigned parents to choose the preferred or less-preferred value indicated by each bit. For two candidates, all preferences before their first differing issue are evaluated under identical parent assignments. At that first difference, the preferred candidate has bit \(0\), and the other has bit \(1\). Their ranking therefore agrees with the numerical order of their bit strings.

Table lookups and arithmetic on these \(m\)-bit ranks are polynomial-time operations. Exact addition of the rational masses is also polynomial-time: a common denominator obtained by multiplying their denominators has bit length bounded by the total input bit length.

Consequently, the associated decision problem asking whether some candidate has score at least a given rational threshold is in \(\mathrm{NP}\). The reduction above proves hardness already at threshold \(1\), so this decision problem is \(\mathrm{NP}\)-complete.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The output resolves the task: finding any maximizing candidate is \(\mathrm{NP}\)-hard, even with empty dependency graphs. The reduction handles rational normalization, distinct support types, binary encoding of \(k\), and arbitrary tie-breaking correctly.

The argument is sound in substance. I found one minor bit-length imprecision and no blocking issues.

Step-by-step verification

1. Starting problem

The prover invokes satisfiability for formulas whose clauses contain exactly three distinct variables. This is a valid \(\mathrm{NP}\)-complete starting problem. A primary source establishes hardness even under further restrictions, including unique clauses: [Monotone 3-Sat-(2,2) is NP-complete](https://arxiv.org/abs/1912.08032).

The assumptions \(q\geq1\) and \(m\geq3\) are consistent with that starting problem. Removing duplicate clauses preserves satisfiability and does not remove every clause from a nonempty formula.

The cited [Dorn–Krüger–Scharpfenecker Theorem 1](https://arxiv.org/pdf/1509.08628) uses the same clause-based construction and approval cutoff. The submitted argument supplies its own justification, so its correctness does not depend on importing that theorem’s proof.

2. Construction and admissibility

Every constructed type has an empty dependency graph and one unconditional strict preference per issue. Thus:

The claim that the types are distinct is correct. Different clause-variable sets produce different first-three-issue sets. For an identical variable set, distinct clauses differ in a literal’s sign and hence in an unconditional preference. After duplicate deletion, \(\tau=q\).

3. Approval sets

The eight-block argument is correct. Fixing the first three issue values defines a block of exactly \(2^{m-3}\) candidates. All members of one block precede or follow all members of another because their comparison is determined within the first three issues.

The triple containing three less-preferred values is last: against any different triple, its value at the first differing issue is less preferred. By construction, that triple falsifies all three literals. The distinct-variable assumption ensures that it is the unique falsifying triple.

Consequently, the first \(7\cdot2^{m-3}\) candidates are exactly the assignments satisfying the clause. The equivalence
\(r_{t_a}(c)\leq k\Longleftrightarrow c\models C_a\)
is established without an off-by-one error.

This remains valid at the boundary \(m=3\): each block then contains one candidate and \(k=7\).

4. Scores and normalization

With masses \(1/q\), the stated score formula is correct:
\(s(c)=|\{a:c\models C_a\}|/q\).

Therefore, maximum score \(1\) is equivalent to satisfiability.

The alternative construction for finite binary expansions also works. For the stated power of two \(Q\), every mass is positive, and their numerators sum to
\((Q-q+1)+(q-1)=Q\).
Their encodings have polynomial length. Although this changes relative clause weights, the proof only needs score \(1\) to mean that every clause is satisfied; positivity guarantees exactly that. The case \(q=1\) is covered.

5. Encoding size

The constructed orders and unconditional tables have the claimed polynomial encoding size. The rational masses also have polynomial-size encodings.

The representation of \(k\) is correctly identified as three initial ones followed by \(m-3\) zeros, giving exactly \(m\) bits. Its range satisfies \(1\leq k<2^m\).

Thus the construction runs in polynomial time and produces an instance polynomial in the source formula’s size.

6. Search hardness and ties

The proposed use of a winner algorithm is correct. On a satisfiable formula, every maximizing candidate has score \(1\), so every possible returned maximizer satisfies the formula. On an unsatisfiable formula, no candidate satisfies it.

Testing the returned assignment against the formula takes polynomial time. Hence a polynomial-time algorithm returning any maximizer would decide the stated \(\mathrm{NP}\)-complete satisfiability problem in polynomial time.

The prover appropriately identifies this as optimization/search hardness; it does not require a particular tie-breaking rule.

7. General rank computation and decision membership

The conditional-model rank formula is correct. Compatibility of the issue order guarantees that every parent value is available during reconstruction, establishing the asserted bijection.

For two candidates, their common prefix gives identical parent assignments at their first differing issue. Their transformed bits agree before that issue and differ there according to the conditional preference. Therefore numerical ordering of the transformed bit strings agrees with the specified candidate ranking.

Exact rational score computation is polynomial-time. The product of input denominators has bit length bounded by the aggregate denominator encoding length, so the proposed common-denominator computation does not require exponentially many bits.

The decision problem has an \(m\)-bit candidate certificate, polynomial-time verification, and hardness at threshold \(1\). Its claimed \(\mathrm{NP}\)-completeness follows.

Minor issue: Section 4 calls the ranks “\(m\)-bit ranks.” The transformed value \(r_t(c)-1\) uses at most \(m\) bits, but the rank \(r_t(c)=2^m\) requires \(m+1\) bits. This does not affect polynomial-time computability.

Minimum clarification: Replace “these \(m\)-bit ranks” with “these ranks of at most \(m+1\) bits.”

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