Answer: \(\Sigma_2^P\)-complete, hence NP-hard, even when \(m=2\) and \(\tau=2\).
Theorem 6 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateIn the case where the axioms in the cor- pus A are given as quantifier-free sentences, the problem EXISTS-JUST is ΣP 2-complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given alternatives \(X\), ranking types \(T=\mathcal{L}(X)\), a target rational society \(\mu^\star\), a desired outcome \(X^\star\), and a finite quantifier-free corpus \(A\) of grounded outcome constraints at listed rational societies \(\mu_j\), does there exist \(A_N\subseteq A\) and an explanation \(A_E\) consisting of instances of \(A_N\) such that \(A_N\) is satisfied by some population rule \(F:\Delta(T)\to 2^X\setminus\{\varnothing\}\), every rule satisfying \(A_E\) selects exactly \(X^\star\) at \(\mu^\star\), and no proper subset of \(A_E\) forces that outcome?
Let \(X\) contain \(m\geq 1\) alternatives, let \(T=\mathcal L(X)\) be the strict ranking types, and let \(\Delta(T)\) be the distributions on \(T\) with nonnegative masses summing to \(1\).
A society is given by its support: the list of its \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) denotes the maximum support size among input societies, not the number \(m!\) of possible types.
The input comprises a target rational society \(\mu^\star\), a nonempty desired outcome \(X^\star\subseteq X\), listed rational societies \(\mu_1,\ldots,\mu_q\), and a finite corpus \(A\) of explicitly written Boolean formulas over atoms \(o(x,\mu_j)\), using negation and conjunction with the usual Boolean abbreviations.
A population rule is any function \(F:\Delta(T)\to 2^X\setminus\{\varnothing\}\); the atom \(o(x,\mu_j)\) means \(x\in F(\mu_j)\). Equal distributions denote the same society. Satisfaction uses ordinary Boolean semantics.
Because the corpus is quantifier-free, a formula's only instance is itself: an explanation therefore satisfies \(A_E\subseteq A_N\subseteq A\).
Call such a pair a justification if some rule satisfies \(A_N\), every rule satisfying \(A_E\) has \(F(\mu^\star)=X^\star\), and for every \(B\subsetneq A_E\) some rule satisfying \(B\) has \(F(\mu^\star)\neq X^\star\).
Let \(L\) be the total binary input length; state running times in \(m,\tau,q,|A|,L\).
Is deciding whether a justification exists solvable in polynomial time, or is it NP-hard?
For finite electorates with explicitly given quantifier-free corpora, justification existence is \(\Sigma_2^P\)-complete. [Boixel and de Haan](https://ojs.aaai.org/index.php/AAAI/article/download/16656/16463)
No result for exactly the distribution-based problem above was located in the literature search.
The problem is \(\Sigma_2^P\)-complete, and therefore NP-hard. Hardness holds even when \(m=2\) and \(\tau=2\).
The proof below applies directly to rational distributions; it does not require transferring the finite-electorate result.
Write \(G\) for the condition \(F(\mu^\star)=X^\star\). A set of formulas is *satisfiable* if some population rule satisfies every formula in it.
Lemma. A justification exists if and only if there is a satisfiable subset \(S\subseteq A\) such that every rule satisfying \(S\) satisfies \(G\).
Proof. If \((A_N,A_E)\) is a justification, a rule satisfying \(A_N\) also satisfies \(A_E\), because \(A_E\subseteq A_N\). Thus \(S=A_E\) is satisfiable and forces \(G\).
Conversely, suppose such an \(S\) exists. Because \(S\) is finite, choose an inclusion-minimal subset \(E\subseteq S\) that forces \(G\). The rule witnessing satisfiability of \(S\) also witnesses satisfiability of \(E\). For every proper subset \(B\subsetneq E\), minimality means that \(B\) does not force \(G\); equivalently, some rule satisfies \(B\) and violates \(G\). Hence \(A_N=A_E=E\) is a justification. \(\square\)
For the degenerate case \(m=1\), every rule necessarily returns \(X=X^\star\), so the empty pair is always a justification. The hardness construction uses \(m=2\).
Identify equal distributions among \(\mu^\star,\mu_1,\ldots,\mu_q\), and let their distinct values be \(\nu_1,\ldots,\nu_r\), where \(r\leq q+1\).
For every \(s\in\{1,\ldots,r\}\) and \(x\in X\), introduce a Boolean variable \(z_{s,x}\). Its intended meaning is \(x\in F(\nu_s)\). Valid assignments are exactly those satisfying
\(D=\displaystyle\bigwedge_{s=1}^{r}\left(\bigvee_{x\in X}z_{s,x}\right).\)
Indeed, each conjunct requires a nonempty outcome. Conversely, every assignment satisfying \(D\) extends to a population rule: use the assigned outcomes on these distinct societies and a fixed singleton outcome everywhere else.
Replace each corpus atom by its corresponding variable. If \(\nu_{s^\star}=\mu^\star\), the target condition becomes
\(G=\displaystyle\left(\bigwedge_{x\in X^\star}z_{s^\star,x}\right)\wedge\left(\bigwedge_{x\in X\setminus X^\star}\neg z_{s^\star,x}\right).\)
Thus, for any \(S\subseteq A\), rule satisfiability is precisely satisfiability of \(D\wedge\bigwedge_{\alpha\in S}\alpha\), and forcing the target means that this Boolean formula entails \(G\). This representation uses \(N=mr\leq m(q+1)\) variables. It never enumerates the \(m!\) ranking types.
Distribution equality is also polynomial-time computable. Match the explicitly listed rankings and compare their rational masses exactly by cross multiplication. Comparing all pairs of societies by a straightforward implementation takes at most
\(P=O\!\left((q+1)^2\tau^2L^2\right)\)
bit operations: there are at most \(\tau^2\) support-entry comparisons per society pair, and an entry comparison costs at most \(O(L^2)\).
Let \(a=|A|\). By the lemma, it suffices to guess a subset \(S\subseteq A\) and a valid Boolean assignment \(v\) satisfying \(S\), then require every valid assignment satisfying \(S\) to satisfy \(G\).
More explicitly, if \(C_S=\bigwedge_{\alpha\in S}\alpha\), the required condition is
\(\displaystyle\exists(S,v)\ \forall w:\quad D(v)\wedge C_S(v)\wedge\bigl(\neg D(w)\vee\neg C_S(w)\vee G(w)\bigr).\)
Here \(S\) uses \(a\) bits, and each assignment uses \(N\leq m(q+1)\) bits. The predicate is polynomial-time evaluable. This proves membership in \(\Sigma_2^P\).
For explicit running-time bounds, a conservative bit-operation bound for evaluating the predicate after preprocessing is
\(O\!\left((L+a+m(q+1))^2\right).\)
Equivalently, a nondeterministic algorithm guesses \(S\) and its satisfying assignment, then makes one NP-oracle query asking whether a valid counterexample to \(G\) exists. Its non-oracle work is bounded by
\(O\!\left(P+(L+a+m(q+1))^2\right).\)
A deterministic exhaustive algorithm scans all assignments for each subset \(S\), recording whether \(S\) has a valid model and whether it has a valid model violating \(G\). Its running time is bounded by
\(O\!\left((q+1)^2\tau^2L^2+2^{\,|A|+m(q+1)}(L+|A|+m(q+1))^2\right).\)
We reduce from the standard \(\Sigma_2^P\)-complete problem of deciding the truth of a quantified Boolean formula
\(\displaystyle\exists u_1,\ldots,u_k\ \forall v_1,\ldots,v_\ell:\ \varphi(u_1,\ldots,u_k,v_1,\ldots,v_\ell),\)
where \(\varphi\) is explicitly given in \(3\)-DNF. This source problem and its completeness are stated in the proof of Theorem 6 of [Boixel and de Haan](https://ojs.aaai.org/index.php/AAAI/article/download/16656/16463).
Put \(n=k+\ell\). We may assume \(n\geq1\), since adding an unused variable preserves truth.
Set \(X=\{a,b\}\), with ranking types \(t_+=(a\succ b)\) and \(t_-=(b\succ a)\). Choose
\(D_0=2^{\lceil\log_2(n+2)\rceil}.\)
For each \(i\in\{1,\ldots,n+1\}\), define
\(\mu_i(t_+)=i/D_0,\qquad \mu_i(t_-)=(D_0-i)/D_0.\)
Both masses are positive, sum to one, and are dyadic rationals with \(O(\log(n+2))\)-bit encodings. The societies are pairwise distinct because their masses on \(t_+\) differ.
Take \(q=n+1\), \(\mu^\star=\mu_{n+1}\), and \(X^\star=\{a\}\). Thus every society has support size exactly two.
For \(i\leq n\), write \(p_i=o(a,\mu_i)\). Interpret \(p_1,\ldots,p_k\) as the existential variables and \(p_{k+1},\ldots,p_n\) as the universal variables. Let \(\widehat\varphi\) be the resulting atom substitution in \(\varphi\).
Define
\(G=o(a,\mu_{n+1})\wedge\neg o(b,\mu_{n+1}),\qquad h=\neg\widehat\varphi\vee G,\)
and set
\(A=\{p_i,\neg p_i:1\leq i\leq k\}\cup\{h\}.\)
All formulas are quantifier-free and use the permitted Boolean abbreviations.
Every assignment to \(p_1,\ldots,p_n\) is realizable: choose outcome \(\{a\}\) at \(\mu_i\) when \(p_i\) is true and \(\{b\}\) when it is false. Independently, choosing \(\{a\}\) at the target makes \(G\) true, while choosing \(\{b\}\) makes \(G\) false. Independence holds because all these societies are distinct.
Suppose the quantified formula is true. Let \(\alpha\) be an existential assignment witnessing its truth, and choose
\(S_\alpha=\{h\}\cup\{p_i:\alpha(u_i)=1\}\cup\{\neg p_i:\alpha(u_i)=0\}.\)
This set is satisfiable: realize the selected existential assignment, choose arbitrary universal values, and choose target outcome \(\{a\}\). Then \(G\), and hence \(h\), is true.
Now consider any rule satisfying \(S_\alpha\). Its existential values equal \(\alpha\), and its universal values form some assignment \(\beta\). By the defining property of \(\alpha\), \(\widehat\varphi\) is true. Since the rule also satisfies \(h=\neg\widehat\varphi\vee G\), it must satisfy \(G\).
Thus \(S_\alpha\) is satisfiable and forces the target. The lemma gives a justification.
Suppose a justification exists. By the lemma, there is a satisfiable \(S\subseteq A\) forcing \(G\).
First, \(h\in S\). Otherwise, every formula in \(S\) concerns a non-target society. Modify a rule satisfying \(S\) only at the target, giving it outcome \(\{b\}\). The modified rule still satisfies \(S\), but violates \(G\), a contradiction.
Second, \(S\) cannot contain both \(p_i\) and \(\neg p_i\), because \(S\) is satisfiable. Its selected literals therefore define a consistent partial assignment to the existential variables. Extend that assignment arbitrarily to a total assignment \(\alpha\).
Fix any assignment \(\beta\) to the universal variables. If \(\varphi(\alpha,\beta)\) were false, realize \(\alpha,\beta\) at the corresponding societies and give the target outcome \(\{b\}\). Every selected literal is satisfied. Moreover, \(\widehat\varphi\) is false, so \(h\) is satisfied even though \(G\) is false. This would be a rule satisfying \(S\) and violating \(G\), again a contradiction.
Consequently, \(\varphi(\alpha,\beta)\) is true for every \(\beta\). The quantified formula is true.
The reduction has parameters
\(m=2,\qquad \tau=2,\qquad q=n+1,\qquad |A|=2k+1.\)
If \(K\) is the total bit length of the source instance, the constructed input has length \(O(K\log(K+2))\) and can be produced in polynomial time. Boolean abbreviations expand into negation and conjunction with only a linear increase in formula length.
Both directions are proved, so this is a polynomial-time many-one reduction.
Justification existence is \(\Sigma_2^P\)-complete, even with two alternatives and support size two. In particular, it is NP-hard and cannot be polynomial-time solvable unless \(\mathrm{P}=\mathrm{NP}\).
⟨structured verdict parsed — rendered above⟩
The output proves the claimed result: justification existence is \(\Sigma_2^P\)-complete, hence NP-hard, even when \(m=2\) and \(\tau=2\). I found no mathematical errors or gaps requiring clarification.
The lemma correctly characterizes justification existence by the existence of a satisfiable subset \(S\subseteq A\) forcing the target condition \(G\).
In the forward direction, satisfiability of \(A_N\) implies satisfiability of \(A_E\), since \(A_E\subseteq A_N\). Explanatoriness supplies entailment of \(G\).
In the reverse direction, finiteness ensures the existence of an inclusion-minimal subset \(E\subseteq S\) forcing \(G\). Every subset of the satisfiable set \(S\) is satisfiable. For every proper subset \(B\subsetneq E\), failure to force \(G\) means precisely that a rule satisfies \(B\) while violating \(G\). Taking \(A_N=A_E=E\) therefore satisfies all three requirements in the task.
This argument correctly handles all proper subsets, rather than merely asserting minimality under individual deletions.
When \(m=1\), the nonempty desired outcome necessarily equals \(X\), and every population rule must return \(X\). The empty pair satisfies consistency and entailment; its minimality condition is vacuous. Thus the stated edge case is correct, even if the full corpus is inconsistent.
Identifying equal distributions before introducing variables is essential and is correctly included. It ensures that two names for the same society cannot receive different outcomes.
The formula \(D\) enforces exactly the required nonempty outcomes on all relevant societies. Every population rule induces an assignment satisfying \(D\). Conversely, assigning a fixed singleton elsewhere extends any assignment satisfying \(D\) to a rule on all of \(\Delta(T)\). This extension is legitimate because the task imposes no continuity, measurability, or other restrictions on rules.
The expression for \(G\) correctly enforces equality with \(X^\star\), including exclusion of every alternative outside \(X^\star\).
Consequently, both satisfiability and entailment are preserved by the Boolean representation. The variable bound \(N=mr\leq m(q+1)\) is correct, and no enumeration of ranking types is required.
On the task’s valid support-list inputs, matching the listed rankings and comparing their positive masses exactly determines distribution equality. Types absent from a support have zero mass and therefore require no additional enumeration.
Exact cross multiplication correctly compares binary rational masses, including differently represented equal rationals. A straightforward pairwise support comparison uses at most \(\tau^2\) entry comparisons per pair of societies. Each comparison fits within the conservative \(O(L^2)\) bit-operation bound, including ranking comparison and integer arithmetic.
The resulting preprocessing bound
\[
O\!\left((q+1)^2\tau^2L^2\right)
\]
is valid.
The quantified predicate has the correct logical structure. The existential assignment \(v\) witnesses consistency of the selected subset. The universal assignment \(w\) tests entailment only when it represents a valid outcome assignment satisfying that subset.
The selection string has \(|A|\) bits, and each assignment has at most \(m(q+1)\) bits. Since societies and rankings are explicitly listed, these lengths are polynomially bounded by the input length. Evaluation of the explicitly written formulas is polynomial-time.
The stated quadratic evaluation bound is conservative and sufficient. The NP-oracle formulation is also correct: counterexample existence is an NP question, and the nondeterministic machine accepts when that query returns a negative answer. The reported work bound explicitly excludes oracle computation.
The deterministic algorithm examines \(2^{|A|}\) subsets and at most \(2^{m(q+1)}\) assignments per subset. Recording both model existence and counterexample existence suffices by the lemma. Its stated running-time bound is therefore valid.
The source problem is stated precisely: truth of a formula with an existential block followed by a universal block and an explicitly written \(3\)-DNF matrix. The proof of Theorem 6 in the cited paper explicitly identifies this problem as \(\Sigma_2^P\)-complete. Thus the citation supports exactly the source problem used here. [Boixel and de Haan, proof of Theorem 6](https://ojs.aaai.org/index.php/AAAI/article/download/16656/16463)
Adding an unused variable preserves truth and justifies the assumption \(n\geq1\).
The denominator satisfies \(D_0\geq n+2\). Hence, for every constructed index, both numerators are positive, and the masses sum to one. All constructed societies have support size exactly two.
Different indices give different masses on \(t_+\), so the societies are pairwise distinct. In particular, the target is distinct from every society encoding a Boolean variable. The dyadic masses have \(O(\log(n+2))\)-bit encodings.
Every Boolean assignment is realizable using the outcomes specified in the output. Target truth and falsity are independently realizable at the distinct target society.
The corpus uses only permitted atoms and Boolean operations. Although \(G\) contains two target atoms, it expresses exactly the desired outcome \(\{a\}\).
The subset \(S_\alpha\) is satisfiable because setting the target outcome to \(\{a\}\) makes \(G\), and therefore \(h\), true.
Every rule satisfying \(S_\alpha\) assigns the existential variables according to \(\alpha\). Its universal atom values constitute a Boolean assignment, regardless of any additional winning alternatives at those societies. The source formula’s truth under every such assignment makes \(\widehat\varphi\) true. Satisfaction of \(h\) then forces \(G\).
The lemma consequently supplies a justification. No assumption that all rule outcomes are singletons is made or needed.
If \(h\) were absent, a satisfying rule could be modified solely at the distinct target society without affecting any selected literal. Choosing \(\{b\}\) would violate \(G\), contradicting entailment. Thus \(h\in S\).
Satisfiability excludes selecting both polarities of an existential atom. The selected literals therefore determine a consistent partial assignment, which admits a total extension \(\alpha\).
For any universal assignment \(\beta\), falsity of \(\varphi(\alpha,\beta)\) would make \(h\) true even with target outcome \(\{b\}\). The resulting rule would satisfy every formula of \(S\) and violate \(G\). This contradiction proves truth for every \(\beta\).
The quantifier order is correct: one extension \(\alpha\) is fixed before considering arbitrary \(\beta\).
The parameter counts \(m=2\), \(\tau=2\), \(q=n+1\), and \(|A|=2k+1\) are correct. The constructed society encodings and indexed atom references satisfy the stated polynomial size bound. Expanding the Boolean abbreviations used in the construction causes only linear growth.
The reduction establishes \(\Sigma_2^P\)-hardness under polynomial-time many-one reductions. Combined with membership, it establishes completeness. The conclusion that a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{NP}\) follows from NP-hardness.
No repair or additional clarification is needed.
⟨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.