Answer: Both decision problems are \(\mathrm{NP}\)-hard under polynomial-time many-one reductions, already with \(\tau=1\), disjunction-free generating rules, and one unconditional binary preference rule.
Theorem 1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateLet ⟨P, Φ⟩be a prioritized program. Then 1. Deciding whether a ground atom G is true in some preferred stable models of ⟨P, Φ⟩ is Σp 3-complete; 2. Deciding whether a ground atom G is true in all preferred stable models of ⟨P, Φ⟩is Πp 3-complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite policy schema, complete case types \(T\), and binary-rational masses \(\mu_t\), represent a population interpretation by masses \(x_{t,S}\) assigned to local stable states \(S\), with \(\sum_S x_{t,S}=\mu_t\). Lift PAS's strata and conflict comparisons so a preference rule witnesses a comparison only on positive mass. Decide whether some PAS-preferred population interpretation gives \(G\) positive mass, and whether every such interpretation gives \(G\) mass one.
Input consists of a finite propositional policy \(\Pi=(P,\Phi)\) over \(m\) atoms, a designated set \(E\) of exogenous atoms absent from rule heads of \(P\), and a query atom \(G\). \(P\) is a disjunctive logic program with default negation and constraints; exclusive disjunction means exactly one head atom when the body holds. Preference rules have form \(a_1>\cdots>a_k\leftarrow B\), with \(k>1\) and \(B\) a conjunction of atoms and default-negated atoms.
A society is given by its support: the list of \(\tau\) complete types \(t\subseteq E\) with positive binary-rational masses \(\mu_t\), normalized by \(\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 and \(r\) the number of policy rules; state running times in \(m,\tau,L,r\).
For each type, let \(\mathcal S_t=\operatorname{SM}(P\cup\{e\leftarrow:e\in t\})\); these local stable states are implicit, not supplied as a list. A population interpretation is a family of real masses \(x_{t,S}\geq0\), indexed by \(S\in\mathcal S_t\), satisfying \(\sum_Sx_{t,S}=\mu_t\). Define \(g(x)=\sum_{t,S:G\in S}x_{t,S}\).
Split preference chains into adjacent binary rules and take their conditional transitive closure \(\Phi^*\): compose \(a>b\leftarrow B\) and \(b>c\leftarrow C\) into \(a>c\leftarrow B\land C\) when \(a\ne c\). Treat bodies as sets of signed literals.
To obtain strata, form a graph on policy atoms and a fresh \(\mathsf{true}\): preference rules give edges from every body atom to every head atom, of weight \(1\); generating rules give edges from every head or body atom to every head atom, of weight \(0\). Ignore negation signs and treat empty bodies as \(\mathsf{true}\). Collapse strongly connected components; a source has level \(0\), and every other component has the maximum predecessor level plus edge weight. A closure rule's stratum is the maximum level of its body atoms, with empty bodies at level \(0\).
For \(\rho:a>b\leftarrow B\), put \(R_{t,\rho}(x)=\sum_{S\models B\land(a\lor b)}x_{t,S}\). Opposite-head rules are conflicting. Interpret \(R_{t,\rho}(x)>0\) as relevance on positive mass.
Populations \(x,y\) are comparable at stratum \(0\). They remain comparable at stratum \(i+1\) precisely when they were comparable at \(i\) and there are no type \(t\) and conflicting rules \(\rho,\sigma\) in stratum \(i\) with \(R_{t,\rho}(x)>0=R_{t,\sigma}(x)\) and \(R_{t,\sigma}(y)>0=R_{t,\rho}(y)\).
A rule \(\rho:a>b\leftarrow B\) witnesses \(x\) over \(y\) if some \(t\) and \(S,U\in\mathcal S_t\) satisfy \(x_{t,S}>y_{t,S}\), \(y_{t,U}>x_{t,U}\), \(S,U\models B\), \(a\in S\setminus U\), and \(b\in U\setminus S\).
Define \(x\succeq y\) when a rule in some stratum \(i\) witnesses \(x\) over \(y\), the populations are comparable there, and no rule in any stratum \(j<i\) witnesses \(y\) over \(x\). Define \(x\succ y\) by \(x\succeq y\) and \(y\not\succeq x\), without taking a transitive closure. A population is PAS-preferred if no feasible population strictly dominates it.
Are each of the following decision problems in \(\mathrm P\) or NP-hard: does some PAS-preferred population \(x\) satisfy \(g(x)>0\), and does every PAS-preferred population \(x\) satisfy \(g(x)=1\)? Universal quantification over an empty preferred set is true.
Discrete PAS atom truth in some preferred stable model is \(\Sigma_3^p\)-complete, and truth in every preferred stable model is \(\Pi_3^p\)-complete, under data complexity; for disjunction-free generating programs the corresponding bounds are \(\Sigma_2^p\)- and \(\Pi_2^p\)-completeness. [Source](https://www.ed.aaai.org/Papers/JAIR/Vol30/JAIR-3013.pdf).
No result settling this exact population formulation was located in the literature search.
Both decision problems are NP-hard under polynomial-time many-one reductions. This holds already with \(\tau=1\), a disjunction-free generating program, and one unconditional binary preference rule. The reduction always has at least one preferred population, so the universal question does not rely on vacuous truth.
Let \(F=C_1\land\cdots\land C_c\) be a \(3\)-CNF formula over variables \(z_1,\ldots,z_n\). Introduce distinct policy atoms \(G,D,p_1,n_1,\ldots,p_n,n_n\). Here \(p_i,n_i\) are ordinary atoms representing the two possible truth values of \(z_i\).
Take \(E=\varnothing\), with the single supported type \(t=\varnothing\) and mass \(\mu_t=1\). The query is \(G\).
The generating program \(P_F\) contains the following rules:
Thus the constraint for a clause forbids precisely its falsification in the \(G\) branch.
The preference set consists of the single rule \(\rho:G>D\leftarrow\), with empty body.
For an assignment \(A\), define
\(S_A=\{G\}\cup\{p_i:A(z_i)=1\}\cup\{n_i:A(z_i)=0\}\).
Also define \(S_D=\{D\}\).
Lemma 1. The local stable states are exactly
\(\mathcal S=\{S_D\}\cup\{S_A:A\models F\}\).
Proof. For a normal program, its reduct removes each rule whose default-negated body contains an atom in the candidate state, and then removes the remaining default negations. The positive generating rules have a least model. A candidate is stable precisely when it equals that least model and satisfies the reduct’s constraints: every model contains the least model, and a positive constraint violated by the least model is violated by every larger model.
Let \(S\) be a stable state.
First, \(S\) contains exactly one of \(G,D\):
If \(D\in S\), then \(G\notin S\). Every rule generating an assignment atom requires \(G\), so the reduct’s least model is exactly \(\{D\}\). All constraints require \(G\), so \(S_D\) is indeed stable.
Suppose instead that \(G\in S\). For each \(i\), exactly one of \(p_i,n_i\) must belong to \(S\):
Consequently \(S=S_A\) for a unique assignment \(A\). For such a candidate, the reduct contains the fact \(G\) and derives exactly the selected assignment atoms. Its least model is therefore \(S_A\). A clause constraint is violated exactly when every literal in that clause is false under \(A\). Hence \(S_A\) is stable exactly when \(A\models F\). This proves the lemma. \(\square\)
In particular, feasibility is guaranteed even when \(F\) is unsatisfiable.
The preference closure contains only \(\rho\): there is no rule with which it can compose. Its empty body puts it in stratum \(0\). All populations are comparable at that stratum, and there are no earlier strata to check.
Suppress the singleton type index and write \(x_S=x_{t,S}\). Let \(q(x)=x_{S_D}\). By Lemma 1, every other stable state contains \(G\), while \(S_D\) does not. Thus
\(g(x)=1-q(x)\).
Lemma 2. For any feasible populations \(x,y\),
\(x\succeq y\ \Longleftrightarrow\ q(x)<q(y)\),
and consequently
\(x\succ y\ \Longleftrightarrow\ q(x)<q(y)\).
Proof. The sole rule can witness \(x\) over \(y\) only by using a satisfying-assignment state \(S_A\) as its \(G\) state and \(S_D\) as its \(D\) state. Its witness conditions are therefore precisely
\(x_{S_A}>y_{S_A}\) and \(y_{S_D}>x_{S_D}\)
for some \(A\models F\). A witness immediately implies \(q(x)<q(y)\).
Conversely, suppose \(q(x)<q(y)\). Since both populations have total mass \(1\),
\(\sum_{A\models F}(x_{S_A}-y_{S_A})=q(y)-q(x)>0\).
This is a finite sum, so some satisfying assignment \(A\) has \(x_{S_A}>y_{S_A}\). Together with \(y_{S_D}>x_{S_D}\), this supplies a witness. Comparability and the absence of earlier strata then give \(x\succeq y\).
Finally, \(q(x)<q(y)\) excludes \(q(y)<q(x)\), so the same characterization holds for strict dominance. \(\square\)
This argument applies to arbitrary real masses and uses exactly the specified dominance relation, without taking a transitive closure.
If \(F\) is unsatisfiable, Lemma 1 gives just \(S_D\). The unique feasible population assigns it mass \(1\). It is preferred and has \(g(x)=0\). Therefore both questions have answer no.
If \(F\) is satisfiable, fix a satisfying assignment \(A\). Any feasible population \(x\) with \(q(x)>0\) is strictly dominated: transfer all its mass on \(S_D\) to \(S_A\), obtaining a feasible population \(y\) with \(q(y)=0<q(x)\). Lemma 2 gives \(y\succ x\).
Conversely, a population with \(q(x)=0\) cannot be strictly dominated, because no feasible population has negative mass on \(S_D\). Such populations exist, for example the population assigning mass \(1\) to \(S_A\). Thus the preferred populations are exactly those with \(q(x)=0\), and every one has \(g(x)=1\). Therefore both questions have answer yes.
We have proved the two equivalences
\(F\text{ is satisfiable}\ \Longleftrightarrow\ \exists x\text{ preferred with }g(x)>0\),
\(F\text{ is satisfiable}\ \Longleftrightarrow\ \forall x\text{ preferred},\ g(x)=1\).
Since \(3\)-SAT is NP-hard, these are polynomial-time many-one reductions proving NP-hardness of both target problems.
The construction has
\(m=2n+2,\qquad \tau=1,\qquad |P_F|=2n+c+2,\qquad |\Phi_F|=1\).
Counting generating and preference rules together gives \(r=2n+c+3\). All bodies have constant length, and the sole society mass is the binary rational \(1\).
With binary atom identifiers, the output length satisfies \(L=O((m+r)\log(m+r+2))\). The construction requires \(O(m+r+\tau)\) rule and support operations; including encoding and reading the source formula, its bit running time is \(O(N+L)\), where \(N\) is the formula’s encoded length. This is polynomial in the source input size.
Thus an algorithm polynomial in \(m,\tau,L,r\) for either question would yield a polynomial-time algorithm for \(3\)-SAT. No claim of membership in NP or of an exact higher complexity classification is needed for the requested NP-hardness conclusion.
⟨structured verdict parsed — rendered above⟩
The prover’s claim is proved. Both reductions are correct under the specified population semantics. No major or minor mathematical issues were found.
The construction produces a valid instance of the task:
For each clause, the constraint body contains precisely the assignment atoms representing falsity of its literals. In an assignment state, the constraint therefore excludes exactly assignments falsifying that clause.
The reduction does not require finding a satisfying assignment during construction.
Lemma 1 correctly applies the reduct characterization for finite normal programs with constraints. After removing default negation, the nonconstraint rules are positive Horn rules and have a least model. Positive constraints are preserved under taking subsets of a satisfying interpretation; equivalently, if the least model violates a constraint, every interpretation containing it violates that constraint. Thus the stated stability criterion is valid.
The cases exhaust all candidate stable states:
Consequently,
\[
\mathcal S=\{S_D\}\cup\{S_A:A\models F\}
\]
is established in both directions. In particular, every constructed instance has a feasible population.
The preference closure contains only the original rule: composing it with itself would require its second head atom \(D\) to equal its first head atom \(G\), which is impossible.
Its stratum is \(0\) because its body is empty. This follows directly from the task’s rule-stratum definition, regardless of the graph levels assigned to \(G\) and \(D\).
All populations are comparable at stratum \(0\), and there are no earlier strata. Therefore, in this construction, existence of a witness for the sole preference rule is exactly the condition for weak dominance.
Every stable state other than \(S_D\) contains \(G\), so normalization gives
\[
g(x)=1-q(x).
\]
A witness must use a satisfying-assignment state for its \(G\) side and \(S_D\) for its \(D\) side. Thus a witness implies \(q(x)<q(y)\).
Conversely, the identity
\[
\sum_{A\models F}\bigl(x_{S_A}-y_{S_A}\bigr)=q(y)-q(x)
\]
is correct. The state set is finite, so a positive sum implies that at least one summand is positive. This gives exactly the required witness.
If \(F\) is unsatisfiable, the assignment-state sum is empty and every feasible population has \(q=1\); the converse implication has an impossible premise. There is no missing edge case.
The resulting weak-dominance characterization also correctly implies
\[
x\succ y\quad\Longleftrightarrow\quad q(x)<q(y),
\]
because the reverse strict inequality cannot simultaneously hold. No transitive closure is used.
For unsatisfiable \(F\), there is exactly one feasible population. It cannot be strictly dominated and has \(g=0\). Both decision questions therefore answer no, including the universal question because its preferred set is nonempty.
For satisfiable \(F\), transferring the mass on \(S_D\) to any fixed satisfying-assignment state preserves feasibility and strictly lowers \(q\) whenever \(q>0\). Hence every such population is strictly dominated.
A population with \(q=0\) cannot be strictly dominated, since feasible populations have nonnegative coordinates. Such populations exist. Thus the preferred populations are exactly those with \(q=0\), all of which have \(g=1\).
Both stated equivalences with satisfiability follow. These are separate valid many-one reductions from \(3\)-SAT to the existential and universal decision problems.
The counts are correct:
\[
m=2n+2,\qquad \tau=1,\qquad r=2n+c+3.
\]
Since clauses have at most three literals, rule bodies have bounded length. Binary atom identifiers give the stated polynomial bound on \(L\), and the explicit construction takes polynomial time in the source encoding length.
The output establishes NP-hardness for both problems. Membership in NP or a tighter complexity classification is unnecessary for that conclusion. No clarification or repair is required.
⟨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.