Answer: \(\Sigma_2^p\)-complete for decision and \(\mathrm{F}\Sigma_2^p\)-complete for search; hardness holds with \(\Gamma=\top\), \(u=0\), and \(\tau=8\) equally weighted types.
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateWinDet(RA) is Σp 2-complete and FWinDet(RA) is FΣp 2-complete. We would like to point out that the complexity result for WinDet(Kemeny) has been shown before [13]. We give an alternative proof of hardness for this problem. We prove hardness by giving a reduction directly from a canon- ical complete problem for PNP[log], which allows us to ex- tend this hardness result to the case of the search prob- lem FWinDet(Kemeny), which would not have been at all straightforward with the known PNP[log]-hardness proof for WinDet(Kemeny) from the literature.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given an agenda \(\Phi\), integrity constraint \(\Gamma\), a support list of complete \(\Gamma\)-consistent judgment types \(t\) with positive binary-rational masses \(\mu_t\) summing to \(1\), and constraints \(L_0,\ldots,L_u\), define each formula’s strength as \(M_\mu(\varphi)=\sum_{t:\,\varphi\in t}\mu_t\). Order the formulas by nonincreasing strength, allowing any order among ties, and scan that order, adding each formula exactly when the resulting judgment set remains \(\Gamma\)-consistent. Does some permitted ordering produce a winner \(J^\star\) with \(L_0\subseteq J^\star\) and \(L_i\not\subseteq J^\star\) for every \(i>0\)? The search version outputs such a winner and a witnessing order, if one exists.
An agenda \(\Phi\) is a finite nonempty set of propositional formulas, closed under complementation and containing no doubly negated formulas; write \(|\Phi|=2m\). Complementation removes an outer negation when present and otherwise adds one. The integrity constraint \(\Gamma\) is an arbitrary propositional formula. A set \(J\subseteq\Phi\) is \(\Gamma\)-consistent when \(\Gamma\land\bigwedge_{\varphi\in J}\varphi\) is satisfiable, and complete when it contains exactly one formula from each complementary pair.
A society is given by its support: the list of the \(\tau\) distinct complete, \(\Gamma\)-consistent types \(t\subseteq\Phi\) with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Formulas are explicitly encoded propositional expressions; let \(L\) be the total input bit length. State running times in \(m,\tau,L,u\).
The input also contains explicitly listed sets \(L_0,\ldots,L_u\subseteq\Phi\), with \(u\geq0\); empty sets are allowed. Define \(M_\mu(\varphi)=\sum_{t:\varphi\in t}\mu_t\). A permitted order lists every formula of \(\Phi\) by nonincreasing strength, with arbitrary ordering within ties.
Starting from \(J=\varnothing\), scan a permitted order and add each formula exactly when its addition preserves \(\Gamma\)-consistency. The final set is a winner. The decision problem asks whether some permitted order yields \(J^\star\) with \(L_0\subseteq J^\star\) and \(L_i\not\subseteq J^\star\) for every \(1\leq i\leq u\). The search version outputs such a winner and a witnessing order, if they exist.
Is this continuous Ranked-Agenda winner-existence problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
For explicitly listed finite profiles, Ranked-Agenda winner existence is \(\Sigma_2^p\)-complete, even with \(\Gamma=\top\) and \(u=0\); producing a qualifying winner is \(\mathrm{F}\Sigma_2^p\)-complete. [Endriss and de Haan](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p117.pdf)
No result settling exactly the support-encoded rational-mass formulation was identified in the literature search.
1. Result
The decision problem is \(\Sigma_2^p\)-complete, and hence \(\mathrm{NP}\)-hard. Hardness holds even when \(\Gamma=\top\), \(u=0\), and the support consists of exactly eight distinct types, each with mass \(1/8\).
The search problem, including output of a witnessing order, is \(\mathrm{F}\Sigma_2^p\)-complete under polynomial-time Levin reductions, using the search-class convention of [Endriss and de Haan, Section 2.3](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p117.pdf).
Thus the conclusion also holds if “binary-rational” is interpreted restrictively as requiring dyadic masses.
2. Exact strength computation and membership
Write each input mass as \(\mu_t=a_t/b_t\), with positive integers encoded in binary. Set
\(\displaystyle D=\prod_t b_t,\qquad w_t=a_t(D/b_t),\qquad s_\varphi=\sum_{t:\varphi\in t}w_t.\)
Then \(M_\mu(\varphi)=s_\varphi/D\). Consequently, strength comparisons and ties can be computed exactly by comparing integers.
Because the total encoding length of the denominators is at most \(L\), the bit length of \(D\) is \(O(L)\). Moreover, \(\sum_t w_t=D\), so every strength numerator also has \(O(L)\) bits. Ordinary integer arithmetic therefore gives polynomial-time preprocessing. A generous bound, including sorting strengths and preparing membership tables, is
\(\displaystyle P(m,\tau,L,u)=O\!\left((m\tau+m\log(m+1)+(u+1)m+1)L^2\right).\)
A nondeterministic algorithm now guesses a permutation \((\varphi_1,\ldots,\varphi_{2m})\), verifies that its strengths are nonincreasing, and simulates the prescribed scan. At step \(k\), it queries a satisfiability oracle on
\(\displaystyle \Gamma\land\bigwedge_{\varphi\in J_{k-1}}\varphi\land\varphi_k.\)
It adds \(\varphi_k\) precisely when the answer is yes. Finally, it checks the listed containment requirements.
There are at most \(2m\) satisfiability queries, each of length \(O(L)\), and the work outside the oracle is bounded by \(P(m,\tau,L,u)\). Thus decision belongs to \(\mathrm{NP}^{\mathrm{NP}}=\Sigma_2^p\). Returning the computed set and guessed order gives membership of search in \(\mathrm{F}\Sigma_2^p\).
For completeness, every such scan produces a complete, consistent judgment set. Consistency is maintained at every step. For any complementary pair, consider whichever member is scanned first. If it is accepted, consistency prevents acceptance of its complement. If it is rejected, the current consistent conjunction entails its complement. Every later accepted conjunction still entails that complement, so the complement is accepted when scanned. Hence exactly one member of every pair is selected.
3. A reduction with eight equally weighted types
We reduce from the standard \(\Sigma_2^p\)-complete quantified satisfiability problem
\(\displaystyle \exists X\,\forall Y\,\psi(X,Y),\)
where \(X=\{x_1,\ldots,x_v\}\), \(X\) and \(Y\) are disjoint, and \(\psi\) is an explicitly encoded propositional formula. Its corresponding assignment-search problem is \(\mathrm{F}\Sigma_2^p\)-complete; these source problems are also stated in [Endriss and de Haan, Section 2.3](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p117.pdf).
Introduce fresh variables \(y_1,\ldots,y_8,q\), and fresh variables \(a_i,b_i\) for each \(i\). Define
\(\displaystyle E=\bigvee_{j=1}^{8}y_j,\)
\(\displaystyle C=\bigwedge_{i=1}^{v}\bigl((a_i\leftrightarrow x_i)\land(b_i\leftrightarrow\neg x_i)\bigr),\)
\(\displaystyle B=(\neg y_1\land\neg y_2\land\neg y_3)\land(E\lor\neg\psi),\)
and the agenda formula
\(\displaystyle H=(E\lor C)\land(q\leftrightarrow B).\)
All abbreviations can be expanded into explicit propositional expressions with polynomial growth in size.
Take the agenda consisting of the formulas
\(\displaystyle H,\ q,\ y_1,\ldots,y_8,\ a_1,b_1,\ldots,a_v,b_v\)
and their complements. Set \(\Gamma=\top\), \(u=0\), and \(L_0=\{\neg q\}\). There are \(m=2v+10\) complementary pairs.
For each \(j\in\{1,\ldots,8\}\), define a complete type \(t_j\) by the following choices:
Give each type mass \(1/8\).
These eight types are distinct because their choices on the \(y_j\) differ. Each is consistent: \(E\) is true, so \(E\lor C\) is true regardless of the choices on \(X,Y,a_i,b_i\). Also, under its one-hot choice of the \(y_j\), the formula \(B\) is false exactly for \(j\in\{1,2,3\}\). Thus its stipulated value of \(q\) satisfies \(q\leftrightarrow B\), and therefore satisfies \(H\).
Their strengths are:
| Formula | Strength |
|---|---|
| \(H\) | \(1\) |
| Each \(\neg y_j\) | \(7/8\) |
| Each \(a_i,b_i\) | \(6/8\) |
| \(q\) | \(5/8\) |
| \(\neg q\) | \(3/8\) |
| Each \(\neg a_i,\neg b_i\) | \(2/8\) |
| Each \(y_j\) | \(1/8\) |
| \(\neg H\) | \(0\) |
The construction has polynomial encoding length and requires no satisfiability computation.
4. Verification of the reduction
We analyze every permitted order.
First, \(H\) is scanned and accepted: it is satisfiable, as witnessed by any support type.
Next, all eight formulas \(\neg y_j\) are scanned and accepted. To justify every acceptance, the conjunction
\(\displaystyle H\land\bigwedge_{j=1}^{8}\neg y_j\)
is satisfiable. Indeed, choose arbitrary assignments to \(X,Y\), set \(a_i=x_i\) and \(b_i=\neg x_i\), and set \(q\) to the truth value of \(\neg\psi\). This satisfies \(C\), makes \(E\) false, and satisfies \(q\leftrightarrow B\). The same assignment witnesses consistency for every prefix of the eight negative \(y_j\)-formulas.
After this block, the accepted conjunction entails
\(\displaystyle C\land(q\leftrightarrow\neg\psi).\)
Now all the positive formulas \(a_i,b_i\) are scanned, in an arbitrary order within their common strength.
For each \(i\), the first of \(a_i,b_i\) encountered is accepted. Previously accepted formulas from this block impose only choices on other existential variables, and these choices can be extended by setting \(x_i\) appropriately. Choose the remaining variables arbitrarily and set \(q=\neg\psi\) to satisfy \(H\).
The second member of the pair is rejected, because \(C\) entails that exactly one of \(a_i,b_i\) is true.
Consequently, this block determines an assignment \(\alpha\) to \(X\), with
\(\displaystyle \alpha(x_i)=1\quad\text{if and only if }a_i\text{ was accepted}.\)
Conversely, every assignment \(\alpha\) can be obtained: place all of its selected formulas—\(a_i\) when \(\alpha(x_i)=1\), and \(b_i\) otherwise—before the other formulas in this tied block.
The next formula is \(q\). Its addition is consistent exactly when
\(\displaystyle \exists Y\,\neg\psi(\alpha,Y)\)
holds. One direction follows because the accepted conjunction forces \(X=\alpha\), all \(y_j\) false, and \(q\leftrightarrow\neg\psi\). For the reverse direction, a satisfying assignment to \(\neg\psi(\alpha,Y)\), together with the stipulated values of the auxiliary variables and \(q=1\), satisfies the entire proposed conjunction.
It follows that \(q\) is rejected exactly when
\(\displaystyle \forall Y\,\psi(\alpha,Y)\)
holds. The formula \(\neg q\), scanned next, is accepted exactly in this case: if \(q\) was accepted, its complement is inconsistent; if \(q\) was rejected, the current consistent conjunction entails \(\neg q\).
Therefore,
\(\displaystyle \exists\text{ permitted order with }\neg q\in J^\star \quad\Longleftrightarrow\quad \exists X\,\forall Y\,\psi(X,Y). \)
This is a polynomial-time many-one reduction establishing \(\Sigma_2^p\)-hardness under all the restrictions claimed above.
For search, extract \(\alpha\) from any qualifying output by setting \(\alpha(x_i)=1\) exactly when \(a_i\in J^\star\). The argument proves that this assignment satisfies \(\forall Y\,\psi(\alpha,Y)\). Extraction is polynomial-time and works for every qualifying output, including outputs carrying a witnessing order. Hence the same construction is a polynomial-time Levin reduction establishing search hardness.
Together with membership, both completeness claims follow.
5. Running times and the finite-profile connection
For a fixed permitted order, the winner can be computed with at most \(2m\) satisfiability queries and polynomial additional work bounded by \(P(m,\tau,L,u)\).
An unconditional deterministic decision-and-search algorithm enumerates all permutations, retains the permitted ones, and simulates them. Since at most \(L\) propositional variables occur, exhaustive satisfiability checking gives the bound
\(\displaystyle O\!\left( P(m,\tau,L,u) +(2m)!\bigl[m\,2^L L+(u+1)m\bigr] \right). \)
It outputs a qualifying winner and its order upon finding one, or reports nonexistence after exhausting the orders.
Under the usual numerator-and-denominator encoding of rationals, the cited finite-profile hardness also transfers immediately: replace each distinct type occurring \(c_t\) times in a profile of length \(n\) by mass \(c_t/n\). Every strength becomes its old count divided by \(n\), preserving all strict comparisons, ties, permitted orders, and winners. This compression has polynomial size because the source profile is explicitly listed. The eight-type construction above additionally proves hardness for dyadic masses and constant support size.
Thus a polynomial-time algorithm for the general problem would imply \(\mathrm{P}=\mathrm{NP}\).
⟨structured verdict parsed — rendered above⟩
The output resolves the task. The decision proof establishes \(\Sigma_2^p\)-completeness, including hardness with exactly eight equally weighted support types. The search completeness claim is also justified under the explicitly cited convention. I found no major or minor mathematical issues requiring repair.
The common-denominator construction is correct: each \(b_t\) divides \(D\), and \(w_t=a_t(D/b_t)\) is an integer. Consequently, \(M_\mu(\varphi)=s_\varphi/D\), so integer comparisons preserve both strict strength comparisons and ties.
The bit-length bounds are valid. The bit length of \(D\) is at most the sum of the denominator bit lengths, up to a constant. Positivity and normalization give \(\sum_t w_t=D\), hence \(0\leq s_\varphi\leq D\). All integers used therefore have \(O(L)\) bits.
The stated preprocessing bound \(P(m,\tau,L,u)\) is sufficiently generous for ordinary integer arithmetic, membership tables, strength comparisons, sorting, and preparation of the listed containment conditions. It does not assume that the number of possible consistent types is small.
Guessing a permutation of all \(2m\) agenda formulas supplies a polynomial-length certificate for the order. Checking that it is a permutation and that strengths are nonincreasing is polynomial.
Each consistency query is exactly the query required by the prescribed scan. Its length is \(O(L)\), because the accepted formulas form a subset of the explicitly encoded agenda. There are at most \(2m\) queries.
Checking \(L_0\subseteq J^\star\) and \(L_i\not\subseteq J^\star\) for all \(1\leq i\leq u\) is polynomial. Thus the described algorithm correctly establishes membership in \(\mathrm{NP}^{\mathrm{NP}}=\Sigma_2^p\).
Initial consistency is justified by the input assumptions: positive masses summing to one imply nonempty support, and every support type is \(\Gamma\)-consistent. Therefore \(\Gamma\) is satisfiable.
Accepted additions preserve consistency by definition. For a complementary pair, acceptance of the first member prevents acceptance of the second. If the first member is rejected, the current consistent conjunction entails its complement. Subsequent accepted additions preserve that entailment and consistency, so the complement is accepted when encountered.
This proves exactly one accepted formula per complementary pair. There is no missing assumption about satisfiability of individual agenda formulas.
The cited source states that quantified satisfiability with a quantifier-free matrix \(\exists X\,\forall Y\,\psi\) is \(\Sigma_2^p\)-complete. It also states completeness of the corresponding assignment-search problem for \(\mathrm{F}\Sigma_2^p\), defines that class using nondeterministic polynomial-time machines with witness \(\mathrm{FNP}\) oracles, and gives the stated definition of polynomial-time Levin reductions. These references match the prover’s applications. [Endriss and de Haan, Section 2.3](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p117.pdf)
The search membership argument fits that convention: a witness satisfiability oracle supplies the yes/no information needed for the scan, and its additional witness can be ignored. Each accepting branch outputs a qualifying winner together with its guessed permitted order.
The agenda has one pair for \(H\), one for \(q\), eight for the auxiliary \(y_j\), and two for each existential variable. Thus \(m=2v+10\) is correct.
Freshness prevents auxiliary variables from colliding with source variables. The displayed positive agenda formulas and their complements form the required complementary pairs. Expanding the abbreviations causes only polynomial growth: the construction uses a constant number of copies of \(E\), \(C\), and \(\psi\).
The settings \(\Gamma=\top\), \(u=0\), and \(L_0=\{\neg q\}\) satisfy the task’s restrictions.
Each listed type makes exactly one \(y_j\) true, so the eight types are distinct and \(E\) is true in each.
Under these assignments, \(B\) is false for \(j\in\{1,2,3\}\) and true for \(j\in\{4,\ldots,8\}\). The stipulated values of \(q\) therefore satisfy \(q\leftrightarrow B\). Since \(E\lor C\) is already true, every type satisfies \(H\), independently of \(\psi\).
Every type specifies one member of each agenda pair and has a satisfying extension. Its completeness and consistency are therefore established.
All strength entries are correct:
The masses are positive, sum to one, and are dyadic.
The distinct strength levels force \(H\) first, then all eight \(\neg y_j\), then the positive \(a_i,b_i\) block.
Acceptance of \(H\) follows from the established support consistency. The prover supplies a simultaneous satisfying assignment for \(H\) and all eight negative auxiliary literals. This also witnesses consistency for every prefix, irrespective of their tied order.
After these acceptances, \(E\) is false. Substitution into \(H\) yields precisely \(C\land(q\leftrightarrow\neg\psi)\), as claimed.
Before either \(a_i\) or \(b_i\) has been accepted, earlier acceptances in this block constrain only other existential coordinates through \(C\). The prover’s extension argument therefore justifies accepting whichever of \(a_i,b_i\) is encountered first.
Once that member is accepted, \(C\) makes the second inconsistent. Thus exactly one positive member is accepted for every index, determining the claimed assignment \(\alpha\).
Conversely, placing all formulas selected by a prescribed \(\alpha\) before the other formulas respects the common strength and yields that assignment. Both the universal analysis of permitted orders and realization of every existential assignment are justified.
When \(q\) is scanned, the accepted conjunction fixes \(X=\alpha\), makes every auxiliary \(y_j\) false, and imposes \(q\leftrightarrow\neg\psi\). Therefore accepting \(q\) is consistent exactly when \(\exists Y\,\neg\psi(\alpha,Y)\).
Both directions are explicitly justified in the output. Rejecting \(q\) is consequently equivalent to \(\forall Y\,\psi(\alpha,Y)\).
The next formula is \(\neg q\). It is rejected if \(q\) was accepted and accepted if \(q\) was rejected. Subsequent steps cannot remove an accepted formula. Hence the claimed equivalence between qualifying winner existence and source quantified satisfiability follows.
This is a valid polynomial-time many-one reduction establishing the stated restricted hardness.
The instance map preserves existence in both directions. From every qualifying winner, the proposed extraction reads the accepted \(a_i\) formulas and returns the assignment determined by the positive block.
The preceding analysis ensures that this assignment satisfies \(\forall Y\,\psi(\alpha,Y)\). Extraction is polynomial and works for every qualifying output, regardless of its witnessing order. These are exactly the required Levin-reduction conditions.
The fixed-order bound correctly uses at most \(2m\) satisfiability queries with polynomial additional work.
The unconditional enumeration bound is valid: there are at most \((2m)!\) orders, at most \(L\) occurring variables, and each exhaustive satisfiability test takes \(O(2^L L)\) time. The displayed bound also accommodates order checking and containment tests.
The finite-profile compression preserves all strengths up to the same positive scaling factor. Its encoding size is polynomial in the explicitly listed source profile. The separate eight-type construction establishes the dyadic restriction without relying on that compression.
Empty forbidden sets are correctly handled by the final containment checks: any such set makes qualification impossible. Empty \(L_0\), \(u=0\), and empty quantifier blocks cause no failure. For an empty existential block, \(C\) has the conventional empty-conjunction value \(\top\), and the same analysis applies.
No additional lemma or clarification is needed to verify the claimed result. NP-hardness does not unconditionally exclude membership in \(\mathrm{P}\); the output correctly states the consequence that a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{NP}\).
⟨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.