Answer: \(\mathrm{NP}\)-hard, already for \(\tau=1\) and \(K=2\), and also for \(\tau=2\) and \(K=3\) with no unconditional antecedents.
Proposition 9 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateDeciding whether there exists a confirmed deal based on a given set C of commitments is ΣP 2 -complete. It turns out that if the coalition partners have expressed consistent commitments, having a stable set is sufficient to obtain a confirmed deal.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finitely many types \(T\) with rational masses \(\mu_t>0\) summing to \(1\), integral local Boolean strategies, and finite commitment menus whose antecedents are rational-threshold predicates over type-level action shares, does there exist a positive-mass coalition allocation and a stable selection of commitments that forms a confirmed deal? The selected consequents must guarantee their antecedents, and each coalition member’s strategy must honor every commitment that could be triggered under every feasible action profile of the outsiders.
A society is given by its support: \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) counts listed types, not possible types. Type \(t\) has local Boolean variables \(\Phi_t\) and a satisfiable propositional constraint \(\delta_t\); its integral strategies are \(S_t=\{a\in\{0,1\}^{\Phi_t}:a\models\delta_t\}\). Let \(m=\sum_t|\Phi_t|\), \(K\) be the total number of menu entries, and \(L\) the total input bit length.
Each type has an explicitly listed commitment menu \(C_t\). An entry \(c\in C_t\) has an antecedent \(A_c\), a Boolean formula of rational-threshold comparisons \(h_{u,p}\ge q\), where \(u\ne t\), \(p\in\Phi_u\), and \(q\in[0,1]\); \(h_{u,p}\) is the fraction of the entire mass of type \(u\) setting \(p\) true. Its consequent \(B_c\) is a propositional formula over \(\Phi_t\), satisfiable together with \(\delta_t\). Every antecedent must hold in some feasible full profile; unconditional antecedents and tautological consequents are allowed. Menus need not be jointly consistent.
A feasible population profile distributes each type's mass arbitrarily over \(S_t\), using nonnegative real masses. A coalition allocation consists of nonnegative real masses \(x_{t,D,a}\), indexed by nonempty selections \(D\subseteq C_t\) and strategies \(a\in S_t\), with \(\sum_{D,a}x_{t,D,a}\le\mu_t\) and \(\sum_{t,D,a}x_{t,D,a}>0\). Write \(z_{t,D}=\sum_a x_{t,D,a}\); the remaining mass of each type consists of outsiders. Every occupied allocation cell must satisfy \(a\models\bigwedge_{c\in D}B_c\).
The selection is stable if it has a feasible coalition allocation satisfying its selected consequents and, for every redistribution of each fixed mass \(z_{t,D}\) among strategies satisfying those consequents and every feasible outsider profile, all \(A_c\) with \(z_{t,D}>0\) and \(c\in D\) hold. Shares are computed from coalition and outsider masses together, always divided by the original \(\mu_t\).
A confirmed deal additionally has a safely playable allocation \(x\): for every feasible outsider profile, every occupied cell \(x_{t,D,a}>0\), and every commitment \(c\in C_t\), \(A_c\) holding in the combined profile implies \(a\models B_c\). This includes commitments outside \(D\); if there are no outsiders, their unique profile is the empty allocation.
Is deciding whether such a confirmed deal exists solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), \(K\), and \(L\).
For finite agents with propositional commitments, confirmed-deal existence is \(\Sigma_2^{\mathrm P}\)-complete ([source](https://faculty.washington.edu/mdecock/papers/sdeclercq2016b.pdf)). No result settling this exact mass-allocation problem was located.
Confirmed-deal existence is \(\mathrm{NP}\)-hard, so it has no polynomial-time algorithm unless \(\mathrm P=\mathrm{NP}\).
The permission for jointly inconsistent menus already gives hardness with \(\tau=1\) and \(K=2\). To address the interaction with mass splitting and stability, I also prove hardness with \(\tau=2\), \(K=3\), and no unconditional antecedents. In that reduction, stability forces both types’ entire masses into the coalition.
Lemma. Suppose every antecedent is unconditional. A confirmed deal exists exactly when some type \(t\) with \(C_t\ne\varnothing\) has a strategy satisfying
\(\delta_t\land\bigwedge_{c\in C_t}B_c.\)
Proof. If a confirmed deal exists, its positive total mass guarantees an occupied cell \(x_{t,D,a}>0\). Every commitment in \(C_t\) has a true antecedent. Safe play therefore requires \(a\models B_c\) for every \(c\in C_t\); feasibility also requires \(a\models\delta_t\).
Conversely, suppose such a strategy \(a\) exists. Allocate all of type \(t\)’s mass to the cell with \(D=C_t\) and strategy \(a\), and leave every other type outside the coalition. This allocation satisfies its selected consequents. Stability holds because all selected antecedents are unconditional. Safe play holds because \(a\) satisfies every commitment of its type, independently of outsider choices. \(\square\)
Now let \(F\) be an arbitrary propositional SAT instance over variables \(X\), and introduce a fresh variable \(s\). Construct one type with
\(\mu_1=1,\qquad \Phi_1=X\cup\{s\},\qquad \delta_1=\top.\)
Its two commitments have unconditional antecedents and consequents
\(B_1=s\lor F,\qquad B_2=\neg s.\)
Both consequents are individually satisfiable: use \(s=1\) for \(B_1\) and \(s=0\) for \(B_2\). Their conjunction is equivalent to \(\neg s\land F\). By the lemma, the constructed society has a confirmed deal exactly when \(F\) is satisfiable.
The construction takes \(O(|F|)\) time and has
\(\tau=1,\qquad K=2,\qquad m=|X|+1,\qquad L=O(|F|).\)
The unconditional restriction also belongs to \(\mathrm{NP}\): a certificate consists of a type and a strategy satisfying the conjunction in the lemma. Thus this restriction is \(\mathrm{NP}\)-complete, already for \(\tau=1\) and \(K=2\).
The following reduction shows explicitly why arbitrary real mass splitting does not remove the hardness.
Let \(F\) again be a SAT instance over \(X\). Introduce fresh variables \(s,p,q\). Construct two types, each of mass \(1/2\), with
\(\Phi_1=X\cup\{s,p\},\qquad \Phi_2=\{q\},\qquad \delta_1=\delta_2=\top.\)
Their menus are:
| Type | Commitment | Antecedent | Consequent |
|---|---|---|---|
| \(1\) | \(c_1\) | \(h_{2,q}\ge 1\) | \(p\land(s\lor F)\) |
| \(1\) | \(c_2\) | \(h_{2,q}\ge 1\) | \(p\land\neg s\) |
| \(2\) | \(d\) | \(h_{1,p}\ge 1\) | \(q\) |
All input promises hold:
Write \(\beta_t\) for the total coalition mass of type \(t\).
Every allowed type-\(1\) coalition strategy sets \(p=1\): every nonempty selection contains \(c_1\) or \(c_2\), and both consequents imply \(p\). Every allowed type-\(2\) coalition strategy sets \(q=1\).
If \(\beta_1>0\), some occupied type-\(1\) selection requires stability of \(h_{2,q}\ge1\). Choose a feasible outsider profile in which all type-\(2\) outsiders set \(q=0\). Under every permitted coalition redistribution, the resulting share is
\(h_{2,q}=\beta_2/\mu_2.\)
Stability therefore implies \(\beta_2=\mu_2\).
Likewise, if \(\beta_2>0\), its only nonempty selection is \(\{d\}\). Choose all type-\(1\) outsiders to set \(p=0\). Stability of \(d\) then requires
\(h_{1,p}=\beta_1/\mu_1\ge1,\)
so \(\beta_1=\mu_1\).
A coalition must have positive total mass. Consequently, either starting case forces
\(\beta_1=\mu_1,\qquad \beta_2=\mu_2.\)
In any confirmed deal, type \(2\)’s coalition strategies all set \(q=1\), and the preceding argument leaves no outsiders. Thus both \(c_1\) and \(c_2\) have true antecedents.
Safe play requires every occupied type-\(1\) strategy to satisfy both consequents, including whichever commitment was omitted from its selection. Hence every such strategy satisfies
\(p\land(s\lor F)\land\neg s,\)
and therefore satisfies \(F\). Type \(1\) has positive coalition mass, so an occupied strategy exists. Thus \(F\) is satisfiable.
Conversely, let \(a_X\models F\). Allocate all type-\(1\) mass to selection \(\{c_1,c_2\}\) and strategy \((a_X,s=0,p=1)\). Allocate all type-\(2\) mass to selection \(\{d\}\) and strategy \(q=1\).
Every redistribution satisfying these selections still makes all type-\(1\) mass set \(p=1\) and all type-\(2\) mass set \(q=1\). Both threshold antecedents therefore remain true. There are no outsiders, and the displayed allocation satisfies every triggered consequent. It is a confirmed deal.
This proves the required equivalence. The reduction takes \(O(|F|)\) time, with
\(\tau=2,\qquad K=3,\qquad m=|X|+3,\qquad L=O(|F|).\)
For unconditional antecedents, the lemma gives an exhaustive-search algorithm with running time
\(O\!\left(L\sum_{t=1}^{\tau}2^{|\Phi_t|}\right)\subseteq O(\tau\,2^m L).\)
For completeness, the unrestricted problem also admits an exact finite algorithm. The following is a deliberately coarse upper bound:
\(2^{O(R^2\log R)},\qquad R=L+\tau\,2^{m+K}+2.\)
I give the construction and justify this bound below.
Enumerate each \(S_t\), and enumerate all valid coalition cells
\(I_t=\{(D,a):\varnothing\ne D\subseteq C_t,\ a\in S_t,\ a\models\bigwedge_{c\in D}B_c\}.\)
Set \(N=\sum_t|I_t|\) and \(M=\sum_t|S_t|\). Then
\(N\le\tau\,2^{m+K},\qquad M\le\tau\,2^m.\)
Use one existential allocation variable \(x_i\) per valid cell. Its feasibility constraints are nonnegativity, the type-mass bounds, and positive total coalition mass. Define
\(z_{t,D}=\sum_{a:(D,a)\in I_t}x_{t,D,a},\qquad \beta_t=\sum_{(D,a)\in I_t}x_{t,D,a}.\)
Introduce redistribution variables \(r_{t,D,a}\) over the same valid cells, and outsider variables \(b_{t,a}\) over \(S_t\).
A stability violation exists exactly when nonnegative \(r,b\) satisfy
\(\sum_a r_{t,D,a}=z_{t,D},\qquad \sum_a b_{t,a}=\mu_t-\beta_t,\)
and some selection with \(z_{t,D}>0\) has a selected commitment whose antecedent is false in the combined profile \((r,b)\).
A safe-play violation exists exactly when nonnegative \(b\) satisfies its outsider-mass equations, and some occupied cell \(x_{t,D,a}>0\) has a commitment \(c\in C_t\) such that \(a\not\models B_c\) but \(A_c\) is true in \((x,b)\).
These characterizations include zero outsider mass: nonnegativity and the mass equations then force every outsider variable of that type to be zero.
Let \(W(x,r,b)\) be the disjunction of these two violation formulas. The desired decision is precisely whether some feasible \(x\) satisfies
\(\neg\exists(r,b)\,W(x,r,b).\)
All atoms are rational affine comparisons. For example, a threshold is expressed without division as
\(\sum_{D,a:a_p=1}r_{u,D,a}+\sum_{a:a_p=1}b_{u,a}\ge\mu_u q.\)
There are \(O(N+M+L+\tau)\) distinct affine comparisons: repeated occurrences of an antecedent reuse its comparisons. The entire Boolean formula and its rational coefficients have size polynomial in \(R\).
Enumerate truth assignments to the distinct affine comparisons in \(W\). Each assignment making \(W\) true specifies a conjunction of weak or strict linear inequalities.
Consider one such conjunction, written as rows
\(U_jw\le v_j(x)\quad\text{or}\quad U_jw<v_j(x),\)
where \(w=(r,b)\), and each \(v_j\) is affine in \(x\).
Motzkin’s transposition theorem says that this system has a solution exactly when every nonnegative vector \(\lambda\) satisfying \(U^{\mathsf T}\lambda=0\) obeys
\(\lambda^{\mathsf T}v(x)\ge0,\)
with strict inequality required whenever \(\lambda\) assigns positive weight to a strict row. This theorem applies to arbitrary finite mixtures of strict and weak linear inequalities, as occur here. [Motzkin’s theorem and a formal proof](https://isa-afp.org/entries/Farkas.html)
It suffices to check the extreme rays of the cone \(\{\lambda\ge0:U^{\mathsf T}\lambda=0\}\): every cone vector is a nonnegative combination of these rays. If that vector gives positive weight to a strict row, at least one ray in its decomposition does so.
If \(w\) has dimension \(d\), every extreme ray has support at most \(d+1\). Indeed, on a support of size \(k\), an extreme ray requires the restricted kernel to have dimension one; otherwise a kernel perturbation would express it as a sum of two nonproportional cone vectors. Hence \(k-1\le d\).
The rays can therefore be enumerated by subsets of rows and rational linear algebra. With \(s\) distinct comparisons, there are at most \(2^s\) truth assignments and at most \((s+1)^{d+1}\) rays per conjunction. Thus the bad allocations are a union of explicitly described sets defined by affine weak or strict inequalities. Including allocation-feasibility constraints, the total number \(P\) of resulting affine expressions satisfies
\(\log(P+2)=O(R\log R).\)
Their coefficient bit lengths remain polynomial in \(R\), by determinant bounds for rational linear systems.
Construct the arrangement of these affine hyperplanes in the \(N\)-dimensional allocation space, retaining faces of every dimension. On each relatively open face, every affine expression has a fixed sign. Allocation feasibility and membership in the union of bad sets are therefore constant on that face.
Such an arrangement has at most \((P+1)^{O(N)}\) faces. One justification is to choose a basis of the hyperplanes vanishing on a face, then count full-dimensional regions in their intersection using the usual hyperplane-region recurrence. Summing over basis sizes gives the stated bound.
The faces can be constructed incrementally, testing each proposed sign region by rational linear programming. Strict feasibility is handled by introducing a common margin \(0\le\varepsilon\le1\), replacing strict rows by rows with margin \(\varepsilon\), and checking whether the maximum margin is positive.
Accept exactly when a nonempty face consists of feasible allocations outside all bad sets. Because \(N\le R\), this procedure has total running time
\(2^{O(R^2\log R)}.\)
The algorithm handles arbitrary real allocations directly. The hardness proofs settle the requested polynomial-time-versus-hardness alternative; no matching complexity upper classification is claimed.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly. Both reductions establish NP-hardness under the stated input promises. The unrestricted finite algorithm also correctly models the two universal requirements, and its deliberately coarse running-time bound is justified. No major or minor mathematical issue was found.
The equivalence is correct.
For necessity, positive total coalition mass guarantees an occupied cell, since the indexing sets are finite. Its selection is nonempty, so its type has a nonempty menu. Feasibility requires its strategy to satisfy \(\delta_t\), and safe play requires it to satisfy every consequent in that type’s menu because every antecedent holds.
For sufficiency, the proposed selection \(D=C_t\) is nonempty. The assumed strategy satisfies all selected consequents and is feasible. Stability holds under every permitted redistribution because the antecedents are unconditional. Safe play holds for every outsider profile because the occupied strategy satisfies every consequent of its type.
Types with empty menus cause no exception: they cannot supply an occupied coalition cell and are explicitly excluded from the lemma’s existential condition.
The construction satisfies all promises:
The critical Boolean calculation is correct:
\[
(s\lor F)\land\neg s\quad\text{is equivalent to}\quad\neg s\land F.
\]
Thus the lemma gives the claimed equivalence between satisfiability of \(F\) and confirmed-deal existence. Arbitrary mass splitting cannot evade the implication: every occupied strategy must satisfy both consequents.
The construction is linear in the encoded SAT-instance size, with \(\tau=1\), \(K=2\), and \(m=|X|+1\). The stated input-size bound is consistent with ordinary explicit formula encoding.
The NP-membership claim for the unconditional restriction is also correct. A type index and one Boolean strategy form a polynomial-size certificate, and all formulas in the lemma can be evaluated in polynomial time. Consequently, the NP-completeness claim for this restriction is justified.
All listed checks are valid. In particular, each threshold concerns the other type, each antecedent is attainable in a feasible full profile, and each can also be false. Every consequent is satisfiable together with its type’s local constraint.
Every permissible type-\(1\) coalition strategy sets \(p=1\), and every permissible type-\(2\) coalition strategy sets \(q=1\).
If \(\beta_1>0\), some positive type-\(1\) selection activates a stability requirement for \(h_{2,q}\ge1\). The outsider profile setting all type-\(2\) outsiders’ \(q\) values to zero is feasible. Under every permitted coalition redistribution, the resulting share is exactly \(\beta_2/\mu_2\). Since \(\beta_2\le\mu_2\), stability forces equality.
The symmetric argument correctly forces \(\beta_1=\mu_1\) whenever \(\beta_2>0\). Positive total coalition mass ensures that one of these implications starts, and then both types participate fully.
The quantification over redistributions introduces no vacuity: the feasible allocation witnessing stability itself supplies a permitted redistribution.
With full participation, there are no outsiders, and all type-\(2\) strategies set \(q=1\). Both type-\(1\) antecedents therefore hold.
Safe play applies to every commitment in the menu, including commitments omitted from an occupied cell’s selection. Every occupied type-\(1\) strategy consequently satisfies \(p\land(s\lor F)\land\neg s\), and hence \(F\). Positive type-\(1\) mass guarantees such a strategy exists.
The proposed allocation satisfies both selections. Every permitted redistribution preserves \(p=1\) throughout type \(1\) and \(q=1\) throughout type \(2\), so stability holds. The allocation satisfies every triggered consequent, and the empty outsider profile is correctly included.
The equivalence and the parameter bounds \(\tau=2\), \(K=3\), and \(m=|X|+3\) are therefore valid.
Enumerating local assignments and evaluating the relevant formulas gives the stated bound
\[
O\!\left(L\sum_{t=1}^{\tau}2^{|\Phi_t|}\right)
\subseteq O(\tau\,2^mL).
\]
This enumeration also covers types with no local variables.
The valid-cell enumeration includes precisely the strategies permitted for each nonempty selection. The bounds on \(N\) and \(M\) are valid coarse bounds.
The stability-violation formula correctly fixes each selection’s mass while allowing its redistribution among strategies satisfying that selection’s consequents. Its outsider equations use the remaining mass of each type.
The safe-play-violation formula correctly keeps the allocation \(x\) fixed, varies only outsiders, and checks all commitments of each occupied cell’s type.
Sharing outsider variables between the two disjuncts introduces no restriction: the existential quantifier distributes over the disjunction, and redistribution variables are unused in the safe-play branch.
The cross-multiplied threshold comparison is correct because \(\mu_u>0\). Thus all relevant conditions are Boolean combinations of rational affine comparisons. Zero outsider masses are handled correctly by nonnegativity and the mass equations.
The stated version of Motzkin’s theorem is correct: feasibility requires nonnegative right-hand-side combinations for every nonnegative multiplier annihilating the left-hand sides, with positivity when a strict row receives positive weight. The systems here are finite systems of real linear inequalities, so its hypotheses apply. The linked [formalization](https://isa-afp.org/browser_info/current/AFP/Farkas/outline.pdf) covers the relevant strict and non-strict transposition theorem.
The multiplier cone is polyhedral and pointed because it lies in the nonnegative orthant. The reduction to extreme rays is valid, including the treatment of strict rows.
The support bound follows from the stated kernel-dimension argument. Enumeration by row subsets and rational linear algebra is therefore justified. Determinant bounds give polynomial coefficient bit lengths, and the resulting number of affine expressions satisfies the claimed coarse logarithmic bound.
On each relatively open arrangement face, all affine comparisons have fixed truth values. Including faces of every dimension correctly retains allocations lying on threshold boundaries or satisfying equalities.
The face-count estimate and incremental feasibility testing fit the claimed bound. The common-margin method correctly tests simultaneous strict inequalities: a finite strictly feasible system admits a positive common margin, while a positive optimum certifies strict feasibility.
Combining the expression count, \(N\le R\), and polynomial coefficient bit lengths yields the stated total bound \(2^{O(R^2\log R)}\), where \(R=L+\tau\,2^{m+K}+2\).
The NP-hardness conclusion follows already from the first reduction; the second independently verifies that nonconstant antecedents and arbitrary real mass splitting do not invalidate the hardness result.
The write-up supplies running times in the requested parameters and does not claim an unsupported matching complexity classification.
No repair or additional clarification 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.