Answer: \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\)-complete under polynomial-time many-one reductions; in particular, \(\mathrm{NP}\)-hard.
Proposition 8 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateMERGE(∆PLMIN,X) in Θp 2. Let X = (X1, ..., Xn), where Xi = bo, maxsat, or leximin (i = 1, ..., n), then MERGE(∆PLMIN,X) is Θp 2-complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite propositional language, a satisfiable integrity constraint \(\kappa\), a query \(\psi\), and a finite support of types \(t=(K_t,X_t)\) with positive binary-rational masses \(\lambda_t\) summing to \(1\), take each type's priority-level function \(\ell_t(w)\) as available after the paper's assumed offline stratification. Let \(R\) be the largest priority level and, for each world \(w\models\kappa\), set \(F_w(j)=\sum_{t:\ell_t(w)\le j}\lambda_t\) for \(j=1,\ldots,R-1\). Select the worlds lexicographically maximizing \((F_w(1),\ldots,F_w(R-1))\); decide whether every selected world satisfies \(\psi\).
Fix a propositional language with \(m\) atoms and worlds \(\Omega=\{0,1\}^m\). Input includes propositional formulas \(\kappa,\psi\), with \(\kappa\) satisfiable.
A society is given by its support: \(\tau\) types \(t=(K_t,X_t)\), each with positive binary-rational mass \(\lambda_t\), where \(\sum_t\lambda_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each \(K_t\) is a finite sequence of nonempty strata of propositional formulas, ordered from most to least important; inconsistency is allowed. Its ordering strategy \(X_t\) supplies a total preorder on all worlds.
Offline stratification is supplied as a Boolean circuit computing \(\ell_t(w)\) in binary and a binary integer \(R_t\). These are promised to give the consecutive ranks \(1,\ldots,R_t\) of the preorder's nonempty equivalence classes, with rank \(1\) best; ranks are computed over all \(\Omega\), before imposing \(\kappa\). Computing or checking this preprocessing is outside the problem.
Put \(R=\max_tR_t\). For \(w\models\kappa\), define \(F_w(j)=\sum_{t:\ell_t(w)\le j}\lambda_t\) for \(1\le j<R\). Select every world lexicographically maximizing \((F_w(1),\ldots,F_w(R-1))\); retain all ties, and use the empty vector when \(R=1\).
Let \(L\) be the total binary input length, including formulas, masses, rank circuits, and rank bounds. State running times in \(m,\tau,L\), and \(\log R\).
Is deciding whether every selected world satisfies \(\psi\) solvable in polynomial time, or is it NP-hard?
For finite multisets of bases, the corresponding entailment problem is \(\Theta_2^p\)-complete for best-out, maxsat, and leximin strategies under offline stratification ([Qi, Liu, and Bell, 2006](https://aaai.org/Papers/AAAI/2006/AAAI06-045.pdf)). No result settling the exact rational-mass problem with the input encoding above was located.
For unbounded \(m\), the problem is \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\)-complete under polynomial-time many-one reductions, on the promised inputs. In particular, it is \(\mathrm{NP}\)-hard and has no polynomial-time algorithm unless \(\mathrm{P}=\mathrm{NP}\).
The hardness already holds with \(R=2\), dyadic masses, and bases consisting of one singleton stratum. For genuinely fixed \(m\), exhaustive enumeration gives polynomial time in the remaining input size.
I first give a direct \(\mathrm{NP}\)-hardness reduction, then prove the stronger classification and running-time bounds.
Let \(\varphi\) be an arbitrary propositional formula. Introduce fresh atoms \(s,y\), and define
\(\kappa=s\land y,\qquad \psi=\varphi,\qquad g=\neg s\lor(y\land\varphi).\)
Use one type of mass \(1\), with rank circuit
\(\ell(w)=1\) if \(w\models g\), and \(\ell(w)=2\) otherwise.
Set \(R_1=2\). This preorder can be induced by the base with the single stratum \(\{g\}\), using any of best-out, maxsat, or leximin: satisfying \(g\) is strictly preferable to falsifying it.
Both offline rank classes are nonempty independently of \(\varphi\): worlds with \(s=0\) have rank \(1\), while worlds with \(s=1,y=0\) have rank \(2\). Also, \(\kappa\) is always satisfiable.
On worlds satisfying \(\kappa\), the formula \(g\) is equivalent to \(\varphi\). Consequently:
Thus the constructed instance answers yes exactly when \(\varphi\) is satisfiable. The construction has polynomial size and satisfies every promise. This proves \(\mathrm{NP}\)-hardness even with \(\tau=1\) and \(R=2\).
The apparent obstacle to a polynomial oracle algorithm is that \(R\) can be exponentially large. We can avoid constructing the cumulative vector.
Write the masses in their ordinary binary rational encoding as \(\lambda_t=a_t/b_t\). Define
\(D=\prod_{t=1}^{\tau}b_t,\qquad A_t=a_t(D/b_t).\)
Then every \(A_t\) is a positive integer, and \(\sum_t A_t=D\). Moreover, the bit length of \(D\) is \(O(L)\). Finite binary fractions are covered by this construction.
For a world \(w\), define its integer rank histogram by
\(H_w(r)=\sum_{t:\ell_t(w)=r}A_t,\qquad 1\le r\le R.\)
It satisfies
\(D F_w(j)=\sum_{r=1}^{j}H_w(r),\qquad \sum_{r=1}^{R}H_w(r)=D.\)
Suppose two histograms first differ at rank \(r\). Their cumulative sums agree before \(r\), and their difference at \(r\) is exactly the difference between their histogram entries at \(r\).
That first differing rank cannot be \(R\): equality at every earlier rank, together with equal total mass \(D\), forces equality at \(R\).
Therefore lexicographic comparison of the cumulative vectors is exactly lexicographic comparison of the full histograms
\((H_w(1),\ldots,H_w(R)).\)
This also preserves ties. When \(R=1\), all histograms equal \((D)\), as required by the empty-vector rule.
Each histogram has at most \(\tau\) positive entries. List them as
\((r_1,h_1),\ldots,(r_k,h_k),\qquad r_1<\cdots<r_k,\qquad k\le\tau.\)
Pad this list to length \(\tau\) using \((R+1,0)\). Encode the list by the coordinate sequence
\(E(w)=(R+1-r_1,h_1,\ldots,R+1-r_\tau,h_\tau).\)
To verify its ordering, consider the first pair where two padded lists differ.
Thus lexicographic maximization of \(E(w)\) selects exactly the worlds prescribed in the question.
Use a fixed width \(b=\lceil\log_2(R+1)\rceil\) for each rank coordinate and a fixed width \(B=\lceil\log_2(D+1)\rceil\) for each mass coordinate. Concatenating their unsigned binary representations gives a bit string of length
\(s=\tau(b+B)=O\!\left(\tau(L+\log(R+1))\right).\)
Because all coordinate widths are fixed, lexicographic comparison of these bit strings preserves the coordinate ordering.
Sorting the supplied ranks, grouping equal ranks, and adding the corresponding integers computes \(E(w)\) in polynomial time.
Find the lexicographically maximum feasible encoding one bit at a time.
Suppose the already chosen prefix is \(p\). Ask the following \(\mathrm{NP}\) question:
“Does there exist \(w\models\kappa\) whose encoding \(E(w)\) begins with \(p1\)?”
A witness is a world assignment. Verification evaluates \(\kappa\), the rank circuits, and the polynomial-time encoding procedure.
Choose the next bit to be \(1\) precisely when the answer is yes. Otherwise choose \(0\). The invariant that the chosen prefix has a feasible extension holds initially because \(\kappa\) is satisfiable, and is preserved at every step. After \(s\) queries, the resulting string \(e^\star\) is the maximum feasible encoding.
Finally ask whether there exists a world satisfying
\(w\models\kappa\land\neg\psi,\qquad E(w)=e^\star.\)
This is another \(\mathrm{NP}\) query. Answering its negation decides the requested universal entailment, because equality with \(e^\star\) characterizes all selected worlds.
The algorithm uses at most
\(O\!\left(\tau(L+\log(R+1))\right)+1\)
adaptive \(\mathrm{NP}\)-oracle queries and polynomial additional work. Hence the problem belongs to \(\mathrm{P}^{\mathrm{NP}}\).
For complexity measured solely by \(L\), unused atoms can be ignored: only atoms occurring in \(\kappa,\psi\), or the rank circuits affect the decision. Their number is bounded by the ordinary explicit input length.
We give a direct reduction from an arbitrary language \(A\in\mathrm{P}^{\mathrm{NP}}\).
Fix a deterministic polynomial-time machine \(M\) deciding \(A\) with a satisfiability oracle. On input \(x\), choose a polynomial bound \(q=q(|x|)\ge1\) on its number of queries.
Pad computations to exactly \(q\) queries by asking a fixed unsatisfiable formula after the original computation halts, while preserving its output.
Introduce answer atoms \(a_1,\ldots,a_q\). Given a hypothetical answer sequence \(a\), simulate \(M(x)\) using those answers. This defines polynomial-time functions:
For each query introduce a polynomial-length certificate block \(u_i\). Let \(V_i(x,a_1,\ldots,a_{i-1},u_i)\) verify that \(u_i\) satisfies the query formula \(Q_i\).
Construct a Boolean circuit expressing
\(C_x(a,u,z)= \left(\bigwedge_{i=1}^{q}(\neg a_i\lor V_i(x,a_1,\ldots,a_{i-1},u_i))\right) \land \left(z\leftrightarrow O(x,a_1,\ldots,a_q)\right).\)
All these circuits have polynomial size: the machine and verifier have fixed polynomial running-time bounds, and their bounded computations can be unrolled into Boolean circuits.
Convert \(C_x\) into a propositional formula \(\kappa_x\) by introducing a variable for each gate, imposing its defining equivalence, and requiring the output gate to be true. Thus an assignment to \(a,u,z\) extends to a model of \(\kappa_x\) exactly when it satisfies \(C_x\).
The formula \(\kappa_x\) is satisfiable: take every \(a_i=0\), arbitrary certificates, and \(z=O(x,0,\ldots,0)\). Every certificate implication then holds.
Let \(a^\star\) be the lexicographically maximum answer sequence extendible to a model of \(\kappa_x\). We prove inductively that it equals the actual oracle transcript.
Assume its first \(i-1\) answers are correct. The circuit \(Q_i\) therefore describes the actual next query.
If this query is unsatisfiable, no certificate \(u_i\) makes \(V_i\) true. Hence every feasible extension of this prefix has \(a_i=0\).
If this query is satisfiable, choose a satisfying certificate and set \(a_i=1\). The earlier positive answers also have certificates, since they are actual positive oracle answers. Set every later answer to \(0\), so that all later certificate implications hold automatically, and choose \(z\) according to \(O\). This produces a feasible extension with \(a_i=1\). Lexicographic maximality therefore forces \(a_i^\star=1\).
This proves the induction. Every model with answer sequence \(a^\star\) consequently has \(z=1\) exactly when \(M\) accepts \(x\).
Create \(q\) types, one for each answer atom. Type \(i\) has the singleton-stratum base \(\{a_i\}\), mass
\(\lambda_i=2^{-i},\)
and ranks
\(\ell_i(w)=1\) if \(a_i=1\), and \(\ell_i(w)=2\) otherwise.
Add one type with the singleton-stratum base \(\{\top\}\), constant rank \(1\), and mass
\(\lambda_0=2^{-q}.\)
All masses are positive dyadic rationals, and
\(\lambda_0+\sum_{i=1}^{q}\lambda_i=2^{-q}+(1-2^{-q})=1.\)
Each answer type has both rank classes nonempty over all worlds, since its answer atom can independently be true or false before imposing \(\kappa_x\). The additional type has exactly one nonempty class. Therefore all offline rank promises hold, and \(R=2\).
There is only one cumulative coordinate:
\(F_w(1)=2^{-q}+\sum_{i=1}^{q}2^{-i}a_i.\)
This strictly orders answer sequences lexicographically. Indeed, if two sequences first differ at position \(i\), with the first having \(1\), their score difference is at least
\(2^{-i}-\sum_{j=i+1}^{q}2^{-j}=2^{-q}>0.\)
Consequently, the selected worlds are exactly the models of \(\kappa_x\) with answer sequence \(a^\star\).
Set \(\psi=z\). Every selected world satisfies \(\psi\) exactly when \(M\) accepts \(x\), equivalently when \(x\in A\).
The construction has polynomial size, including all \(q+1\) binary-encoded masses. This proves \(\mathrm{P}^{\mathrm{NP}}\)-hardness under polynomial-time many-one reductions, and completes the classification.
An unconditional deterministic algorithm enumerates all \(2^m\) worlds, computes their sparse encodings, and maintains the best encoding together with whether any tied world falsifies \(\psi\).
Using elementary integer arithmetic, one valid bit-operation bound is
\(O\!\left( \tau L^2+ 2^m\left[m+L+\tau L+ \tau\log_2(\tau+1)\lceil\log_2(R+1)\rceil\right] \right).\)
The preprocessing term covers conversion to common-denominator integer masses. Per world, the remaining terms cover formula and circuit evaluation, sorting ranks, grouping masses, and comparing encodings.
The oracle algorithm instead takes polynomial time in \(m,\tau,L,\log(R+1)\), with \(O(\tau(L+\log(R+1)))\) adaptive \(\mathrm{NP}\)-oracle calls.
The hardness construction also explains why the [multiset result quoted in the question](https://aaai.org/Papers/AAAI/2006/AAAI06-045.pdf) does not yield the same upper bound here. Realizing its dyadic masses as equal-mass individuals requires a population size divisible by \(2^q\), because one mass is \(2^{-q}\). The rational support representation has polynomial size, whereas that explicit expansion has exponential size in \(q\).
⟨structured verdict parsed — rendered above⟩
The argument is correct. It establishes \(\mathrm{P}^{\mathrm{NP}}\)-completeness under polynomial-time many-one reductions for the promised rational-mass input model, and therefore resolves the requested polynomial-time-versus-hardness question. I found no major or minor gaps requiring repair.
The freshness of \(s,y\) ensures that \(\kappa=s\land y\) is satisfiable independently of \(\varphi\). Both offline rank classes are nonempty: \(s=0\) guarantees \(g\), and \(s=1,y=0\) guarantees \(\neg g\). Thus the reduction satisfies the consecutive, nonempty-rank promise even when \(\varphi\) is unsatisfiable.
On feasible worlds, \(g\) and \(\varphi\) agree. If \(\varphi\) is satisfiable, the maximum cumulative score is \(1\), and precisely the feasible worlds satisfying \(\varphi\) attain it. If \(\varphi\) is unsatisfiable, all feasible worlds have score \(0\) and falsify \(\psi=\varphi\). Consequently, the answer is yes exactly for satisfiable \(\varphi\).
The construction has polynomial size. A singleton-stratum base distinguishes satisfying from falsifying worlds as asserted. This reduction independently settles the requested \(\mathrm{NP}\)-hardness conclusion.
With explicitly binary-encoded numerators and denominators, the product \(D=\prod_t b_t\) has bit length bounded by the sum of the denominator bit lengths, hence by \(O(L)\). Each \(A_t=a_t(D/b_t)\) is a positive integer. The mass-normalization promise gives \(\sum_t A_t=D\), so every histogram entry is at most \(D\).
No enumeration of an expanded population is required. The arithmetic produces integers of polynomial bit length.
If two histograms first differ at rank \(r\), their cumulative sums agree before \(r\) and differ at \(r\) with the same sign as their histogram entries.
The argument correctly excludes \(r=R\): equality at all earlier ranks and equality of total mass force equality at the final rank. Thus every genuine first difference occurs in a coordinate included in the original objective.
Ties are preserved. For \(R=1\), every histogram is \((D)\), so all feasible worlds tie, exactly as the empty-vector convention requires.
Each histogram has at most \(\tau\) positive entries because each type contributes at one rank. Grouping equal ranks therefore gives the stated sparse representation.
At the first unequal pair of two padded lists, all preceding rank–mass pairs coincide. If the ranks differ, the smaller rank has positive mass where the other histogram has zero; it therefore wins the histogram comparison. Reversing the rank coordinate to \(R+1-r_i\) correctly makes this preference a maximization. If the ranks agree, the larger mass wins in both representations.
Padding with \((R+1,0)\) introduces no false distinction. The fixed-width binary encoding also preserves the coordinate order. The widths are sufficient: rank coordinates lie between \(0\) and \(R\), and mass coordinates lie between \(0\) and \(D\).
The resulting length \(\tau(b+B)=O(\tau(L+\log(R+1)))\) is polynomial in the stated parameters. Its computation uses only circuit evaluation, sorting, and polynomial-bit integer arithmetic.
Each prefix-extension query has a polynomially verifiable witness: a world assignment satisfying \(\kappa\) whose computed encoding has the requested prefix.
The satisfiability promise supplies the initial feasible extension. At each step, choosing \(1\) when possible and \(0\) otherwise preserves feasibility and maximizes the next bit. After all bits are fixed, the resulting string is therefore the maximum feasible encoding.
The final query checks for a feasible world with that encoding that falsifies \(\psi\). Negating its answer correctly implements universal entailment over every selected world, including ties.
The query count and polynomial additional work follow from the encoding length. The observation about unused atoms also justifies membership measured by \(L\), even if the ambient language names more atoms than occur in the relevant formulas and circuits.
The hardness construction handles adaptivity correctly: query \(i\) depends only on the preceding hypothetical answers. Polynomial bounds on the oracle machine and query lengths permit polynomial-length certificate blocks and polynomial-size circuits.
The constraints require certificates for positive answers while permitting unsupported negative answers. That asymmetry is intentional and is subsequently resolved by lexicographic maximization.
Introducing gate variables with defining equivalences preserves exactly the satisfying assignments projected onto \(a,u,z\). The all-zero answer sequence makes every certificate implication true, establishing the required satisfiability promise.
The induction is valid. Under a correct preceding prefix, an unsatisfiable next query prohibits a positive answer. A satisfiable next query permits a positive answer with a certificate; certificates for earlier positive answers exist by the induction hypothesis.
Setting later answers to zero removes all later certificate obligations, and the output constraint can be satisfied by choosing the computed output bit. Thus a feasible extension with the next answer equal to one exists whenever the actual oracle answer is positive.
Lexicographic maximality consequently forces every answer bit to match the actual oracle transcript. Every feasible model with that transcript has the correct acceptance bit \(z\).
All masses are positive, and the normalization calculation is correct:
\[
2^{-q}+\sum_{i=1}^{q}2^{-i}=1.
\]
Each answer type has two nonempty offline classes; the constant type has one. The description therefore determines rank bounds \(2\) and \(1\), respectively, and global maximum rank \(R=2\).
The dominance calculation is also correct:
\[
2^{-i}-\sum_{j=i+1}^{q}2^{-j}=2^{-q}>0.
\]
Hence the score strictly orders distinct answer sequences lexicographically. Worlds sharing an answer sequence tie, as required.
With \(\psi=z\), universal entailment over selected worlds is equivalent to acceptance by the oracle machine. The formulas, circuits, atoms, and binary-encoded masses all have polynomial total size. This establishes the claimed polynomial-time many-one hardness for every language in \(\mathrm{P}^{\mathrm{NP}}\).
The enumeration bound accounts for common-denominator preprocessing, world assignments, formula and circuit evaluation, rank sorting, mass grouping, and encoding comparison. Integer lengths are \(O(L)\), and the supplied rank bounds ensure \(\log(R+1)=O(L)\), so the displayed terms cover these operations.
For fixed \(m\), the factor \(2^m\) is constant, yielding polynomial time in the remaining input size. The oracle algorithm has the stated polynomial resource bounds.
The multiset comparison is appropriately limited to representation size: an equal-mass realization of a type of mass \(2^{-q}\) requires population size divisible by \(2^q\). This explains why explicit expansion is not a polynomial-size transfer of the multiset upper bound. The proof does not rely on the cited multiset theorem.
No additional clarification is needed to verify the conclusion.
⟨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.