← back to the atlas

d4-conf-aaai-2020-1736 (d4-conf-aaai-2020-1736)

Answer: \(\mathrm{NP}\)-complete under polynomial-time many-one reductions, already for \(\tau=1\), \(q_j=1\) for every item, and one hidden ReLU layer.

The anchor (named result in the paper)

Theorem 1 (MIP FORMULATION) — class: other

PDF text-layer excerpt — equations and symbol order may be approximateThe DNN-based WDP as defined in (OP1) is equivalent to the MIP defined in (OP2).

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

The continuous mirror question, as graded

Given \(m\) item categories, a finite support \(T\) of types with rational masses \(\mu_t\) summing to \(1\), rational per-capita supplies \(q_j\), and a fixed rational-weight ReLU network \(N_t:\{0,1\}^m\to\mathbb{Q}_{\ge 0}\) for each type, choose masses \(x_{t,b}\ge 0\) assigned to integral bundles \(b\in\{0,1\}^m\) to maximize \(\sum_{t\in T}\sum_{b\in\{0,1\}^m}x_{t,b}N_t(b)\), subject to \(\sum_b x_{t,b}=\mu_t\) for each \(t\) and \(\sum_{t,b}x_{t,b}b_j\le q_j\) for each item \(j\).

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

A society is given by its support: a list \(T\) of \(\tau\ge1\) types with positive binary-rational masses \(\mu_t\) summing to \(1\); \(\tau\) is the support size, not the number of possible types.
There are \(m\ge1\) item categories with nonnegative binary-rational per-capita supplies \(q_j\). Each individual receives an integral bundle \(b\in\{0,1\}^m\), including the empty bundle.
Each type has an explicitly supplied, fully connected feed-forward network \(N_t:\{0,1\}^m\to\mathbb{Q}_{\ge0}\), with arbitrary finite depth and width, signed rational weights and biases, and ReLU activation at every hidden layer and the scalar output. Its parameters are fixed during allocation; no monotonicity or empty-bundle normalization is assumed.
Masses may split between bundles. Define \(W^*:=\max_{x_{t,b}\in\mathbb{R}_{\ge0}}\sum_{t\in T}\sum_{b\in\{0,1\}^m}x_{t,b}N_t(b)\), subject to \(\sum_bx_{t,b}=\mu_t\) for every \(t\) and \(\sum_{t,b}x_{t,b}b_j\le q_j\) for every \(j\).
The input also contains a binary-rational threshold \(h\). Let \(S\) be the total network size, counting nodes and connections, and \(L\) the total binary input length, including architectures, coefficients, masses, supplies, and \(h\). State running times in \(m,\tau,S,L\).

