Answer: \(\mathrm{NP}\text{-hard}\)
Theorem 6 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateLet B be a bargaining game and ϕ a formula. Deciding whether A(B) ⊢ϕ is ΠP 2 -hard.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite support of bargaining-game types \(B_t\), binary-rational masses \(\mu_t\) summing to \(1\), a common formula \(\varphi\), and a threshold \(q\), compute or decide whether \(\sum_{t:A(B_t)\vdash\varphi}\mu_t\ge q\).
A society is given by its support: a list of \(\tau\) bargaining-game types \(B_t\) with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. All formulas use classical propositional logic over \(m\) atoms; \(L\) is the total input bit length.
Each type has two finite, individually consistent demand sets \(X_i\), explicitly partitioned into priority levels \(X_i^1,\ldots,X_i^{r_i}\), highest first. Equal-level demands are tied. Writing \(\operatorname{rank}_i(\psi)\) for a demand's level, require \(\operatorname{rank}_i(\psi)\le\max_{\theta\in Y}\operatorname{rank}_i(\theta)\) whenever \(\varnothing\ne Y\subseteq X_i\), \(\psi\in X_i\), and \(Y\vdash\psi\). Empty demand sets have \(r_i=0\).
Write \(X_i^{\le k}=\bigcup_{j=1}^kX_i^j\) and \(D_{-i}=D_{3-i}\). A deal is a pair \(D_i\subseteq X_i\) with consistent union such that, for each \(i,k\), \(D_i\cap X_i^k\) is inclusion-maximal among \(Z\subseteq X_i^k\) making \((D_i\cap X_i^{\le k-1})\cup Z\cup D_{-i}\) consistent. Let \(\Omega(B)\) contain all deals.
Define \(\rho_i(D_i)=\max\{k\in\{0,\ldots,r_i\}:X_i^{\le k}\subseteq D_i\}\), \(\rho_B=\max_{D\in\Omega(B)}\min_i\rho_i(D_i)\), \(\gamma(B)=\{D\in\Omega(B):\min_i\rho_i(D_i)=\rho_B\}\), and \(\Phi_i=\bigcap_{D\in\gamma(B)}D_i\).
For consistent \(F\), let \(\mathcal H_i(F)\) contain the subsets \(H\subseteq X_i\) such that each \(H\cap X_i^k\) is inclusion-maximal among \(Z\subseteq X_i^k\) making \((H\cap X_i^{\le k-1})\cup Z\cup F\) consistent. Define \(X_i\otimes_i F=\bigcap_{H\in\mathcal H_i(F)}\operatorname{Cn}(H\cup F)\) and \(A(B)=(X_1\otimes_1\Phi_2)\cap(X_2\otimes_2\Phi_1)\).
Given a common formula \(\varphi\) and binary-rational \(q\in[0,1]\), apply this rule independently to each type and decide whether \(\sum_{t:A(B_t)\vdash\varphi}\mu_t\ge q\).
Is this threshold decision problem solvable in polynomial time in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
The discrete single-game inference result is reported as \(\Pi_2^P\)-hard, but its displayed proof conflicts with the individually consistent demand-set domain ([original source](https://cdn.aaai.org/AAAI/2006/AAAI06-116.pdf)).
Later work retains individual consistency but changes the bargaining solution ([later source](https://arxiv.org/pdf/1405.5201)); no result for this exact distributional threshold problem was located.
Result
The threshold decision problem is \(\mathrm{NP}\)-hard under polynomial-time many-one reductions, even with one support type, two singleton demand sets, and an atomic query. Consequently, a polynomial-time algorithm in \(m,\tau,L\) would imply \(\mathrm{P}=\mathrm{NP}\).
The proof below uses the stated definitions directly and does not rely on the reported hardness argument in Theorem 6 of the [original source](https://cdn.aaai.org/AAAI/2006/AAAI06-116.pdf).
Reduction and admissibility
Let \(f\) be an arbitrary instance of propositional SAT. Introduce an atom \(p\) absent from \(f\), and write \(g=(p\to f)\).
Construct a society with \(\tau=1\), mass \(\mu_1=1\), and threshold \(q=1\). Its only game \(B_f\) has demand sets
\(X_1=X_1^1=\{p\},\qquad X_2=X_2^1=\{g\}.\)
Set the query to \(\varphi=p\).
Both demand sets are individually consistent, regardless of whether \(f\) is satisfiable: \(p\) has a satisfying valuation, and every valuation assigning \(p\) false satisfies \(g\). The priority condition also holds: each demand has rank \(1\), so every required rank inequality is \(1\le 1\).
The construction has polynomial size and uses only one additional atom. We prove that its threshold answer is yes exactly when \(f\) is satisfiable.
Case 1: \(f\) is satisfiable
A satisfying valuation of \(f\), extended by assigning \(p\) true, satisfies \(X_1\cup X_2\).
For any candidate deal, adding either player’s sole demand preserves consistency, because the resulting union is a subset of the consistent set \(X_1\cup X_2\). Thus inclusion-maximality forces both demands to be retained. Consequently,
\(\Omega(B_f)=\{(\{p\},\{g\})\}.\)
Both coverage values are \(1\), so this deal is also the unique member of \(\gamma(B_f)\). Hence
\(\Phi_1=\{p\},\qquad \Phi_2=\{g\}.\)
Because \(\{p,g\}\) is consistent, the unique maximal revision subset for either player is its entire demand set:
\(\mathcal H_1(\Phi_2)=\{\{p\}\},\qquad \mathcal H_2(\Phi_1)=\{\{g\}\}.\)
Therefore,
\(A(B_f)=\operatorname{Cn}(\{p,g\})\cap\operatorname{Cn}(\{p,g\})=\operatorname{Cn}(\{p,g\}).\)
In particular, \(A(B_f)\vdash p\).
Case 2: \(f\) is unsatisfiable
Now \(g=(p\to f)\) is logically equivalent to \(\neg p\). Thus the pair retaining both demands is inconsistent.
The pair retaining neither demand is not a deal: with the other player’s component empty, either player can consistently add its sole demand.
The remaining two pairs are precisely the deals:
\(\Omega(B_f)=\{(\{p\},\varnothing),(\varnothing,\{g\})\}.\)
Indeed, in each pair the retained singleton is consistent and maximal; adding the omitted demand would produce the inconsistent set \(\{p,g\}\).
Their coverage pairs are respectively \((1,0)\) and \((0,1)\). Therefore \(\rho_{B_f}=0\), both deals belong to \(\gamma(B_f)\), and
\(\Phi_1=\Phi_2=\varnothing.\)
Since each original demand set is individually consistent, revision by the empty set retains its entire singleton uniquely. Hence
\(A(B_f)=\operatorname{Cn}(\{p\})\cap\operatorname{Cn}(\{g\})=\operatorname{Cn}(\{p\})\cap\operatorname{Cn}(\{\neg p\}).\)
This intersection is exactly the set of tautologies. To verify this, any formula belonging to both theories holds under every valuation assigning \(p\) true and under every valuation assigning \(p\) false. These two classes exhaust all valuations. Conversely, every tautology belongs to both theories.
Thus \(A(B_f)=\operatorname{Cn}(\varnothing)\), which does not entail the non-tautological atom \(p\).
Threshold equivalence and conclusion
There is only one type, with mass \(1\). The preceding case analysis therefore gives
\(\displaystyle \sum_{t:A(B_t)\vdash p}\mu_t=\begin{cases}1,&f\text{ is satisfiable},\\0,&f\text{ is unsatisfiable}.\end{cases}\)
With \(q=1\), the threshold answer is yes if and only if \(f\) is satisfiable. This is a polynomial-time many-one reduction from SAT whose outputs satisfy every promised demand-set and priority condition. Since SAT is \(\mathrm{NP}\)-complete, the stated threshold problem is \(\mathrm{NP}\)-hard.
⟨structured verdict parsed — rendered above⟩
The proof is correct and resolves the assigned question: the threshold problem is \(\mathrm{NP}\)-hard, even with a single support type. No mathematical gaps or false statements were found.
Given a SAT instance \(f\), introducing a fresh atom \(p\) and forming \(g=(p\to f)\) takes polynomial time and increases formula size only linearly. The parameters \(\tau=1\), \(\mu_1=1\), and \(q=1\) satisfy the support, mass, and threshold requirements. The query \(p\) is atomic. The reduction does not need to determine whether \(f\) is satisfiable when constructing the instance.
The singleton \(\{p\}\) is consistent. The singleton \(\{g\}\) is consistent because assigning \(p\) false satisfies \(g\), independently of \(f\). For each player, the only nonempty subset of its demand set is the singleton itself, and its only demand has rank \(1\). Every required rank inequality is therefore \(1\le 1\). This verifies all promised input conditions.
Freshness of \(p\) permits extending a satisfying valuation of \(f\) with \(p\) true, establishing consistency of \(\{p,g\}\). Every possible component union, including one obtained by adding an omitted demand, is a subset of this consistent set. Thus an empty component cannot satisfy inclusion-maximality at its sole priority level. Both singleton components must be retained, and their pair satisfies the deal definition. Consequently, the asserted singleton description of \(\Omega(B_f)\) is exact.
The unique deal has coverage values \((1,1)\), so \(\rho_{B_f}=1\) and it is the unique selected deal. The claimed values of \(\Phi_1\) and \(\Phi_2\) follow directly. For either revision, the entire singleton demand set is consistent with the other player’s core, and the empty subset is not maximal. Hence each revision family has exactly the stated member. It follows that \(A(B_f)=\operatorname{Cn}(\{p,g\})\), which entails \(p\).
Unsatisfiability of \(f\) makes \(g\) logically equivalent to \(\neg p\). Of the four possible component pairs, the pair retaining both demands is inconsistent, and the pair retaining neither fails maximality. In each remaining pair, the retained singleton is consistent and maximal, while adding the omitted singleton is inconsistent. The enumeration of \(\Omega(B_f)\) is therefore exhaustive and correct.
The two deals have coverage pairs \((1,0)\) and \((0,1)\). Both attain the maximum minimum coverage, namely \(0\), so both belong to \(\gamma(B_f)\). Their componentwise intersections are empty. Revision by the empty set uniquely retains each individually consistent singleton, giving the stated intersection of consequence theories.
The calculation
\(\operatorname{Cn}(\{p\})\cap\operatorname{Cn}(\{\neg p\})=\operatorname{Cn}(\varnothing)\)
is correct over the full propositional language. Every valuation assigns \(p\) either true or false, so a formula entailed by both singletons holds under every valuation. Conversely, every tautology belongs to both theories. Thus the resulting set does not entail \(p\); a valuation assigning \(p\) false satisfies every tautology.
With one type of mass \(1\), the threshold sum is exactly \(1\) in the satisfiable case and \(0\) in the unsatisfiable case. Threshold \(q=1\) therefore preserves yes and no answers. Together with polynomial construction size and admissibility, this establishes a polynomial-time many-one reduction from SAT. The standard NP-completeness of propositional SAT yields the claimed NP-hardness and the stated consequence for a polynomial-time algorithm.
The argument uses the supplied definitions directly. It does not depend on either cited bargaining-game result. 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.