← back to the atlas

d4-conf-aaai-2023-0196 (d4-conf-aaai-2023-0196)

Answer: \(\mathrm{NP}\text{-hard}\)

The anchor (named result in the paper)

Theorem 4 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet G be a system representing a mecha- nism M. The SCF f E-implemented by M is (interim) in- dividual rational iff G, v∅|= ∃s. E(s) ∧F(ter ∧φf,s∧ V θ∈Θ IR(s, θ)). In order to collect truthful preferences, the mechanism can be designed to incentivize the agents to tell the truth. In Dominant Strategy Incentive Compatible (DSIC), truth revelation is the best strategy for each agent irrespective of what is reported by the other agents.

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

The continuous mirror question, as graded

Given a rational mass vector \(\mu\) over \(\tau\) complete agent types, a finite anonymous mechanism with rational piecewise-polynomial aggregate transition and outcome rules, type utilities, and target per-type lotteries \(F_t\), does there exist a memoryless strategy kernel \(x_t(v)\in\Delta(A)\) that is a Bayesian best response for every positive-mass type, induces \(F_t\), and gives every such type nonnegative interim utility? A unilateral deviation has zero effect on the aggregate action masses \(q_{t,a}(v)=\mu_t x_t(v,a)\).

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

A society is given by its support: a list of \(\tau\) complete types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; the masses are the entire population specification, with no additional random population composition.
The input contains nonempty finite sets of observable states \(V\), actions \(A\), and individual alternatives \(B\), an initial state \(v_0\), nonempty legal-action sets \(A(v)\), and absorbing terminal states, each labelled by exactly one alternative. Write \(n=|V|\), \(k=|A|\), and \(m=|B|\).
An anonymous mechanism specifies representative-agent transition kernels \(K_t(v,a,q)\in\Delta(V)\), depending on the type, the individual's legal action, and the aggregate action masses at that state. These kernels include the individual's outcome rule through terminal labels; a deviation can change the individual's transitions and outcome while leaving the aggregate field fixed.
Each kernel entry is a rational piecewise-polynomial function on \(q_{t,a}\geq0\), \(\sum_{a\in A(v)}q_{t,a}=\mu_t\), with illegal-action coordinates zero. Pieces are explicitly listed using polynomial inequality guards and polynomial monomial lists with binary coefficients and exponents; the first matching guard applies, and guards cover the domain. The input is promised to define probability distributions and to make every supported path from \(v_0\) reach a terminal state under every admissible aggregate field and legal strategy.
Each type has signed binary-rational quasi-linear utility \(u_t(b)=w_t(c_b)-p_b\), where \(b=(c_b,p_b)\), with signed binary-rational valuations and payments, and a target binary-rational lottery \(F_t\in\Delta(B)\). The outside-option utility is zero.
A candidate consists of real-valued memoryless kernels \(x_t(v)\in\Delta(A(v))\), defining \(q_{t,a}(v)=\mu_t x_t(v,a)\). For any legal memoryless deviation \(y\), let \(D_t(y;q)\) be the terminal-label lottery from \(v_0\) in the Markov chain with transition \(\sum_a y(v,a)K_t(v,a,q(v))\), and put \(U_t(y;q)=\sum_bD_t(y;q)(b)u_t(b)\).
Feasibility requires, for every supported type, \(D_t(x_t;q)=F_t\), \(U_t(x_t;q)\geq0\), and \(U_t(x_t;q)\geq U_t(y;q)\) for every legal memoryless \(y\); the entire aggregate field \(q\) stays fixed during a unilateral deviation. These comparisons are interim comparisons from the initial state.

Is this feasibility problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L,n,k\), where \(L\) is the total binary input length, including all polynomial descriptions.