Is deciding whether \(W^*\ge h\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finitely many bidders and unit item supplies, maximizing the sum of these network valuations over feasible integral allocations has an equivalent mixed integer linear formulation ([Weissteiner–Seuken, 2020](https://cdn.aaai.org/ojs/5606/5606-13-8831-1-10-20200512.pdf)); this formulation alone supplies no polynomial-time guarantee.
No result settling the exact mass-allocation problem with explicitly supplied rational ReLU networks 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 decision problem is \(\mathrm{NP}\)-complete under polynomial-time many-one reductions. Hardness holds already when \(\tau=1\), every supply is \(q_j=1\), and the valuation network has one hidden layer and only integer coefficients of constant magnitude.

Thus a polynomial-time algorithm exists if and only if \(\mathrm{P}=\mathrm{NP}\).

1. A direct reduction from satisfiability

Let \(F=C_1\land\cdots\land C_k\) be a 3-CNF formula on \(m\) Boolean variables, with \(m,k\ge1\). A bundle \(b\in\{0,1\}^m\) represents a truth assignment. For a literal \(\ell\), define its truth value by

\(\ell(b)=b_j\) if \(\ell\) is the positive literal on variable \(j\), and \(\ell(b)=1-b_j\) if it is the negative literal.

Write \(\rho(z)=\max\{0,z\}\). Construct one hidden neuron for each clause:

\[ \]
\(u_i(b)=\rho\!\left(1-\sum_{\ell\in C_i}\ell(b)\right).\)

The preactivation is affine in the inputs, so it is implemented directly by rational weights and a bias. Since each clause has at most three literals, all these coefficients are integers of constant magnitude. Every input is connected to every hidden neuron; connections not used by a clause have weight zero.

For a Boolean input, the sum of literal truth values is an integer. Consequently,

\(u_i(b)=1\) when \(C_i\) is unsatisfied, and \(u_i(b)=0\) when \(C_i\) is satisfied.

Use the scalar ReLU output

\(N(b)=\rho\!\left(1-\sum_{i=1}^{k}u_i(b)\right).\)

This gives exactly

\(N(b)=1\) if \(b\) satisfies \(F\), and \(N(b)=0\) otherwise.

The output is connected to every hidden neuron with weight \(-1\), and its bias is \(1\). The resulting network satisfies all the architectural requirements and has size \(S=O(mk+m+k)\). Its explicit binary encoding has length polynomial in the formula length.

Construct the allocation instance with one supported type, mass \(\mu_1=1\), supplies \(q_j=1\) for all \(j\), and threshold \(h=1\).

For every nonnegative allocation satisfying \(\sum_b x_{1,b}=1\), each supply constraint holds automatically:

\(\sum_b x_{1,b}b_j\le\sum_b x_{1,b}=1=q_j.\)

Therefore the feasible allocations are precisely probability distributions over bundles. Their welfare is a weighted average of the bundle values, so

\(W^*=\max_{b\in\{0,1\}^m}N(b).\)

The upper bound follows because an average cannot exceed its largest constituent value. Equality follows by assigning the entire mass to a maximizing bundle. Hence

\(W^*\ge1\quad\Longleftrightarrow\quad F\text{ is satisfiable}.\)

This is a polynomial-time reduction from the \(\mathrm{NP}\)-complete problem 3-SAT. It proves \(\mathrm{NP}\)-hardness and explicitly handles arbitrary splitting of mass.

2. Exact network evaluation has polynomial bit complexity

To establish membership in \(\mathrm{NP}\), we first bound the cost of evaluating a supplied network on a specified bundle.

Every coefficient has absolute value at most \(2^L\), and each neuron has at most \(S\) incoming connections. Starting from Boolean inputs, a topological induction bounds the absolute value of every preactivation and activation by

\(M=\bigl((S+1)2^L\bigr)^S.\)

Indeed, an affine combination of at most \(S\) preceding values, followed by a ReLU, increases the bound by at most the factor \((S+1)2^L\).

Let \(D_N\) be the product of the denominators of all coefficient occurrences in the network. Its binary length is \(O(L)\). For a fixed input, replace each ReLU by either the identity or zero according to its evaluated preactivation. Expanding the resulting affine computation expresses each node value as a sum of terms corresponding to directed paths. Each term uses each coefficient occurrence at most once, because the network is feed-forward. Its denominator therefore divides \(D_N\), and so does the denominator of the sum.

Combining this denominator bound with the magnitude bound shows that every node value has numerator and denominator of bit length at most

\(B=O\!\left(L+S\bigl(L+\log(S+1)\bigr)\right).\)

The same argument applies to intermediate affine partial sums. Exact rational arithmetic, reducing fractions after each operation, therefore evaluates a specified bundle in time polynomial in \(m,S,L\). In particular, arbitrary depth does not cause exponentially long evaluation results.

3. Polynomial-size allocation certificates

Put \(r=\tau+m\), and introduce nonnegative supply slacks \(s_j\). The allocation constraints become

\(\sum_b x_{t,b}=\mu_t\) for every \(t\), and

\(\sum_{t,b}b_jx_{t,b}+s_j=q_j\) for every \(j\).

Write this system as \(Ay=d\), \(y\ge0\), where \(y\) contains the allocation variables and slacks. Every entry of \(A\) is zero or one.

The system is feasible: assign every type its mass on the empty bundle and set \(s_j=q_j\). Its feasible set is compact, since

\(0\le x_{t,b}\le\mu_t\) and \(0\le s_j\le q_j.\)

Thus the welfare objective attains a maximum.

A maximizing solution uses at most \(r\) positive variables

Choose an optimal solution \(y\) having the fewest positive coordinates. Suppose that the columns of \(A\) corresponding to those coordinates are linearly dependent. Then there is a nonzero vector \(z\), supported on those coordinates, with \(Az=0\).

For sufficiently small positive \(\varepsilon\), both \(y+\varepsilon z\) and \(y-\varepsilon z\) remain nonnegative and satisfy the equality constraints. If \(c\) is the welfare coefficient vector, optimality forces \(c^\mathsf{T}z=0\); otherwise one of these perturbations would improve welfare.

After changing the sign of \(z\) if necessary, it has a positive coordinate. Set

\(\varepsilon_*=\min_{i:z_i>0}y_i/z_i.\)

Then \(y-\varepsilon_*z\) is feasible, has the same welfare, and has fewer positive coordinates. This contradicts the choice of \(y\).

The supported columns are therefore linearly independent. Since \(A\) has \(r\) rows, there are at most \(r\) positive coordinates, including slacks. In particular, at most \(r\) type–bundle pairs receive positive mass.

The masses have polynomial-length rational encodings

The matrix \(A\) has row rank \(r\). Indeed, the empty-bundle column for each type and the \(m\) slack columns together form an identity matrix.

Extend the independent columns supporting \(y\) to an invertible \(r\)-by-\(r\) submatrix \(A_0\). Give the added coordinates value zero. The selected coordinates are then the unique solution of

\(A_0y_0=d.\)

Let \(D\) be the product of the denominators in \(d\), and put \(a=Dd\). The integer \(D\) has bit length \(O(L)\), and every entry of \(a\) has absolute value at most \(2^{2L}\).

Cramer’s rule gives each selected coordinate as

\((y_0)_i=\det(A_0^{(i)})/(D\det(A_0)),\)

where \(A_0^{(i)}\) replaces column \(i\) of \(A_0\) by \(a\).

By the determinant expansion,

\(|\det(A_0)|\le r!\) and \(|\det(A_0^{(i)})|\le r!\,2^{2L}.\)

Thus every positive allocation mass has numerator and denominator of bit length

\(O\!\left(L+r\log(r+1)\right).\)

These witness masses may be general rationals, even if the input masses and supplies are dyadic.

Verification

For every yes-instance, the optimal allocation supplies a certificate listing at most \(r\) type–bundle pairs and their rational masses. Its total encoding length is at most

\(O\!\left(r\left[m+\log(\tau+1)+L+r\log(r+1)\right]\right).\)

A verifier checks nonnegativity, every type-mass equality, every supply inequality, and the welfare threshold. It evaluates the listed networks exactly using Section 2.

All checks take time polynomial in \(m,\tau,S,L\). Conversely, any accepted certificate specifies a feasible allocation of welfare at least \(h\). Therefore the decision problem belongs to \(\mathrm{NP}\).

Together with Section 1, this proves \(\mathrm{NP}\)-completeness.

4. Running times and interpretation

Enumerating all bundles produces an explicit rational linear program with \(\tau2^m\) allocation variables and \(\tau+m\) allocation constraints. Section 2 bounds every generated welfare coefficient by polynomial bit length. Applying polynomial-time exact rational linear programming therefore gives a deterministic running time of

\(2^{O(m)}\operatorname{poly}(m,\tau,S,L).\)

In particular, the problem is polynomial-time solvable when \(m\) is fixed. When \(m\) is part of the input, the hardness reduction rules out a polynomial-time algorithm unless \(\mathrm{P}=\mathrm{NP}\), even for fixed support size \(\tau=1\).

The related [Weissteiner–Seuken mixed-integer formulation](https://cdn.aaai.org/ojs/5606/5606-13-8831-1-10-20200512.pdf) concerns discrete winner determination. The reduction above establishes hardness directly for the stated mass-allocation problem.

⟨structured verdict parsed — rendered above⟩

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

The proof resolves the task correctly. The reduction establishes hardness for the exact mass-allocation problem, and the certificate argument establishes membership in \(\mathrm{NP}\). No major or minor mathematical issues were found.

1. Scope and claimed result

The prover addresses the stated model: explicitly supplied rational ReLU networks, integral bundles, continuous splitting of type masses, and supply inequalities. It establishes \(\mathrm{NP}\)-completeness, which strengthens the requested \(\mathrm{NP}\)-hardness conclusion.

The restricted hardness instance respects every input requirement: \(m\ge1\), \(\tau=1\), positive mass \(\mu_1=1\), nonnegative supplies \(q_j=1\), and a rational threshold \(h=1\).

2. Satisfiability reduction

Clause neurons. For each Boolean bundle, every literal truth value belongs to \(\{0,1\}\). Thus the sum of clause literal values is a nonnegative integer. The expression \(u_i(b)=\rho(1-\sum_{\ell\in C_i}\ell(b))\) equals one precisely when every literal is false, and zero otherwise. This calculation is correct.

Expanding the literal expressions gives an affine preactivation with integer coefficients of constant magnitude. Repeated literals, if allowed in the chosen 3-SAT representation, do not invalidate either the evaluation or the constant bound: each clause contains at most three literal occurrences.

Output neuron. The sum of the hidden activations counts unsatisfied clauses. Consequently, \(N(b)=\rho(1-\sum_i u_i(b))\) equals one when there are none and zero when there is at least one. The scalar output uses ReLU as required, and its values are nonnegative.

Architecture and construction size. Zero-weight connections satisfy the fully connected architecture requirement. Counting all input-to-hidden connections gives the claimed size \(S=O(mk+m+k)\). The explicit construction and coefficient encoding have polynomial size.

Allocation constraints. With one type of mass one, each supply constraint follows from \(b_j\le1\) and nonnegative allocation masses. Therefore every distribution over bundles is feasible. Welfare is a weighted average of the finitely many network values, and concentrating all mass on a maximizing bundle attains their maximum.

Hence \(W^*\ge1\) holds exactly when the formula is satisfiable. Both directions are established, including the possibility of arbitrary mass splitting. The invocation of 3-SAT’s \(\mathrm{NP}\)-completeness is applicable.

3. Exact network evaluation

Magnitude bound. The input length bounds each coefficient’s magnitude by \(2^L\). With at most \(S\) incoming connections per neuron, the factor \((S+1)2^L\) accounts for the weighted inputs and bias. Induction through at most \(S\) computational nodes yields the stated bound \(M=((S+1)2^L)^S\). ReLU cannot increase absolute magnitude.

Denominator bound. The product \(D_N\) of coefficient-occurrence denominators has binary length \(O(L)\). For a fixed input, replacing each ReLU by its actual identity-or-zero branch is valid. In the resulting affine expansion, feed-forward acyclicity prevents a directed path from using a coefficient occurrence more than once. Each term’s denominator therefore divides \(D_N\), and the denominator of the sum does also.

Bias contributions are covered by the same affine expansion. Signed coefficients and cancellation do not invalidate this denominator-divisibility claim.

Bit length and arithmetic. Combining the denominator bound with the magnitude bound gives \(B=O(L+S(L+\log(S+1)))\). Affine partial sums satisfy the same kind of bound. Reducing fractions after arithmetic operations consequently keeps operand lengths polynomial; temporary products and sums also have polynomial length. The polynomial-time exact evaluation conclusion follows.

4. Allocation certificates

Feasibility and attainment. Assigning each type to the empty bundle provides a feasible allocation regardless of its valuation. The bounds on allocation variables and slacks are correct. The feasible set is also closed, since it is defined by finitely many linear equalities and nonnegativity inequalities. Thus the compactness and maximum-attainment claims are justified.

Sparse optimal solution. Choosing an optimum with the fewest positive coordinates is legitimate because the number of coordinates is finite. If its supported columns were dependent, a nonzero supported null vector would permit sufficiently small feasible perturbations in both directions.

Optimality forces the objective’s directional coefficient to vanish. The stated endpoint perturbation then preserves feasibility and welfare while making at least one positive coordinate zero. Coordinates outside the support stay zero, and coordinates corresponding to negative entries of the perturbation vector increase. The contradiction is valid.

Therefore an optimum has at most \(r=\tau+m\) positive variables, including slacks.

Rational mass bounds. The empty-bundle columns and slack columns form an identity submatrix, so the asserted full row rank is correct. Extending the supported independent columns to an invertible square submatrix is justified.

The Cramer’s-rule expression correctly includes the factor \(D\) in the denominator. Since each determinant-expansion term contains at most one entry from the replacement column, the bounds \(|\det(A_0)|\le r!\) and \(|\det(A_0^{(i)})|\le r!2^{2L}\) are valid. The resulting rational mass encodings have the claimed polynomial length.

Allowing general rational witness masses is appropriate: the optimization variables are real, and the input’s binary-rational restriction does not restrict certificates to dyadic masses.

Verification. The certificate lists sufficiently many bits to identify types, bundles, and masses. All mass equalities, supply inequalities, and the welfare threshold can be checked exactly in polynomial time using the established evaluation bound. Accepted certificates describe feasible allocations, and every yes-instance has such a certificate. Membership in \(\mathrm{NP}\) follows.

5. Running times and conclusion

The enumerated linear program has \(\tau2^m\) allocation variables, polynomially bounded coefficient bit lengths, and a feasible bounded region. These satisfy the hypotheses of polynomial-time rational linear programming. Polynomial dependence on the explicit program length yields \(2^{O(m)}\operatorname{poly}(m,\tau,S,L)\).

The fixed-\(m\) polynomial-time conclusion and unrestricted \(\mathrm{NP}\)-completeness conclusion are consistent. The cited mixed-integer formulation is contextual; neither hardness nor membership depends on it.

No additional clarification is required to make the mathematical argument verifiable.

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