Answer: \(\mathrm{NP}\text{-hard}\), even when \(\tau=\ell=1\) and \(a=\lambda_1=1/2\); therefore not polynomial-time solvable unless \(\mathrm{P}=\mathrm{NP}\).
Corollary 2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet Δ = Δmax or ΔΣ, and ak−1<a≤ak. Then MERGE(BE,μ,Δ) is in k·Θp 2, where Θp 2 is the class of all languages that can be recognized in polynomial time by a deterministic Turing machine using a number of calls to an NP oracle bounded by a logarithmic function of the size of the input data.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Input a finite propositional vocabulary \(P\), integrity constraint κ, query \((\phi,a)\), and a support \(T\) of complete, consistent possibilistic knowledge bases \(B_t\) with rational masses ρ_t>0 and \(\sum_{t\in T}\rho_t=1\). For each priority level λ_r, let \(K_t^r\) be the formulas of type \(t\) at that level, set \(S_1=\operatorname{Mod}(\kappa)\), and define \(S_{r+1}=\arg\min_{\omega\in S_r}\sum_{t\in T}\rho_t d_H(\omega,K_t^r)\), with an empty stratum contributing zero. Construct the possibility distribution as in Algorithm 1, then decide whether its canonical possibilistic base entails \((\phi,a)\) under Definition 3, including the maximality condition.
Input a finite propositional vocabulary \(P\), with \(m=|P|\), a satisfiable integrity constraint \(\kappa\), and a query \((\phi,a)\), where \(a\in\mathbb{Q}\cap(0,1]\). Formulas are given explicitly in ordinary propositional syntax.
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational \(\rho_t>0\), with \(\sum_t\rho_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type is a finite possibilistic base \(B_t\) of pairs \((\psi,w)\), with binary rational \(w\in(0,1]\); its underlying classical base is consistent and complete, hence has exactly one model. Individual priority strata need not be complete.
Let \(\lambda_1>\cdots>\lambda_\ell>0\) be all distinct input weights and \(K_t^r=\{\psi:(\psi,\lambda_r)\in B_t\}\). Define \(d_H(\omega,K)=\min_{\nu\models\bigwedge K}d_H(\omega,\nu)\), using Hamming distance; an empty stratum has distance zero.
Set \(S_1=\operatorname{Mod}(\kappa)\) and \(S_{r+1}=\arg\min_{\omega\in S_r}\sum_t\rho_t d_H(\omega,K_t^r)\) for \(1\le r\le\ell\), retaining all minimizers.
Define \(\pi(\omega)=0\) outside \(S_1\), \(\pi(\omega)=1-\lambda_r\) on \(S_r\setminus S_{r+1}\), and \(\pi(\omega)=1\) on \(S_{\ell+1}\).
For a set of interpretations \(M\), let \(\operatorname{form}(M)\) denote any formula with model set \(M\). Define the canonical base implicitly by \(C_\pi=\{(\operatorname{form}(\{\omega:\pi(\omega)>c\}),1-c):c\in\pi(\{0,1\}^{P}),\ c<1\}\).
For \(b\in(0,1]\), let \((C_\pi)_{\ge b}\) contain the unweighted formulas whose weights are at least \(b\). The decision question is whether this cut at \(a\) is consistent and entails \(\phi\), while \((C_\pi)_{\ge b}\not\vdash\phi\) for every \(b\in(a,1]\).
Is this decision problem solvable in polynomial time, or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,\ell\) and the total binary input length \(L\).
For discrete iterated Hamming-sum merging, an upper bound of \(k\) calls to a \(\Theta_2^p\) procedure is reported, where \(k\) counts the relevant priority levels; this is an oracle bound, not a polynomial-time algorithm. [Source](https://cdn.aaai.org/AAAI/2007/AAAI07-074.pdf)
No result settling exactly the rational-mass, complete-type problem specified here was located in the literature search.
The decision problem is \(\mathrm{NP}\)-hard under polynomial-time many-one reductions, even when \(\tau=\ell=1\), the sole mass is \(1\), the sole weight and query threshold are both \(1/2\), and the query is an atom. Thus a polynomial-time algorithm in the total binary input length \(L\) would imply \(\mathrm{P}=\mathrm{NP}\).
A deterministic upper bound is \(2^m\operatorname{poly}(L)\). More explicitly, the enumeration algorithm below uses \(O(2^m[L+\tau\ell(m+1)])\) elementary evaluation, graph, and arithmetic operations, plus polynomial preprocessing; its arithmetic operands have polynomial bit length. The problem also belongs to \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\).
Write \(\Omega=\{0,1\}^{P}\). Every stratum is consistent: the unique model of the underlying complete base of type \(t\) satisfies every subset of that base. Hence every distance in the definition is finite. Since \(\kappa\) is satisfiable, minimization over finite nonempty sets shows that every \(S_r\) is nonempty.
For \(b\in(0,1]\), define \(r(b)=|\{j:\lambda_j\ge b\}|\). We claim that
\(\operatorname{Mod}((C_\pi)_{\ge b})=\{\omega:\pi(\omega)>1-b\}=S_{r(b)+1}.\)
To prove the first equality, the formulas in this cut are precisely those associated with realized values \(c\le 1-b\). An interpretation satisfying \(\pi(\omega)>1-b\) satisfies every such formula. Conversely, if \(\pi(\omega)\le 1-b\), its own realized value \(c=\pi(\omega)<1\) contributes a formula to the cut, and \(\omega\) fails that formula.
For the second equality, interpretations outside \(S_1\) have possibility \(0\), so they fail the strict inequality. An interpretation removed at level \(j\) has possibility \(1-\lambda_j\), and therefore satisfies the inequality exactly when \(\lambda_j<b\). Final survivors have possibility \(1\). This gives precisely \(S_{r(b)+1}\).
In particular, every cut under consideration is consistent.
For completeness, this also removes the universal quantification over larger thresholds:
\(S_{j+1}\subseteq\operatorname{Mod}(\phi)\) and \(S_j\not\subseteq\operatorname{Mod}(\phi)\).
For the last assertion, a threshold immediately above \(\lambda_j\) has model set \(S_j\). Every other larger threshold has a model set containing \(S_j\), so a countermodel in \(S_j\) witnesses failure of entailment at all larger thresholds.
We reduce propositional satisfiability to the specified decision problem.
Let \(F\) be a propositional formula on variables \(x_1,\ldots,x_n\), with \(n\ge1\). Restricting satisfiability to this case preserves its \(\mathrm{NP}\)-hardness; an unused variable can be added if necessary.
Introduce fresh variables \(q,z_1,\ldots,z_{n+2}\), and set
\(P=\{x_1,\ldots,x_n,q,z_1,\ldots,z_{n+2}\}.\)
Define
\(A=q\land F\land\bigwedge_{i=1}^{n+2}\neg z_i,\)
\(E=\neg q\land\bigwedge_{i=1}^{n}\neg x_i\land\bigwedge_{i=1}^{n+2}z_i,\)
and \(\kappa=A\lor E\).
The formula \(E\) has exactly one model, denoted \(\eta\). Consequently, \(\kappa\) is satisfiable regardless of whether \(F\) is satisfiable.
There is one type, with mass \(\rho_1=1\), and base
\(B_1=\{(\neg p,1/2):p\in P\}.\)
Its underlying classical base has exactly one model, the all-zero interpretation \(\mathbf{0}\). Thus this base is consistent and complete, as required. There is exactly one priority level, \(\lambda_1=1/2\).
Choose the query \((\phi,a)=(q,1/2)\).
The construction uses \(m=2n+3\) variables and polynomial binary encoding length. All formulas are explicit ordinary propositional formulas.
The sole stratum has model set \(\{\mathbf{0}\}\). Therefore its objective is
\(d_H(\omega,K_1^1)=d_H(\omega,\mathbf{0}),\)
the number of true variables in \(\omega\).
The fallback model \(\eta\) has precisely the \(n+2\) variables \(z_i\) true. Hence
\(d_H(\eta,\mathbf{0})=n+2.\)
Every model \(\omega\) of \(A\) has \(q\) true, all \(z_i\) false, and at most \(n\) true variables among the \(x_i\). Therefore
\(d_H(\omega,\mathbf{0})\le n+1<n+2.\)
It follows that:
By Section 1,
\(\operatorname{Mod}((C_\pi)_{\ge 1/2})=S_2.\)
This cut is consistent and entails \(q\) exactly when \(F\) is satisfiable.
For every \(b\in(1/2,1]\), no priority weight is at least \(b\), so
\(\operatorname{Mod}((C_\pi)_{\ge b})=S_1=\operatorname{Mod}(\kappa).\)
The fallback model \(\eta\) belongs to \(S_1\) and falsifies \(q\). Therefore none of these larger cuts entails \(q\), independently of the satisfiability of \(F\).
We have proved the exact equivalence
\(F\text{ is satisfiable}\quad\Longleftrightarrow\quad\text{the constructed query is accepted}.\)
This proves \(\mathrm{NP}\)-hardness, including the required failure of entailment at every larger threshold.
The following algorithm works for the general promised input and never constructs formulas representing survivor sets.
Let \(k=|\{r:\lambda_r\ge a\}|\le\ell\). Section 1 shows that only these \(k\) levels can matter.
Write each mass as \(\rho_t=u_t/v_t\), and let
\(D=\prod_{t=1}^{\tau}v_t,\qquad c_t=u_t(D/v_t).\)
Then every \(c_t\) is a positive integer and \(\sum_t c_t=D\). Multiplying an objective by \(D\) preserves its minimizers, so use the integer scores
\(F_r(\omega)=\sum_{t=1}^{\tau}c_t\,d_H(\omega,K_t^r).\)
They satisfy \(0\le F_r(\omega)\le mD\). The binary length of \(D\) is at most the sum of the denominator lengths, hence \(O(L)\). All scores consequently have \(O(L+\log(m+1))\) bits.
Enumerate the \(2^m\) interpretations. For each relevant nonempty stratum, evaluate its formulas to identify its models.
Consider the graph whose vertices are interpretations and whose edges join interpretations differing in one variable. Its graph distance equals Hamming distance: every differing coordinate must be changed, and changing each such coordinate once gives a path of that length.
A breadth-first search initialized at all models of a stratum therefore computes its distance from every interpretation. Each search costs \(O((m+1)2^m)\) graph operations. Empty strata contribute distance zero directly.
The combined formula-evaluation cost is \(O(L2^m)\), because each input formula belongs to just one stratum of one type.
Initialize the survivor mask with the models of \(\kappa\). At each relevant level, accumulate the integer scores, find their minimum among current survivors, and retain every interpretation attaining it. Finally, apply the entailment and countermodel tests from Section 1.
The resulting operation count, including evaluation of \(\kappa\) and \(\phi\), is
\(O(2^m[L+\tau k(m+1)]),\)
plus polynomial preprocessing. These are elementary evaluation, graph, and arithmetic operations on operands of polynomial bit length. Thus the deterministic bit running time is
\(2^m\operatorname{poly}(L+m+\tau+\ell)=2^m\operatorname{poly}(L),\)
where the last equality uses the explicit input encoding, under which \(m,\tau,\ell\) are bounded by a polynomial in \(L\). In particular, this is polynomial for fixed \(m\), but the hardness reduction already fixes \(\tau=\ell=1\).
A direct argument gives membership in \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\), also for binary rational masses.
Let \(h_j\) be the optimum integer score at level \(j\). Suppose \(h_1,\ldots,h_{r-1}\) are known. To test whether the next optimum is at most an integer \(u\), ask whether there exist:
such that
\(\sum_t c_t d_H(\omega,\nu_t^j)\le h_j\quad(j<r),\)
and
\(\sum_t c_t d_H(\omega,\nu_t^r)\le u.\)
This is an \(\mathrm{NP}\) predicate: the certificate has \(O(m\tau r)\) bits, and all formulas and binary inequalities can be checked in polynomial time.
For any fixed \(\omega\), each actual stratum distance is at most its witnessed distance. Conversely, witnesses attaining every actual distance exist and can be chosen independently. Therefore the existential inequalities are equivalent to the corresponding inequalities on actual scores.
Moreover, within \(\operatorname{Mod}(\kappa)\), the conditions \(F_j(\omega)\le h_j\) for all \(j<r\) characterize \(S_r\). This follows inductively because \(h_j\) is the minimum over \(S_j\): once earlier conditions hold, a score at most \(h_j\) must equal that minimum.
Binary search on \([0,mD]\) now computes each \(h_r\) with \(O(L+\log(m+1))\) oracle calls. Entailment and its required predecessor failure are checked with at most two further calls, adding \(\omega\models\neg\phi\) to the same certificate conditions. The total is
\(O(k[L+\log(m+1)]+1)\)
calls to an \(\mathrm{NP}\) oracle, with polynomial computation and query length.
The cited paper’s Proposition 11 and Corollary 2 likewise describe an oracle bound for its discrete setting, rather than an ordinary polynomial-time algorithm. Our hardness proof applies directly to the complete-type problem specified here. [Qi, *A Model-based Approach for Merging Prioritized Knowledge Bases in Possibilistic Logic*](https://cdn.aaai.org/AAAI/2007/AAAI07-074.pdf)
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned problem correctly. The reduction establishes \(\mathrm{NP}\)-hardness under all stated input promises, and both upper bounds are justified. I found no major or minor mathematical issues requiring repair.
Each stratum is a subset of its type’s consistent underlying base, so it has a model. Empty strata have distance zero by the task’s convention. Thus every objective is finite. Starting from the nonempty finite set \(\operatorname{Mod}(\kappa)\), each minimization retains a nonempty set. The asserted nonemptiness of every \(S_r\) is correct.
The cut contains exactly the canonical formulas indexed by realized possibility values \(c\le 1-b\). If \(\pi(\omega)>1-b\), then \(\omega\) satisfies every formula in that cut. If \(\pi(\omega)\le 1-b\), its own realized value indexes a cut formula that it falsifies; that value is strictly below \(1\), since \(b>0\).
The second equality also respects the strict boundary: an interpretation removed at level \(j\) satisfies \(\pi(\omega)>1-b\) exactly when \(\lambda_j<b\). Consequently,
\[
\operatorname{Mod}((C_\pi)_{\ge b})=S_{r(b)+1}.
\]
This remains valid when a removal layer is empty or the canonical cut has no formulas. Since the survivor set is nonempty, every relevant cut is consistent.
All three cases are correct:
Thus a countermodel in \(S_j\) witnesses nonentailment at every larger threshold. The stated equivalence with entailment on \(S_{j+1}\) and nonentailment on \(S_j\) follows.
The construction is polynomial in the explicit encoding length of \(F\). Its variable count is correctly computed as \(m=2n+3\).
The fallback formula \(E\) fixes every variable and has exactly one model \(\eta\). Hence \(\kappa=A\lor E\) is satisfiable for every source instance, including unsatisfiable \(F\).
The sole type contains one negative literal for every variable, all at weight \(1/2\). Its underlying classical base has the unique all-zero model, so it is consistent and complete. The construction correctly has \(\tau=\ell=1\), mass \(1\), and atomic query \(q\) at threshold \(1/2\). No input promise is violated.
The sole stratum has the all-zero interpretation as its unique model, so its distance is the number of true variables.
The fallback model has distance \(n+2\). Every model of \(A\) has distance at most \(n+1\): \(q\) is true, all auxiliary variables \(z_i\) are false, and at most \(n\) original variables are true. The strict separation is correct.
Therefore, when \(F\) is satisfiable, every minimizer satisfies \(A\) and hence \(q\). When \(F\) is unsatisfiable, the only integrity model is \(\eta\), which falsifies \(q\).
At threshold \(1/2\), the cut has model set \(S_2\). At every larger threshold it has model set \(S_1\), containing the countermodel \(\eta\). Thus the reduction verifies the entire acceptance condition, including its universal clause. This establishes the claimed polynomial-time many-one \(\mathrm{NP}\)-hardness.
The denominator product \(D\) has polynomial binary length because its logarithm is bounded by the sum of the input denominator lengths. Each \(c_t=u_t(D/v_t)\) is a positive integer, and \(\sum_t c_t=D\).
Scaling every objective by \(D\) preserves its minimizers. Since each distance lies between zero and \(m\), the integer scores lie between zero and \(mD\), with the asserted polynomial bit length. The argument does not confuse a potentially exponential numerical value with its binary encoding length.
Multi-source breadth-first search on the interpretation hypercube correctly computes distance to each stratum’s model set. The graph has \(2^m\) vertices and \(m2^{m-1}\) edges when \(m\ge1\), supporting the stated \(O((m+1)2^m)\) search bound.
Formula evaluation over all interpretations costs \(O(L2^m)\), because each input formula is evaluated within its assigned stratum. Score accumulation and survivor filtering fit within the additional stated bound. Empty strata require no search.
The operation count
\[
O\!\left(2^m[L+\tau k(m+1)]\right)
\]
is justified under the explicitly stated model of evaluation, graph, and arithmetic operations. Accounting for polynomial operand lengths gives the claimed deterministic bit-time bound \(2^m\operatorname{poly}(L)\), plus polynomial preprocessing. The output correctly distinguishes this from polynomial time in unrestricted \(L\).
The proposed certificates have polynomial length, and their formula satisfaction, Hamming distances, and binary inequalities are polynomially checkable.
The witness interpretation distances are upper bounds on the actual stratum distances. Conversely, distance-minimizing witnesses exist and can be chosen independently for each type and level. These facts justify the claimed equivalence between witnessed inequalities and actual score inequalities.
The induction characterizing \(S_r\) by the preceding optimum bounds is valid: after earlier bounds establish membership in \(S_j\), a score at most \(h_j\) must equal the minimum on that set.
Binary search over \([0,mD]\) uses the stated polynomial number of oracle calls. Adding the countermodel condition checks entailment and predecessor nonentailment through at most two additional calls. Thus membership in \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\) follows.
The paper’s Proposition 11 explicitly describes repeated calls to a merging procedure, and Corollary 2 reports the corresponding bound using a \(\Theta_2^p\) procedure. The prover’s characterization of this as an oracle bound is faithful to the source. Its proof for the specified rational-mass problem is independent of that citation. [Qi, *A Model-based Approach for Merging Prioritized Knowledge Bases in Possibilistic Logic*, p. 475](https://cdn.aaai.org/AAAI/2007/AAAI07-074.pdf)
The conclusion is appropriately qualified: \(\mathrm{NP}\)-hardness rules out a polynomial-time algorithm assuming \(\mathrm{P}\ne\mathrm{NP}\). No unsupported completeness claim is made.
No additional clarification or repair 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.