Answer: \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions; therefore \(\mathrm{NP}\)-hard under polynomial-time Turing reductions. It is in \(\mathrm{P}\) if and only if \(\mathrm{P}=\mathrm{NP}\).
Proposition 2 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateNASH OUTCOME VERIFICATION is co-NP- complete, even for two player games with τ = τ0 and where c assigns no costs. PROOF. Membership is immediate. For hardness, we reduce SAT to the complement problem. Given an instance ϕ of SAT over variables x1, . . . , xk, define a game G with Ag = {1, 2}, Φ = {x1, . . . , xk, z}, (where z does not occur in ϕ), Φ1 = {x1, . . . , xk}, Φ2 = {z}, γ1 = ϕ, γ2 = z, let v1(y) = ⊥for all y ∈Φ1, and let v2(z) = ⊤.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite list of household types with rational population masses, Boolean action sets, goal formulas, costs and taxes, together with a rational mass profile over actions, determine whether the profile is a Wardrop equilibrium: every action used by positive mass must be a best response when an individual deviation leaves the aggregate state fixed.
A society is given by its support: the list of the \(\tau\) household types with positive mass \(w_t\), each a binary rational, with \(\sum_t w_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The input includes a nonempty Boolean vocabulary \(\Phi\), with \(m=|\Phi|\), partitioned into possibly empty blocks \(\Phi_t\). Type \(t\) has all assignments \(A_t=\{0,1\}^{\Phi_t}\) as actions, represented implicitly, and a propositional goal formula \(\gamma_t\) over \(\Phi\).
Costs \(c(p,b)\) and taxes \(h(p,b)\), for \(p\in\Phi\) and \(b\in\{0,1\}\), are explicitly given nonnegative binary rationals. An action has expense \(d_t(a)=\sum_{p\in\Phi_t}[c(p,a(p))+h(p,a(p))]\).
The given profile explicitly lists positive binary rational masses \(x_{t,a}\), with omitted entries zero and \(\sum_{a\in A_t}x_{t,a}=w_t\). Let \(K\) be the number of listed entries and \(L\) the total input bit length.
For \(p\in\Phi_s\), define the aggregate Boolean value \(B_p(x)=1\) exactly when \(\sum_{a\in A_s:a(p)=1}x_{s,a}\geq w_s/2\); ties therefore give truth.
When type \(t\) considers action \(a\), evaluate \(\gamma_t\) using \(a(p)\) on \(\Phi_t\) and \(B_p(x)\) elsewhere. Preferences first maximize goal satisfaction, then minimize expense; ties are permitted. An individual deviation changes its own assignment but leaves \(x\) fixed.
The profile is a Wardrop equilibrium exactly when every \(a\) with \(x_{t,a}>0\) is a best response among all \(A_t\) at this fixed aggregate.
Is deciding whether the given profile is a Wardrop equilibrium in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard under polynomial-time Turing reductions? State running times in \(m,\tau,K,L\).
Discrete pure Nash outcome verification is \(\mathrm{coNP}\)-complete, even with two players and zero costs and taxes ([2011 result](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2011b.pdf)); the [2013 extended treatment](https://www.lamsade.dauphine.fr/~lang/papers/wekl-aij13.pdf) establishes hardness even with one player.
No result settling this precise continuous verification problem was located in the literature search.
Result
Deciding whether the supplied profile is a Wardrop equilibrium is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, even when \(\tau=K=1\) and all costs and taxes are zero. Consequently, it is \(\mathrm{NP}\)-hard under polynomial-time Turing reductions and belongs to \(\mathrm{P}\) if and only if \(\mathrm{P}=\mathrm{NP}\).
The hardness also persists for two types with nonempty blocks and a genuinely mixed profile. The proof below uses the stated continuous model directly.
1. Exact comparison of actions
Write \(n_t=|\Phi_t|\), so that \(\sum_{t=1}^{\tau}n_t=m\). After computing the aggregate \(B(x)\), define \(s_t(a)\in\{0,1\}\) as the truth value of \(\gamma_t\) under the valuation that uses \(a\) on \(\Phi_t\) and \(B(x)\) elsewhere.
By the specified preferences, an action \(b\in A_t\) is strictly preferred to an action \(a\in A_t\) exactly when
\[ s_t(b)>s_t(a) \quad\text{or}\quad \bigl(s_t(b)=s_t(a)\ \text{and}\ d_t(b)<d_t(a)\bigr). \]
Thus, the profile fails to be an equilibrium exactly when there are a type \(t\), a listed action \(a\) of that type, and an action \(b\in A_t\) satisfying this condition. This equivalence follows directly from the equilibrium definition: a supported action is a best response precisely when no action is strictly preferred to it. Equal satisfaction and equal expense permit a tie.
All these comparisons can be performed exactly in polynomial time. To see this explicitly, represent each input rational as an integer numerator divided by a positive integer denominator, and let \(D\) be the product of all input denominators. Its bit length is \(O(L)\), because the denominators’ total encoded length is at most \(L\). Scaling every rational by \(D\) produces integers of \(O(L)\) bits. Sums of at most \(O(L)\) such integers still have \(O(L)\) bits.
Using elementary integer arithmetic, computing \(D\) and all scaled quantities takes \(O(L^3)\) bit operations. For each \(p\in\Phi_s\), compute
\[ M_p=\sum_{\substack{a\text{ listed for }s\\a(p)=1}}Dx_{s,a}. \]
Then \(B_p(x)=1\) exactly when \(2M_p\geq Dw_s\), which handles ties exactly as required. At most \(Km\) contributions need processing. Formula evaluation and expense comparison for any specified action take \(O(L^2)\) bit operations, a conservative bound that includes assignment lookup and arithmetic.
For convenience, define the polynomial bound
\[ P_0(m,\tau,K,L) = O\!\left((L+Km+K+m+\tau)L^2\right). \]
It bounds aggregate computation, evaluation of all listed actions, and verification of one proposed deviation.
2. Membership in \(\mathrm{coNP}\)
A certificate of failure consists of:
Its length is \(O(m+\log K+\log\tau)\). The verifier computes \(B(x)\), evaluates \(s_t(a)\) and \(s_t(b)\), computes their expenses, and checks the strict-preference condition above. It accepts exactly when the certificate exhibits a profitable deviation.
The verification time is \(P_0(m,\tau,K,L)\). Since the vocabulary, types, and profile entries are explicitly represented, \(m,\tau,K=O(L)\); hence this bound is polynomial in the input length. Non-equilibrium therefore belongs to \(\mathrm{NP}\), and equilibrium verification belongs to \(\mathrm{coNP}\).
3. Hardness with one type and one listed action
Let \(\varphi\) be an arbitrary propositional formula, and let \(X\) be its variable set. Introduce a fresh variable \(z\). Construct the following instance:
This is a valid instance with \(K=1\) and a nonempty vocabulary. Its encoding size is polynomial in the encoding size of \(\varphi\).
The supported action fails the goal because \(a^0(z)=0\). Moreover, the type controls every variable. Consequently, when it considers an action \(b\), the entire goal is evaluated under \(b\); there are no external coordinates on which the fixed aggregate could affect satisfaction.
If \(\varphi\) is satisfiable, extend a satisfying assignment by setting \(z=1\). The resulting action satisfies \(\gamma_1\), so it is strictly preferred to \(a^0\).
If \(\varphi\) is unsatisfiable, every action fails \(\gamma_1\). Every action also has expense zero. Hence all actions are tied best responses, including \(a^0\), and the profile is an equilibrium.
We have therefore proved
\[ \varphi\in\mathrm{UNSAT} \quad\Longleftrightarrow\quad I(\varphi)\text{ is a Wardrop equilibrium}. \]
This is a polynomial-time many-one reduction from the \(\mathrm{coNP}\)-complete problem \(\mathrm{UNSAT}\). Together with Section 2, it proves \(\mathrm{coNP}\)-completeness.
The fresh-variable construction also appears in Proposition 1 of the [2013 discrete Boolean-game treatment](https://www.lamsade.dauphine.fr/~lang/papers/wekl-aij13.pdf). The argument here verifies its applicability to the precise fixed-aggregate deviation rule in this question.
4. Hardness also holds for genuinely mixed profiles
The preceding restriction is sufficient for hardness, but the conclusion does not depend on having a pure profile or only one type.
Starting from \(\varphi\) over \(X\), introduce fresh variables \(z,r,q\), and construct:
Both blocks are nonempty, both types mix between distinct actions, and \(\tau=2\), \(K=4\). The aggregate ties on \(r\) and \(q\) give truth, but neither affects type \(1\)’s goal. Type \(2\)’s goal is always true.
If \(\varphi\) is satisfiable, type \(1\) has a goal-satisfying deviation from either supported action. If it is unsatisfiable, all type \(1\) actions fail its goal and have equal expense; all type \(2\) actions satisfy its goal and have equal expense. Thus this mixed profile is an equilibrium exactly when \(\varphi\) is unsatisfiable.
5. Deterministic running time and the requested reduction
An explicit deterministic algorithm first computes the aggregate and then, for each type \(t\), enumerates its \(2^{n_t}\) actions. It retains a best action under the satisfaction-first, expense-second comparison and checks that every listed action ties with it.
This algorithm is correct because the action set is finite and the comparison orders all actions, allowing ties. Its bit running time is
\[ O\!\left( \left[ L+Km+K+m+\tau+\sum_{t=1}^{\tau}2^{n_t} \right]L^2 \right). \]
Empty blocks cause no difficulty: their action set contains exactly the empty assignment.
For nonnegative integers \(a,b\),
\[ 2^{a+b}+1-2^a-2^b = (2^a-1)(2^b-1) \geq 0. \]
Repeated application, using \(\sum_t n_t=m\), gives
\[ \sum_{t=1}^{\tau}2^{n_t}\leq 2^m+\tau-1. \]
Hence a bound stated solely in the requested parameters is
\[ O\!\left((L+Km+K+m+\tau+2^m)L^2\right). \]
Finally, a satisfiability algorithm can construct \(I(\varphi)\), make one query to an equilibrium-verification oracle, and negate its answer. Therefore \(\mathrm{SAT}\), and consequently every language in \(\mathrm{NP}\), polynomial-time Turing reduces to this verification problem. This establishes the requested \(\mathrm{NP}\)-hardness without asserting \(\mathrm{NP}\)-hardness under many-one reductions.
⟨structured verdict parsed — rendered above⟩
The prover’s output fully resolves the task. The reduction uses the specified fixed-aggregate deviation rule correctly, the certificate argument establishes membership in \(\mathrm{coNP}\), and the stated running-time bounds are valid. I found no mathematical gaps or false claims.
The strict-preference condition correctly implements the stated lexicographic preferences: goal satisfaction takes priority over expense, and expense matters only when satisfaction agrees.
Every action set is finite and nonempty, including when its block is empty. Consequently, a supported action is a best response exactly when no action is strictly preferred to it. The characterization of non-equilibrium therefore has the correct quantifiers: one type, one positively supported action, and one profitable alternative suffice. Omitted profile entries need not be checked as incumbent actions.
The common-denominator construction is valid. The bit length of the product of all input denominators is bounded by their total encoded length, hence by \(O(L)\). Scaling an input rational by this product yields an integer of \(O(L)\) bits. Summing at most \(O(L)\) such integers adds only \(O(\log L)\) bits, preserving the \(O(L)\) bound.
The claimed \(O(L^3)\) preprocessing bound is conservative and valid with elementary integer arithmetic. There are \(O(L)\) input rationals, and each multiplication or exact division involves integers of \(O(L)\) bits.
The test \(2M_p\geq Dw_s\) is exactly equivalent to the required majority comparison. In particular, equality produces truth. Counting at most \(Km\) contributions is a valid upper bound.
Formula evaluation and expense computation for a specified action fit within the stated \(O(L^2)\) bound. Thus
\(P_0(m,\tau,K,L)=O((L+Km+K+m+\tau)L^2)\)
safely bounds the operations attributed to it.
The proposed certificate explicitly identifies a supported action and supplies the alternative assignment. Its length is polynomial: the assignment uses at most \(m\) bits, and the two indices require logarithmic space.
The verifier can check that the indices designate a listed action of the stated type, evaluate both actions against the same aggregate, and compare their expenses exactly. Its acceptance condition is precisely a profitable deviation.
Completeness also holds: if the profile is not an equilibrium, the characterization in Section 1 guarantees such a certificate. Because the vocabulary, types, and profile entries are explicit, \(m,\tau,K=O(L)\). The verifier’s bound is therefore polynomial in the input length.
The construction satisfies every input requirement:
The supported action fails the goal because its fresh variable is false. Since the type controls every variable, evaluating an alternative action uses that action everywhere; the aggregate has no external coordinates to supply.
Both reduction directions are correct. A satisfying assignment of the source formula gives a goal-satisfying alternative. If the source formula is unsatisfiable, every action fails the goal and has zero expense, so every action is a best response.
Hence the displayed equivalence with \(\mathrm{UNSAT}\) is correct and establishes \(\mathrm{coNP}\)-hardness under polynomial-time many-one reductions. Together with membership, it establishes the claimed completeness.
The attribution is also accurate: Proposition 1 of the [2013 treatment](https://www.lamsade.dauphine.fr/~lang/papers/wekl-aij13.pdf) uses the corresponding one-player construction with a fresh variable, an all-false outcome, and zero costs and taxes. The continuous reduction is nevertheless verified directly in the submitted argument.
Each type’s two supported masses sum to its mass of one-half. The actions are distinct because they differ on the fresh mixing coordinate. Both blocks are nonempty, including when the source variable set is empty.
The aggregate values on the mixing coordinates are indeed true by the tie rule. Those coordinates cannot affect the first type’s goal, and the second type’s goal is a tautology.
If the source formula is satisfiable, either supported action of the first type admits a satisfying alternative. If it is unsatisfiable, all actions of that type tie, while all actions of the second type also tie. The claimed equilibrium equivalence and the constants \(\tau=2\), \(K=4\) are correct.
Enumerating each type’s actions and retaining a best action is valid under the stated total preference comparison with ties. Checking every supported action against that best action is sufficient and necessary.
The enumeration count is \(\sum_t2^{n_t}\), and an empty block contributes exactly one action. The displayed algebraic identity is correct for all nonnegative integer block sizes. Its repeated application gives the claimed bound \(\sum_t2^{n_t}\leq2^m+\tau-1\), including when some blocks are empty.
The resulting deterministic running time
\(O((L+Km+K+m+\tau+2^m)L^2)\)
is valid.
Negating the equilibrium oracle’s answer on the constructed instance correctly decides satisfiability. This establishes the requested polynomial-time Turing hardness, without confusing it with many-one \(\mathrm{NP}\)-hardness.
The statement that the verification problem belongs to \(\mathrm{P}\) exactly when \(\mathrm{P}=\mathrm{NP}\) follows from the established completeness and reduction.
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.