For finite-agent mechanisms, equilibrium implementation together with interim individual rationality has a [Probabilistic Strategy Logic characterization](https://ojs.aaai.org/index.php/AAAI/article/download/26373/26145); this is not a polynomial-time or hardness classification.
[Memoryless PSL model checking](https://www.ijcai.org/proceedings/2019/0005.pdf) is decidable in space exponential in the system size and triple-exponential in the formula size. No result settling the exact mass feasibility problem above was located.

Modeling choices made when packaging the task

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

Result

The feasibility problem is \(\mathrm{NP}\)-hard, even when \(\tau=1\), \(m=2\), \(n=3\), every run terminates after one transition, and every kernel entry is a single polynomial of degree at most six.

Thus a running time polynomial in \(m,\tau,L,n,k\) would imply \(\mathrm{P}=\mathrm{NP}\).

For the general promised problem, an existential-real formulation gives a deterministic decision algorithm with running time

\(\displaystyle 2^{\left(L+\tau n^3(m+k+1)\right)^{O(1)}}\)

and space polynomial in \(L+\tau n^3(m+k+1)\). The hardness proof and the upper bound follow.

1. Reduction from Boolean satisfiability

Let \(\Phi\) be a Boolean formula in conjunctive normal form with variables \(z_1,\ldots,z_d\) and clauses \(C_1,\ldots,C_s\), each containing three literals. We reduce from \(\mathrm{3SAT}\), restricting to \(d\geq1\).

For a literal \(\ell\), define its *falsity polynomial* by

\(\displaystyle f_\ell(z)= \begin{cases} 1-z_i,&\ell=z_i,\\ z_i,&\ell=\neg z_i. \end{cases}\)

On Boolean inputs, \(f_\ell(z)\) equals one exactly when \(\ell\) is false. Define

\(\displaystyle R(z)=\sum_{i=1}^{d}z_i^2(1-z_i)^2+ \sum_{j=1}^{s}\left(\prod_{\ell\in C_j}f_\ell(z)\right)^2.\)

Every summand is a square. Consequently,

\(\displaystyle R(z)=0 \quad\Longleftrightarrow\quad z\in\{0,1\}^{d}\text{ and }z\text{ satisfies }\Phi.\)

Indeed, vanishing of the first sum forces each \(z_i\) to be zero or one. On such inputs, a clause summand vanishes exactly when at least one of its literals is true.

Encoding the variables in aggregate masses

Use one supported type, of mass \(\mu_1=1\), and actions \(a_0,a_1,\ldots,a_d\). At the initial state all actions are legal. Write \(q_i=q_{1,a_i}(v_0)\), and substitute

\(\displaystyle z_i=dq_i\qquad(1\leq i\leq d).\)

The aggregate domain is the simplex

\(\displaystyle q_i\geq0,\qquad \sum_{i=0}^{d}q_i=1.\)

Every Boolean vector \(\zeta\in\{0,1\}^{d}\) has a corresponding admissible aggregate vector:

\(\displaystyle q_i=\frac{\zeta_i}{d}\quad(1\leq i\leq d),\qquad q_0=1-\frac{1}{d}\sum_{i=1}^{d}\zeta_i.\)

The last coordinate is nonnegative because \(\sum_i\zeta_i\leq d\).

Making the polynomial a valid probability

Throughout the aggregate simplex, \(0\leq z_i\leq d\). Since \(d\geq1\), both \(|z_i|\) and \(|1-z_i|\) are at most \(d\). Therefore

\(\displaystyle 0\leq R(z)\leq d^5+sd^6.\)

Choose a power of two \(C\) satisfying

\(\displaystyle C\geq d^5+sd^6.\)

Its binary length is \(O(\log(d+s+2))\). Define

\(\displaystyle p(q)=\frac{R(dq_1,\ldots,dq_d)}{C}.\)

Then \(0\leq p(q)\leq1\) everywhere on the aggregate domain.

The mechanism

There are three states: the initial state \(v_0\) and two absorbing terminals \(v_G,v_H\). Their labels are two distinct alternatives \(G,H\).

For every initial action \(a\), set

\(\displaystyle K_1(v_0,a,q)(v_G)=1-p(q),\qquad K_1(v_0,a,q)(v_H)=p(q),\qquad K_1(v_0,a,q)(v_0)=0.\)

At each terminal, allow only \(a_0\), with a deterministic self-loop.

Give both alternatives payment zero and valuation zero. Thus

\(\displaystyle u_1(G)=u_1(H)=0.\)

Set the target lottery to \(F_1=\delta_G\).

This instance satisfies every promise:

2. Correctness and size of the reduction

For any candidate \(x_1\), its aggregate field at the initial state is \(q=x_1(v_0)\). Because the initial transition row is identical for every action,

\(\displaystyle D_1(x_1;q)(H)=p(q).\)

All utilities are zero. Hence individual rationality holds, and every legal deviation has exactly the same utility, zero, with the aggregate field fixed. Feasibility therefore reduces to the target-lottery condition:

\(\displaystyle \text{feasible} \quad\Longleftrightarrow\quad p(q)=0\text{ for some admissible }q. \)

If \(\Phi\) is satisfiable, the aggregate vector constructed from a satisfying Boolean assignment gives \(p(q)=0\), and hence a feasible candidate.

Conversely, if a feasible candidate exists, then \(R(dq_1,\ldots,dq_d)=0\). The sum-of-squares argument proves that \((dq_1,\ldots,dq_d)\) is a Boolean satisfying assignment for \(\Phi\).

Thus

\(\displaystyle \Phi\text{ is satisfiable}\quad\Longleftrightarrow\quad \text{the constructed instance is feasible}.\)

For the input-size check, each variable summand has three monomials. Each clause summand is a product of three squared affine factors, so expansion produces at most \(27\) monomials. Coefficient lengths are polynomially bounded, and substituting \(z_i=dq_i\) does not increase the degree. Repeating these descriptions for the \(d+1\) actions still produces polynomial total length, even if exponent vectors are written densely.

The reduction is therefore computable in polynomial time. Its parameters are

\(\displaystyle m=2,\qquad \tau=1,\qquad n=3,\qquad k=d+1,\qquad L=\operatorname{poly}(|\Phi|).\)

This proves the claimed \(\mathrm{NP}\)-hardness.

3. A finite-horizon consequence of the termination promise

For the upper bound, use the stated promise that every supported path reaches a terminal.

Fix a type \(t\) and an admissible aggregate field \(q\). Put an edge from \(v\) to \(w\) whenever

\(\displaystyle K_t(v,a,q(v))(w)>0\)

for some legal action \(a\). Consider the subgraph reachable from \(v_0\).

This subgraph has no directed cycle consisting of nonterminal states. To prove this, choose a memoryless strategy assigning positive probability to every legal action at every state. Every graph edge then has positive transition probability. A reachable nonterminal cycle would yield an infinite supported path that repeatedly traverses the cycle, contradicting the promise.

Therefore every supported path, under any strategy, reaches a terminal within \(n\) transitions. This conclusion concerns pathwise termination; almost-sure termination alone would not justify it.

Moreover, for this fixed \(q\), an optimal terminal-utility strategy can be chosen deterministic and memoryless. On the reachable nonterminal graph, reverse topological induction defines the value of a state as the maximum, over its legal actions, of the expected successor value. Choosing a maximizing action at each state attains these values. The same induction bounds the utility of every history-dependent strategy.

4. Existential-real encoding

Introduce candidate variables \(x_t(v,a)\), enforcing the legal-action simplex constraints, and impose

\(\displaystyle q_{t,a}(v)=\mu_t x_t(v,a).\)

Introduce transition variables \(\kappa_{t,v,a,w}\) equal to the specified kernel entries evaluated at \(q(v)\).

For an entry whose listed guards and polynomials are \(G_i,p_i\), first-match semantics are expressed by

\(\displaystyle \bigvee_i\left( G_i(q(v))\land \bigwedge_{j<i}\neg G_j(q(v)) \land \kappa_{t,v,a,w}=p_i(q(v)) \right). \)

This is a Boolean combination of polynomial conditions. Guard coverage is part of the input promise.

Candidate outcome probabilities

Set

\(\displaystyle P_t(v,w)=\sum_{a\in A(v)} x_t(v,a)\kappa_{t,v,a,w}.\)

Introduce \(g_{t,h,v,b}\) for horizons \(h\in\{0,\ldots,n\}\). If \(v\) is terminal with label \(\lambda(v)\), impose

\(\displaystyle g_{t,h,v,b}=\mathbf{1}_{\lambda(v)=b}\)

for every horizon. At a nonterminal state impose

\(\displaystyle g_{t,0,v,b}=0,\qquad g_{t,h,v,b}=\sum_w P_t(v,w)g_{t,h-1,w,b}\quad(h\geq1).\)

Induction on \(h\) shows that these are the probabilities of reaching each terminal label within \(h\) transitions. By the preceding termination bound,

\(\displaystyle g_{t,n,v_0,b}=D_t(x_t;q)(b).\)

Require \(g_{t,n,v_0,b}=F_t(b)\).

Incentive certificates

Write the prescribed target utility as

\(\displaystyle f_t=\sum_b F_t(b)u_t(b).\)

Reject immediately if any \(f_t<0\).

Introduce real variables \(W_{t,h,v}\). At terminals require

\(\displaystyle W_{t,h,v}=u_t(\lambda(v)).\)

At nonterminals require \(W_{t,0,v}=0\), and for every legal action and every positive horizon impose

\(\displaystyle W_{t,h,v}\geq \sum_w\kappa_{t,v,a,w}W_{t,h-1,w}. \)

Finally impose

\(\displaystyle W_{t,n,v_0}\leq f_t.\)

These constraints are sufficient: induction on the horizon shows that \(W_{t,h,v}\) bounds the expected terminal utility obtainable within that horizon under any strategy, assigning utility zero if termination has not yet occurred. Every deviation from \(v_0\) terminates within \(n\) transitions, so

\(\displaystyle U_t(y;q)\leq W_{t,n,v_0}\leq f_t=U_t(x_t;q).\)

They are also necessary. Given a feasible candidate, choose the \(W\)-variables to be the exact finite-horizon optimal values. They satisfy the displayed inequalities. At \(v_0\), the horizon-\(n\) optimum equals the optimum attained by a deterministic memoryless strategy, by Section 3. Feasibility therefore implies \(W_{t,n,v_0}\leq f_t\).

The resulting existential formula is consequently equivalent to feasibility on promised inputs.

5. Running-time bound and scope

Binary-encoded exponents cause no exponential expansion: compute each power by repeated squaring and introduce a variable for each arithmetic gate. Gate equations have degree at most two, and their number is polynomial in the original description length.

The outcome recurrences use \(O(\tau n^3m)\) arithmetic operations; the incentive inequalities use \(O(\tau n^3k)\). Kernel evaluation, guard selection, and input constants add polynomial overhead in \(L\). Hence, with

\(\displaystyle S=L+\tau n^3(m+k+1),\)

the existential-real sentence has length \(S^{O(1)}\).

The existential theory of the reals is decidable in polynomial space, by [Canny’s theorem](https://www2.eecs.berkeley.edu/Pubs/TechRpts/1988/6041.html). Its hypotheses apply here: all variables are real, all quantifiers are existential, and the remaining formula is a finite Boolean combination of rational polynomial equalities and inequalities. Applying that theorem gives polynomial space in \(S\), and therefore a deterministic time bound \(2^{S^{O(1)}}\).

The requested classification is thus settled as \(\mathrm{NP}\)-hard. The argument does not assert membership in \(\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

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

The output resolves the task. The hardness reduction is correct, and the additional existential-real upper bound is justified under the stated pathwise termination promise. I found no major or minor issues requiring repair.

The reduction uses the standard NP-hard decision problem of satisfiability for three-literal CNF formulas. Restricting to \(d\geq1\) does not affect hardness.

The falsity polynomials have the stated values on Boolean inputs. Every summand of \(R\) is nonnegative for every real vector. Consequently, \(R(z)=0\) forces each variable summand to vanish, giving \(z_i\in\{0,1\}\). Once these conditions hold, a clause summand vanishes precisely when some literal in that clause is true.

Thus the asserted equivalence between zeros of \(R\) and satisfying Boolean assignments is valid over the entire real domain. Repeated literals or clauses containing both signs of a variable do not invalidate it.

With one type of mass \(1\), the candidate’s initial action probabilities equal the aggregate coordinates. The substitution \(z_i=dq_i\) is valid because \(d\geq1\).

For every Boolean assignment, the displayed coordinates are nonnegative and sum to \(1\), including the case in which all variables equal \(1\) and \(q_0=0\). Conversely, if an admissible aggregate vector makes \(R(dq_1,\ldots,dq_d)=0\), the preceding zero-set argument produces a satisfying Boolean assignment.

The construction therefore establishes both required directions. It neither imposes rationality on candidate strategies nor introduces an additional population-composition variable.

Throughout the simplex, \(0\leq z_i\leq d\). For \(d\geq1\), both \(|z_i|\) and \(|1-z_i|\) are at most \(d\). Hence each variable summand is at most \(d^4\), and each clause summand is at most \(d^6\). Summing gives exactly the claimed bound \(R(z)\leq d^5+sd^6\).

A power of two of the stated bit length can be chosen above this positive bound. Therefore \(p\) and \(1-p\) are valid probabilities on the entire aggregate domain, not merely at encoded assignments. Their coefficients are binary-rational, and their degrees are at most six.

The initial state has no self-transition and sends every action directly to a labelled terminal. The specified terminal self-loops make those states absorbing. The mechanism satisfies the pathwise termination promise.

The two distinct alternative labels are compatible with zero valuations and payments: distinct alternatives need not have distinct utilities.

Because the initial transition row is independent of the individual’s action, the candidate’s probability of terminal label \(H\) is \(p(q)\). Zero utilities make individual rationality and every incentive comparison hold with equality, including deviations evaluated with the aggregate field fixed.

Thus exact implementation of \(\delta_G\) is equivalent to \(p(q)=0\). Together with the preceding checks, this proves the claimed satisfiability–feasibility equivalence.

The size calculation is also correct. A variable summand expands into three monomials. A squared three-literal product can be expanded as three squared affine factors, each with at most three monomials, giving at most \(27\) terms before combining duplicates. Substitution multiplies coefficients by powers of \(d\) of exponent at most six, so coefficient bit lengths remain polynomially bounded. Listing the entries separately for all \(d+1\) actions remains polynomial, including dense exponent-vector encoding.

This establishes NP-hardness with \(m=2\), \(\tau=1\), \(n=3\), and \(k=d+1\). It does not claim hardness with fixed \(k\), or membership in NP.

For fixed \(t\) and \(q\), the union graph includes precisely the transitions available with positive probability under some legal action. A strategy assigning positive probability to every legal action supports every edge of this graph.

A reachable nonterminal directed cycle would consequently support an infinite nonterminal path, contradicting the task’s promise. This reasoning correctly uses pathwise termination; the infinite path need not have positive probability as a singleton event.

Without a reachable nonterminal cycle, a supported trajectory cannot repeat a nonterminal state before termination. The bound of \(n\) transitions is therefore valid. Unreachable cycles are harmless because the conclusion concerns paths from \(v_0\).

The reverse-topological argument also establishes the asserted deterministic memoryless optimum on the reachable graph. Its comparison with history-dependent strategies supplies the equality needed later for the incentive certificates.

The candidate simplex constraints ensure an admissible aggregate field. The first-match formula correctly requires the selected guard to hold and all preceding guards to fail. Coverage and valid transition probabilities are supplied by the input promises.

The outcome recurrences have correct terminal and zero-horizon boundary conditions. Their horizon induction calculates terminal-label probabilities within the specified horizon. Pathwise termination then justifies identifying the horizon-\(n\) values at \(v_0\) with the full outcome lottery.

Consequently, the target equalities impose exactly the implementation requirement, including when \(v_0\) itself is terminal.

Once the target lottery is imposed, candidate utility equals \(f_t\). Rejecting a negative \(f_t\) is therefore exactly justified by interim individual rationality.

For sufficiency, the horizon inequalities propagate upper bounds because all transition coefficients are nonnegative. This remains valid for signed utilities. The zero boundary condition at nonterminals represents the explicitly stated zero payoff for failure to terminate within the truncated horizon.

Every deviation from \(v_0\) terminates by horizon \(n\), so the final bound implies the required incentive comparison.

For necessity, finite-horizon optimal values exist even at unreachable states and satisfy the displayed inequalities. At \(v_0\), the acyclic reachable graph makes the horizon-\(n\) optimum equal to the deterministic memoryless optimum established in Section 3. Feasibility against memoryless deviations therefore implies the required final inequality. No additional incentive condition at unreachable states is assumed.

Repeated squaring and auxiliary arithmetic-gate variables avoid expanding binary-encoded exponents. Gate equations have degree at most two and polynomial total description length. First-match guard expansion can incur polynomial duplication, which is absorbed by the stated \(S^{O(1)}\) bound.

The outcome and incentive operation counts are valid, with \(P_t\) computed once and reused. Rational constants retain polynomial encoding length.

The cited theorem applies to existential real sentences with Boolean combinations of polynomial comparisons; Canny’s original report confirms the polynomial-space decision result. [Canny’s report](https://www2.eecs.berkeley.edu/Pubs/TechRpts/1988/6041.html)

Applying it to the polynomial-length encoding gives polynomial space in \(S=L+\tau n^3(m+k+1)\). A halting deterministic polynomial-space computation has at most exponentially many configurations, yielding the claimed time bound \(2^{S^{O(1)}}\).

No additional clarification is needed. The NP-hardness conclusion and the promised-input upper bound both stand.

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