← back to the atlas

d4-conf-atal-2016-0025 (d4-conf-atal-2016-0025)

Answer: \(\mathrm{NP}\text{-hard}\); the existence decision problem is \(\mathrm{NP}\text{-complete}\).

The anchor (named result in the paper)

Theorem 2 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateAlg. 1 is sound, i.e. the strategy profile obtained by this protocol is socially optimal (see Def. 6).

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite action set \(A\), a finite support \(T\) with positive rational masses \(\mu_t\) summing to \(1\), each type's preferences and internal argumentation framework, and agreed attacks between disclosable arguments, determine whether there is a rational allocation \(x_{t,a}\geq 0\) with \(\sum_a x_{t,a}=\mu_t\), \(x_{t,a}=0\) unless \(a\) is feasible for type \(t\), and rational per-action bounds \(\ell_a\leq\sum_t x_{t,a}\leq u_a\). Feasibility is defined by admissibility of the action's practical argument in the type's perfect-view framework. Return an allocation for which no other feasible allocation \(y\) admits, for every type \(t\), a coupling from \(x_{t,\cdot}\) to \(y_{t,\cdot}\) supported only on actions that type \(t\) strictly prefers; otherwise report that none exists.

Packaged proof task (what the prover saw — nothing else)

Let \(A\) be a nonempty action set of size \(m\). A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) counts supported types, not possible types. Each type has a complete preorder on \(A\); write \(b\succ_t a\) for its strict part, without breaking ties.
Each type has an explicitly given finite internal argumentation framework \(F_t=(P_t\cup D_t\cup Q_t,E_t)\), partitioned into practical arguments \(P_t=\{p_{t,a}:a\in A\}\), disclosable epistemic arguments \(D_t\), and private epistemic arguments \(Q_t\). Argument sets of different types are disjoint. Practical arguments have no outgoing attacks; private epistemic arguments cannot attack disclosable arguments; every private epistemic argument is attacked by a disclosable argument in its internal framework. Every practical argument belongs to some admissible set of its internal framework.
Put \(D=\bigcup_t D_t\). An explicitly given agreed attack relation \(R\subseteq D\times D\) agrees with each internal framework on its disclosable arguments. The perfect-view framework is \(F_t^*=(P_t\cup Q_t\cup D,E_t\cup R)\). Action \(a\) is feasible for \(t\) precisely when \(p_{t,a}\) belongs to some admissible set of \(F_t^*\). Frameworks are specified once per type and do not depend on allocated masses.
Given binary rational bounds \(0\leq\ell_a\leq u_a\leq1\), an allocation is feasible if \(x\in\mathbb Q_{\geq0}^{T\times A}\), \(\sum_a x_{t,a}=\mu_t\), \(x_{t,a}=0\) for infeasible actions, and \(\ell_a\leq\sum_t x_{t,a}\leq u_a\) for every action.
A feasible allocation \(y\) strictly improves \(x\) if every type admits a rational coupling \(c^t\in\mathbb Q_{\geq0}^{A\times A}\) with \(\sum_b c^t_{a,b}=x_{t,a}\), \(\sum_a c^t_{a,b}=y_{t,b}\), and \(c^t_{a,b}=0\) unless \(b\succ_t a\). Call \(x\) socially optimal when no feasible allocation strictly improves it.
Is finding a rational socially optimal allocation, or reporting that none exists, solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), the total input bit length \(L\), and the total numbers of explicitly encoded arguments and attacks.
For finite agents with arbitrary allowed action-count sets, the known coordination protocol is sound: every returned profile is feasible, satisfies the count constraints, and admits no feasible profile strictly improving every agent; the protocol is explicitly incomplete. [Gao et al., 2016](https://www.ifaamas.org/Proceedings/aamas2016/pdfs/p1153.pdf)
No result settling exactly this continuous problem was located in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The problem is \(\mathrm{NP}\)-hard, already with \(m=1\) and \(\tau=2\). Its associated existence decision problem is \(\mathrm{NP}\)-complete. Thus a polynomial-time algorithm for the requested task would imply \(\mathrm{P}=\mathrm{NP}\).

The continuous allocation stage is polynomial-time solvable once the feasible type–action pairs are known. The hardness comes from determining feasibility in the explicitly encoded argumentation frameworks.

1. Feasibility implies existence of a rational socially optimal allocation

For each type \(t\), define
\[ B_t=\{a\in A:p_{t,a}\text{ belongs to an admissible set of }F_t^*\}. \]
Here and below, a set is admissible precisely when it is conflict-free and attacks every argument attacking one of its members.

Temporarily allow real allocation coordinates, and let \(\mathcal X\) be the polytope defined by the allocation constraints using the sets \(B_t\). This polytope is bounded: nonnegativity and the row-sum constraints imply \(0\leq x_{t,a}\leq\mu_t\leq1\).

For each type, number its preference equivalence classes from least preferred to most preferred. Let \(r_t(a)\in\{0,\ldots,m-1\}\) be the number of the class containing \(a\). Ties receive the same number, and
\[ b\succ_t a\quad\Longrightarrow\quad r_t(b)-r_t(a)\geq1. \]

Define the linear objective
\[ W(x)=\sum_{t\in T}\sum_{a\in A}r_t(a)x_{t,a}. \]

Suppose \(y\) strictly improves \(x\), with the couplings specified in the question. Their marginal equations give
\[ W(y)-W(x) =\sum_{t\in T}\sum_{a,b\in A} c^t_{a,b}\bigl(r_t(b)-r_t(a)\bigr) \geq\sum_{t\in T}\sum_{a,b\in A}c^t_{a,b} =\sum_{t\in T}\mu_t =1. \]
The inequality holds because every positive coupling entry represents a strictly preferred destination.

Consequently, every maximizer of \(W\) over \(\mathcal X\) is socially optimal. If \(\mathcal X\) is nonempty, boundedness guarantees a maximizer, and rational linear programming guarantees a rational maximizing vertex. Therefore
\[ \text{a rational socially optimal allocation exists} \quad\Longleftrightarrow\quad \text{a feasible allocation exists}. \]

Once the sets \(B_t\) are supplied, we can find such a maximizer—or establish infeasibility—by rational linear programming in \((L+\tau m)^{O(1)}\) bit operations. The program has \(\tau m\) variables and \(O(\tau m+\tau+m)\) constraints.

There is also an explicit polynomial bound on output length. Put \(d=\tau m\), and let \(H\) be the product of the denominators of the input masses and bounds. Then \(\log_2H=O(L)\). At any vertex, select \(d\) linearly independent active constraints. Their coefficient matrix \(M\) has entries in \(\{0,1,-1\}\). Cramer’s rule gives a common coordinate denominator dividing \(H|\det M|\), while Hadamard’s inequality gives \(|\det M|\leq d^{d/2}\). Since all coordinates lie in \([0,1]\), each coordinate needs only \(O(L+d\log(d+1))\) bits.

2. A satisfiability reduction satisfying every framework restriction

Let \(\varphi\) be a Boolean formula in conjunctive normal form, with variables \(v_1,\ldots,v_n\) and clauses \(C_1,\ldots,C_q\). We construct an instance with two supported types and one action:
\[ T=\{1,2\},\qquad A=\{a\},\qquad \mu_1=\mu_2=\tfrac12,\qquad \ell_a=u_a=1. \]

Write \(p_1=p_{1,a}\) and \(p_2=p_{2,a}\). Both private argument sets are empty.

For type \(1\), let
\[ D_1=\{z\}\cup\{v_i,\neg v_i:1\leq i\leq n\} \cup\{c_j:1\leq j\leq q\}. \]
Its internal attacks are exactly:

For type \(2\), let \(D_2=\{h\}\), and let its internal attack relation be empty.

The agreed relation \(R\) contains every type-\(1\) internal attack whose endpoints are both disclosable, together with the additional attack \(h\to z\). It contains no other attacks.

This construction satisfies all the premises:

Claim: \(p_1\) is feasible exactly when \(\varphi\) is satisfiable

Forward direction. Let \(S\) be an admissible set of \(F_1^*\) containing \(p_1\).

The argument \(h\) has no attackers anywhere in \(F_1^*\). Since \(h\) attacks \(z\), no set can defend \(z\) against \(h\). Hence \(z\notin S\).

Every \(c_j\) attacks \(p_1\). Admissibility therefore requires \(S\) to attack every \(c_j\). Its possible attackers are \(z\) and the literals occurring in \(C_j\). Since \(z\notin S\), the set \(S\) contains a literal from each clause.

Conflict-freeness prevents \(S\) from containing both \(v_i\) and \(\neg v_i\). Assign variables consistently with the literals in \(S\), and assign any remaining variables arbitrarily. Every clause has a selected true literal, so this assignment satisfies \(\varphi\).

Reverse direction. Suppose \(\varphi\) has a satisfying assignment. Let \(S\) consist of \(p_1\) and, for each variable, the literal made true by that assignment.

This set is conflict-free: it contains no complementary literals and contains neither clause arguments nor \(z\). Each selected literal defends itself against its only attacker, its complementary literal, by attacking that complementary literal. Every clause argument attacking \(p_1\) is attacked by a selected satisfying literal. These are all attackers of members of \(S\), so \(S\) is admissible.

This proves the claim.

Meanwhile, \(p_2\) is always feasible in \(F_2^*\), because \(R\subseteq D\times D\) cannot attack \(p_2\), and its internal framework has no attacks.

With one action, the only possible allocation is
\[ x_{1,a}=x_{2,a}=\tfrac12. \]
It is feasible exactly when \(\varphi\) is satisfiable. Whenever feasible, it is socially optimal: the strict preference relation on a singleton action set is empty, so no strict-improvement coupling can transport either type’s positive mass.

The construction uses \(O(n+q)\) arguments and \(O(n+q+s)\) explicitly encoded attacks, where \(s\) is the number of literal occurrences. It is therefore a polynomial-time reduction from satisfiability.

Thus an algorithm performing the requested search-and-report task would decide satisfiability by distinguishing an allocation from a report of nonexistence.

This hardness does not require degenerate preferences. Add a second action \(b\), make its practical argument isolated for both types, set \(a\succ_t b\), and impose \(\ell_a=u_a=1\) and \(\ell_b=u_b=0\). The same equivalence holds with \(m=2\), strict preferences, and a globally feasible alternative for each type.

3. The existence decision problem is \(\mathrm{NP}\)-complete

Hardness follows from the reduction above.

For membership in \(\mathrm{NP}\), a certificate consists of:

Such an allocation exists whenever any feasible allocation exists, by the vertex argument in Section 1. There are at most \(\tau m\) argument-set witnesses, each encoded by a polynomial-length membership vector.

The verifier checks the allocation constraints using exact rational arithmetic. For each argument-set witness, it checks conflict-freeness and defense against all attackers by scanning the framework’s vertices and attacks. All these checks take polynomial time.

By Section 1, existence of a feasible allocation and existence of a rational socially optimal allocation are equivalent. Hence their common existence decision problem is \(\mathrm{NP}\)-complete.

4. Running times

Let
\[ N=\sum_{t\in T}\bigl(|P_t|+|D_t|+|Q_t|\bigr), \qquad K=\sum_{t\in T}|E_t|+|R| \]
be the total explicitly encoded argument and attack counts. For each type, put
\[ n_t^*=m+|Q_t|+|D|, \qquad k_t^*=|E_t\cup R|. \]
Then \(n_t^*\leq N\) and \(k_t^*\leq K\).

With feasible type–action pairs supplied, the task takes \((L+\tau m)^{O(1)}\) bit operations.

With an \(\mathrm{NP}\) oracle, determine every pair’s feasibility using \(\tau m\) queries. Each query asks for an admissible set containing a specified practical argument in a framework with at most \(N\) arguments and \(K\) attacks. These queries are independent and can be issued in parallel. Query preparation and the subsequent allocation optimization take polynomial time in \(L,m,\tau,N,K\).

Without an oracle, an exact algorithm enumerates every argument subset of each \(F_t^*\). Checking one subset and recording its practical members takes \(O(n_t^*+k_t^*)\) elementary graph operations. Thus the framework stage takes
\[ O\!\left(\sum_{t\in T}2^{n_t^*}(n_t^*+k_t^*)\right) \subseteq O\!\left(\tau\,2^N(N+K)\right) \]
graph operations, followed by polynomial-time allocation optimization. Including bit-level overhead gives the conservative total bound
\[ 2^N(L+\tau m+N+K)^{O(1)}. \]

These bounds use supported types directly; they do not expand rational masses into individual agents. Fixing \(m\) and \(\tau\) does not remove hardness, since the reduction has \(m=1\) and \(\tau=2\). In contrast, when \(\tau=1\), agreement of \(R\) with the internal framework makes the perfect-view framework unchanged. Every action is then feasible by the premise, and the task is polynomial-time solvable.

The supplied finite-agent protocol does not contradict this result: its soundness theorem is accompanied by an explicit statement of incompleteness. [Gao et al., 2016, Section 6](https://www.ifaamas.org/Proceedings/aamas2016/pdfs/p1153.pdf)

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover resolves the task correctly. The requested search-and-report problem is \(\mathrm{NP}\)-hard under the specified explicit framework encoding, and its existence decision problem is \(\mathrm{NP}\)-complete. I found no major or minor mathematical gaps.

1. Feasibility and social optimality

Preference ranks are valid. A complete preorder on a finite action set admits ordered equivalence classes. The stated ranks preserve ties and satisfy \(r_t(b)-r_t(a)\geq1\) whenever \(b\succ_t a\). No tie-breaking is introduced.

The objective calculation is correct. The two marginal equations yield the displayed expression for \(W(y)-W(x)\). Every positive coupling entry has rank difference at least \(1\), and the total transported mass is
\(\sum_t\mu_t=1\). Thus the claimed bound \(W(y)-W(x)\geq1\) holds. This uses the task’s actual requirement that all transported mass moves strictly upward.

Maximizers exist and are socially optimal. The allocation constraints define a closed polytope, and the row sums and nonnegativity make it bounded. Consequently, a nonempty allocation polytope has a maximizer of the stated linear objective. The objective increase excludes any strict improvement of such a maximizer.

Rationality is justified. The relevant linear-programming facts apply: a nonempty bounded rational polyhedron has vertices, its vertices are rational, and a linear objective attains its maximum at a vertex. The constraints here have rational coefficients. Hence real feasibility implies rational feasibility and a rational socially optimal allocation.

The resulting equivalence between feasible allocation existence and rational socially optimal allocation existence is established in both directions.

2. Polynomial output length and allocation time

The vertex bound checks out. With \(d=\tau m\), a vertex has \(d\) linearly independent active constraint normals, including when the polytope has lower affine dimension. Their coefficients lie in \(\{0,1,-1\}\).

Multiplying the right-hand side by the product \(H\) of input denominators gives integer entries. Cramer’s rule therefore gives the stated common denominator bound \(H|\det M|\). Hadamard’s inequality gives \(|\det M|\leq d^{d/2}\). Together with coordinates in \([0,1]\), this verifies the coordinate bit bound \(O(L+d\log(d+1))\).

The polynomial allocation bound is valid. Once feasible pairs are supplied, the program has \(\tau m\) variables, the stated number of constraints, and polynomial encoding length. Exact rational linear programming supplies a rational optimizer or an infeasibility determination in the claimed polynomial bit complexity.

3. Validity of the satisfiability reduction

Every framework restriction is respected.

The positive masses, their normalization, the nonempty support, and the allocation bounds also satisfy the task.

Forward implication is correct. In \(F_1^*\), the argument \(h\) is unattacked and attacks \(z\). Therefore no admissible set can contain \(z\). An admissible set containing \(p_1\) must attack each clause argument, and the listed attacks leave a clause literal as the only available defender. Conflict-freeness excludes complementary selected literals. The selected literals therefore yield a consistent satisfying assignment as claimed.

Reverse implication is correct. The set consisting of \(p_1\) and the assignment’s true literal for each variable is conflict-free. Each selected literal counterattacks its complementary literal, its only attacker. Satisfaction supplies a selected attacker of every clause argument attacking \(p_1\). All defense requirements are covered.

The second practical argument stays feasible. Neither its empty internal attack relation nor \(R\subseteq D\times D\) introduces an attack on \(p_2\).

The allocation equivalence is correct. With one action, the row constraints force both coordinates to equal \(\tfrac12\). Feasibility is therefore equivalent to satisfiability. The empty strict relation on a singleton prevents any strict-improvement coupling with positive total mass.

This singleton case is expressly permitted by the task. Moreover, the stated two-action extension correctly preserves the reduction while giving both types a strict preference and an always-feasible alternative. The bounds force all mass onto the original action.

Construction size is polynomial. The stated argument and attack counts follow from the construction. Binary identifiers introduce only polynomial encoding overhead. Thus distinguishing a returned allocation from a correct nonexistence report decides satisfiability.

4. Membership in \(\mathrm{NP}\)

The proposed certificate is sufficient and polynomial in length.

A feasible allocation of polynomial bit length exists by the verified vertex bound. For each positive coordinate, a membership vector specifies an admissible set containing its practical argument. There are at most \(\tau m\) such witnesses, each over at most \(N\) arguments.

Exact rational arithmetic verifies the allocation constraints. Scanning the explicitly constructed perfect-view framework verifies conflict-freeness and defense in polynomial time. Separate witnesses for different positive coordinates are appropriate: the task defines feasibility separately for each action and requires no common admissible set.

The certificate need not establish that its allocation is socially optimal, because the already-proved existence equivalence settles the existence decision problem. The \(\mathrm{NP}\)-completeness conclusion follows.

5. Running times and boundary cases

The bounds \(n_t^*\leq N\) and \(k_t^*\leq K\) are correct.

Enumerating all subsets of each perfect-view framework, checking admissibility, and recording practical members gives the stated graph-operation bound
\(O(\sum_t2^{n_t^*}(n_t^*+k_t^*))\).
Its upper bound \(O(\tau2^N(N+K))\), and the conservative total bit bound \(2^N(L+\tau m+N+K)^{O(1)}\), are valid.

The \(\tau m\) oracle queries have polynomial-length witnesses and do not depend on earlier answers. The subsequent optimization is polynomial. The proof correctly uses supported types without expanding rational masses into agents.

For \(\tau=1\), all disclosable arguments are internal. Agreement implies that adding \(R\) changes no attacks, so the perfect-view framework equals the internal framework. The premise makes every action feasible, leaving only the polynomial allocation stage.

Empty clauses and formulas with no clauses cause no failure in the reduction: an empty clause cannot be defended after \(z\) becomes unavailable, while no clauses leave \(p_1\) unattacked.

The literature comparison is also accurate: Section 6 states soundness and explicitly acknowledges incompleteness. It supplies no complete algorithm contradicting this reduction. [Gao et al., 2016, Section 6](https://www.ifaamas.org/Proceedings/aamas2016/pdfs/p1153.pdf)

6. Required feedback

No repair or additional clarification is necessary. The polynomial allocation stage is a conditional subroutine result; the full continuous problem with the task’s explicitly encoded frameworks is correctly classified as hard.

⟨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.