Answer: \(\mathrm{NP}\)-hard (indeed \(\Theta_2^p\)-hard)
Proposition 3.1 — class: other
Let (¨, Γin, Γout, P) be a given judgment aggre- gation framework. For each R∈{Kemeny, Slater, MaxHamming, Young, Dodgson}, we have that J∈R(P) if and only if there is an optimal solution τto the MaxSAT instance FR(P) with τ∩¨ = J.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given an agenda \(\mathcal{A}\), constraints \(\Gamma_{\rm in},\Gamma_{\rm out}\), required literals \(L\), and rational masses \(\mu_t\) over finitely many complete \(\Gamma_{\rm in}\)-consistent judgment types \(t\), decide whether some \(J\in J(\mathcal{A},\Gamma_{\rm out})\) with \(L\subseteq J\) minimizes \(D_\mu(J)=\sum_t\mu_t H(J,t)\) among all output-feasible collective judgments.
Let \(A=\{x_1,\ldots,x_m,\neg x_1,\ldots,\neg x_m\}\). A complete \(\Gamma\)-consistent judgment set chooses exactly one literal for every \(x_i\) and, together with \(\Gamma\), is satisfiable. The input gives formulas \(\Gamma_{in},\Gamma_{out}\), types \(T_1,\ldots,T_q\) that are complete \(\Gamma_{in}\)-consistent judgment sets, rational masses \(\mu_t\ge0\) with \(\sum_t\mu_t=1\), and \(L\subseteq A\). For a complete \(\Gamma_{out}\)-consistent \(J\), let \(C(J)=\sum_t\mu_t H(J,T_t)\), where \(H\) is Hamming distance.
Is rational-mass Kemeny outcome determination—whether some \(C\)-minimizing \(\Gamma_{out}\)-consistent \(J\) contains \(L\)—solvable in polynomial time, or is it NP-hard?
For finite profiles, Kemeny collective judgments are exactly the agenda restrictions of optimal solutions of a weighted MaxSAT encoding.
For finite profiles, Kemeny outcome determination is \(\Theta^p_2\)-complete.
Rational-mass Kemeny outcome determination is NP-hard. In fact, under the stated finite-profile result, it is $\Theta_2^p$-hard. This remains true even with one judgment type of mass $1$, $\Gamma_{in}=\top$, and a singleton set $L$.
Unless $P=NP$, the problem is therefore not polynomial-time solvable.
Let $\varphi(u_1,\ldots,u_n)$ be a SAT instance, where we may assume $n\geq 1$. Introduce fresh variables $y,z_1,\ldots,z_n$. The agenda contains all literals over
$$ u_1,\ldots,u_n,y,z_1,\ldots,z_n. $$
Set
$$ \Gamma_{in}=\top $$
and
$$ \Gamma_{out} = (y\rightarrow\varphi) \wedge \bigwedge_{j=1}^n(z_j\leftrightarrow y). $$
There is one type, of mass $1$:
$$ T= \{\neg u_1,\ldots,\neg u_n,y,z_1,\ldots,z_n\}. $$
Finally, let
$$ L=\{y\}. $$
The type $T$ is complete and $\Gamma_{in}$-consistent, and the construction has size polynomial in $|\varphi|$.
Let $a$ be a satisfying assignment of $\varphi$. Extend it by setting
$$ y=z_1=\cdots=z_n=1. $$
The resulting judgment set $J_a$ satisfies $\Gamma_{out}$. It disagrees with $T$ only on those variables $u_i$ that are true under $a$. Consequently,
$$ C(J_a)=H(J_a,T)\leq n. $$
Now consider any $\Gamma_{out}$-consistent judgment set $J$ with $\neg y\in J$. The equivalences in $\Gamma_{out}$ force
$$ \neg z_1,\ldots,\neg z_n\in J. $$
Thus $J$ disagrees with $T$ on $y,z_1,\ldots,z_n$, giving
$$ C(J)=H(J,T)\geq n+1. $$
Therefore no minimizing judgment set can contain $\neg y$. Every minimizing judgment set contains $y$, and in particular some minimizing judgment set contains $L$.
If a $\Gamma_{out}$-consistent judgment set contained $y$, then $y\rightarrow\varphi$ would force $\varphi$ to be true, which is impossible. Hence every feasible judgment set contains $\neg y$.
Feasible judgment sets nevertheless exist: set every $u_i,y,z_j$ to false. Therefore a minimum exists, but no minimizing judgment set contains $L$.
We have proved
$$ \varphi\text{ is satisfiable} \quad\Longleftrightarrow\quad \text{some minimizing judgment set contains }L. $$
This is a polynomial-time many-one reduction from SAT, proving NP-hardness. If Hamming distance is defined using symmetric difference of literal sets, all displayed costs are multiplied by $2$, and the strict comparison is unchanged.
The stated finite-profile result yields the stronger $\Theta_2^p$-hardness.
Consider a finite profile
$$ P=(J_1,\ldots,J_N). $$
Let $T_1,\ldots,T_q$ be its distinct judgment sets, and let $c_t$ be the multiplicity of $T_t$. Construct a rational-mass instance with
$$ \mu_t=\frac{c_t}{N}. $$
These masses are nonnegative, sum to $1$, and have polynomial-size binary encodings. For every feasible collective judgment set $J$,
$$ \begin{aligned} C(J) &=\sum_{t=1}^q\frac{c_t}{N}H(J,T_t)\\ &=\frac1N\sum_{r=1}^N H(J,J_r). \end{aligned} $$
Thus the rational-mass objective is exactly the finite-profile Kemeny objective multiplied by the positive constant $1/N$. Positive scaling does not change the set of minimizers. Keeping the agenda, $\Gamma_{in}$, $\Gamma_{out}$, and $L$ unchanged therefore preserves the answer exactly.
Collecting equal judgment sets and computing their multiplicities is polynomial-time. Hence finite-profile Kemeny outcome determination reduces to the rational-mass problem. By the given $\Theta_2^p$-completeness result, the rational-mass problem is $\Theta_2^p$-hard.
The rational-mass problem is in $\Delta_2^p=P^{NP}$ under the standard propositional encoding.
Write $\mu_t=a_t/b_t$ and let
$$ D=\prod_{t=1}^q b_t, \qquad w_t=a_t\frac{D}{b_t}. $$
Then minimizing $C(J)$ is equivalent to minimizing the integer objective
$$ W(J)=D\,C(J)=\sum_{t=1}^q w_tH(J,T_t). $$
Although $D$ may be numerically exponential, its binary length is at most the sum of the binary lengths of the denominators and is therefore polynomial in the input length. Moreover, because the masses sum to $1$,
$$ \sum_t w_t=D. $$
For an integer $K$, the threshold question
$$ \exists J: J\text{ is }\Gamma_{out}\text{-consistent and }W(J)\leq K $$
is in NP. Binary search over the polynomial-bit-length range of possible values determines the optimum using polynomially many adaptive NP-oracle queries. One final NP query asks whether a feasible $J$ satisfying $L\subseteq J$ has cost at most that optimum.
Consequently,
$$ \Theta_2^p\text{-hard} \;\subseteq\; \text{rational-mass Kemeny outcome determination} \;\subseteq\; \Delta_2^p. $$
The exact upper-bound classification is not needed for the target dichotomy.
Rational normalization does not make Kemeny outcome determination tractable. Ordinary finite profiles embed exactly, and NP-hardness already holds with a single unit-mass type.
⟨structured verdict parsed — rendered above⟩
The prover correctly resolves the target: rational-mass Kemeny outcome determination is NP-hard. The direct SAT reduction is valid, polynomial, and establishes NP-hardness even with one unit-mass type, $\Gamma_{in}=\top$, and singleton $L$.
The embedding of explicitly represented finite profiles also correctly establishes unrestricted $\Theta_2^p$-hardness, assuming the finite-profile completeness result stated in the task applies to the same outcome-determination formulation.
There is one minor ambiguity in the theorem statement concerning which hardness claim survives the severe restriction.
The variables, agenda, constraints, single type, and target set are all specified in polynomial size. The type
$$ T=\{\neg u_1,\ldots,\neg u_n,y,z_1,\ldots,z_n\} $$
chooses exactly one literal for every agenda variable and is consistent with $\Gamma_{in}=\top$.
No missing feasibility or encoding condition appears here.
Given a satisfying assignment $a$ for $\varphi$, setting $y=z_1=\cdots=z_n=1$ satisfies both:
The resulting judgment set differs from $T$ only on those $u_i$ assigned true by $a$. Therefore its issue-based Hamming distance is at most $n$.
For any feasible judgment set containing $\neg y$, each equivalence $z_j\leftrightarrow y$ forces $\neg z_j$. Such a set differs from $T$ on $y,z_1,\ldots,z_n$, hence has distance at least $n+1$. This strict separation proves that every minimizer contains $y$.
This reasoning is correct. Possible disagreements on the $u_i$ only increase the lower bound for the $\neg y$ case.
If a feasible complete judgment set contained $y$, then $y\rightarrow\varphi$ would require the assignment selected by that judgment set to satisfy $\varphi$. This contradicts unsatisfiability.
The all-false assignment satisfies $\Gamma_{out}$ because $y\rightarrow\varphi$ is vacuously true and every $z_j\leftrightarrow y$ has both sides false. Thus the feasible set is nonempty and a minimizer exists.
Consequently, no minimizer contains $L=\{y\}$. The many-one equivalence with SAT is established.
The comment concerning symmetric difference is correct: two complete literal sets differ in two literal memberships for every issue on which their truth assignments disagree. Both relevant costs are therefore doubled, preserving the strict inequality.
Grouping identical judgments into types and assigning mass
$$ \mu_t=\frac{c_t}{N} $$
is polynomial-time for an explicitly represented finite profile. The binary encoding length of each numerator and denominator is logarithmic in $N$.
The identity
$$ C(J)=\frac1N\sum_{r=1}^N H(J,J_r) $$
is exact. Multiplication by the positive constant $1/N$ preserves precisely the set of minimizers, and hence preserves whether some minimizer contains $L$.
Thus, under the finite-profile $\Theta_2^p$-completeness result supplied in the task, the unrestricted rational-mass problem is indeed $\Theta_2^p$-hard.
The denominator-clearing argument is correct:
$$ D=\prod_t b_t,\qquad w_t=a_tD/b_t $$
produces integer weights with polynomial binary length. Although $D$ may be exponentially large numerically, its encoding length is at most the sum of the denominator encoding lengths.
Since $\sum_t a_t/b_t=1$, the identity $\sum_t w_t=D$ is also correct. The possible objective values have polynomial bit length, so binary search requires polynomially many adaptive NP queries, not polynomially many queries in the numerical magnitude of the range.
The threshold predicate has an NP certificate consisting of a feasible judgment set, together with any auxiliary propositional assignment needed to certify consistency, and the weighted cost can be checked with polynomial-bit arithmetic.
After the optimum is computed, asking whether a feasible $J$ containing $L$ has cost at most that optimum correctly tests whether such an optimal $J$ exists.
The stated $\Delta_2^p=P^{NP}$ upper bound is therefore justified.
The theorem says:
“In fact ... it is $\Theta_2^p$-hard. This remains true even with one judgment type...”
Grammatically, “This remains true” most naturally refers to the immediately preceding $\Theta_2^p$-hardness claim. The direct reduction proves only NP-hardness under the one-type restriction. The later finite-profile embedding proves $\Theta_2^p$-hardness only for unrestricted numbers of types.
The intended statement is evidently that NP-hardness remains true under those restrictions. This is a minor wording issue because correcting it requires no new mathematics, but the current phrasing should not be read as establishing restricted $\Theta_2^p$-hardness.
⟨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.