← back to the atlas

d4-conf-atal-2018-0203 (d4-conf-atal-2018-0203)

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

The anchor (named result in the paper)

Theorem 3.1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateMax-Min Fair Allocation is NP-hard even in an off-line setting with no restriction, with only 2 agents and in the homogeneous case, with furthermore ℓt (j,i) = ℓt (j) ∈{0, 1}. Note that these instances are trivial in the static case.

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

The continuous mirror question, as graded

Given a finite horizon \(T\), resident types \(i\) with rational masses \(\mu_i\), resource types \(j\) with per-capita supplies \(q_j\), time-dependent values \(v_{tij}\), and compatibility restrictions, optimize the sum of the per-period minimum utility and a stability reward. A feasible plan is a finite-support distribution \(x_{i,h}\) over histories \(h\), where each history gives each resident an integral bundle \(b_{t,j}(h)\), \(\sum_h x_{i,h}=\mu_i\), and \(\sum_{i,h}x_{i,h}b_{t,j}(h)=q_j\) at every time and for each resource type. The per-period minimum is taken over positive-mass histories, and stability counts the mass of resource copies retained by residents between consecutive periods.

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

A society is given by its support: the list of \(\tau\geq1\) resident types with positive binary-rational masses \(\mu_i\), normalized by \(\sum_i\mu_i=1\). Here \(\tau\) is the support size, not the number of possible types.
The offline input specifies \(T\geq2\) periods, \(m\geq1\) persistent resource types, constant per-capita supplies \(q_j\in\mathbb{Q}_{\geq0}\), values \(v_{tij}\in\mathbb{Q}_{\geq0}\), compatibility indicators \(a_{tij}\in\{0,1\}\), and a reward \(K\in\mathbb{Q}_{>0}\). Every positive-supply resource type has a compatible resident type at each period.
A history \(h\) for resident type \(i\) specifies bundles \(b_{t,j}(h)\in\mathbb{Z}_{\geq0}\), with \(b_{t,j}(h)=0\) whenever \(a_{tij}=0\). There is no additional bound on bundle size; empty bundles are allowed.
A plan assigns nonnegative real masses \(x_{i,h}\) to finitely many histories, satisfying \(\sum_hx_{i,h}=\mu_i\) and \(\sum_{i,h}x_{i,h}b_{t,j}(h)=q_j\) for every \(t,j\). Each history follows the same residents throughout the horizon.
Copies within a resource type are interchangeable; between adjacent periods, a resident retains \(\min\{b_{t,j}(h),b_{t+1,j}(h)\}\) copies, with remaining copies transferable.
Define \(F(x)=\sum_{t=1}^{T}\min_{i,h:x_{i,h}>0}\sum_{j=1}^{m}v_{tij}b_{t,j}(h)+K\sum_{t=1}^{T-1}\sum_{i,h}x_{i,h}\sum_{j=1}^{m}\min\{b_{t,j}(h),b_{t+1,j}(h)\}\).

Given a binary-rational threshold \(B\), is deciding whether a feasible finite-support plan satisfies \(F(x)\geq B\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,T,L\), where \(L\) is the total input bit length.

The discrete counterpart is \(\mathrm{NP}\)-hard even with two agents, no compatibility restrictions, and homogeneous values in \(\{0,1\}\); its static restriction is trivial. [Discrete hardness source](https://www.ifaamas.org/Proceedings/aamas2018/pdfs/p766.pdf)
No complexity result for this precise mass-and-history model 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}\)-hard, even when \(\tau=1\), all resources are compatible at every period, every supply is \(\tfrac12\), all values belong to \(\{0,1\}\), and \(K=1\).

The reduction below handles arbitrary real masses and unbounded integer bundles. Its yes-instances have witnesses consisting of just two constant histories.

1. Boolean source problem

A not-all-equal clause is satisfied when its literals include both a true literal and a false literal. We first establish hardness of not-all-equal satisfiability with three literals on distinct variables per clause.

Start from the standard \(\mathrm{NP}\)-complete problem \(\mathrm{3SAT}\); see [Schaefer’s satisfiability paper](https://doi.org/10.1145/800133.804350). We may assume that each clause has three distinct variables. Indeed, discard tautologies and remove repeated literals. A resulting two-literal clause \(a\lor b\) can be replaced by
\((a\lor b\lor u)\land(a\lor b\lor\neg u)\), with fresh \(u\). A unit clause \(a\) can be replaced by the four clauses \(a\lor u^{\epsilon}\lor v^{\delta}\), using all choices of signs on fresh \(u,v\). These replacements preserve satisfiability and increase size by only a constant factor.

Introduce one fresh global variable \(z\). Replace each original clause \(a\lor b\lor c\) by

\[ \operatorname{NAE}(a,b,s),\qquad \operatorname{NAE}(\neg s,c,z), \]

where \(s\) is fresh for that clause.

For fixed truth values of \(a,b,c,z\), these two clauses admit a choice of \(s\) exactly when \(a,b,c,z\) are not all equal:

An original satisfying assignment therefore extends to a satisfying not-all-equal assignment by setting \(z=0\). Conversely, complementing every variable preserves every not-all-equal clause. Thus any satisfying transformed assignment can be complemented, if necessary, so that \(z=0\). The equivalence just proved then implies that every original clause has a true literal.

Consequently, this not-all-equal problem is \(\mathrm{NP}\)-hard. Its clauses use three distinct variables.

2. Construction of the society

Let \(\Phi\) be such a not-all-equal instance, with variables \(y_1,\ldots,y_n\) and clauses \(C_1,\ldots,C_c\). Restricting to nonempty instances ensures \(n+2c\geq2\).

Create one resident type of mass \(\mu_1=1\). For each variable \(y_k\), create two persistent resource types \(j_k^+\) and \(j_k^-\). Set

\[ m=2n,\qquad q_j=\tfrac12,\qquad K=1, \]

and make every resource compatible at every period.

For a literal \(\ell\), let \(j(\ell)\) denote its corresponding resource: \(j(y_k)=j_k^+\) and \(j(\neg y_k)=j_k^-\).

There are \(T=n+2c\) periods:

All other values are zero. Set the threshold to

\[ B=T+n(T-1). \]

Every constructed input satisfies the hypotheses in the question.

3. Universal upper bound and its equality conditions

Fix any feasible finite-support plan. Since there is one resident type, write its positive history masses as \(x_h\), with \(\sum_hx_h=1\). Define the period minimum

\[ r_t=\min_{h:x_h>0}\sum_jv_{t1j}b_{t,j}(h). \]

Every history’s utility is an integer, so \(r_t\) is an integer. Feasibility gives its mass-weighted average as

\[ \sum_hx_h\sum_jv_{t1j}b_{t,j}(h) =\sum_jv_{t1j}q_j. \]

This average is one at a variable period and \(\tfrac32\) at either clause period. The minimum cannot exceed the average; hence, in every period,

\[ r_t\leq1. \]

Let \(R\) denote total retention, before multiplication by \(K\). The identity

\[ \min\{u,v\}=\frac{u+v-|u-v|}{2} \]

and the resource equalities imply

\[ R =n(T-1) -\frac12\sum_{t=1}^{T-1}\sum_hx_h \sum_j|b_{t,j}(h)-b_{t+1,j}(h)|. \]

Therefore \(R\leq n(T-1)\), and

\[ F(x)=\sum_tr_t+R\leq T+n(T-1)=B. \]

If \(F(x)\geq B\), every bound above must be tight: \(r_t=1\) for every period and \(R=n(T-1)\). Every summand in the retention deficit is nonnegative. Since each supported history has positive mass, equality forces

\[ b_{t,j}(h)=b_{t+1,j}(h) \]

for every supported history, resource, and adjacent pair of periods. Thus each supported history has a constant bundle throughout the horizon.

4. A threshold-achieving plan implies satisfiability

Suppose \(F(x)\geq B\). By the preceding section, every supported history has a constant bundle \(b_j(h)\), and every period minimum equals one.

At the variable period for \(y_k\), every supported history satisfies

\[ b_{j_k^+}(h)+b_{j_k^-}(h)\geq1. \]

The mass-weighted average of this sum is \(q_{j_k^+}+q_{j_k^-}=1\). Consequently every supported history satisfies equality:

\[ b_{j_k^+}(h)+b_{j_k^-}(h)=1. \]

Because the counts are nonnegative integers, each pair is either \((1,0)\) or \((0,1)\). This excludes all larger bundles without imposing an additional bundle bound.

Select any supported history and define \(y_k\) to be true exactly when \(b_{j_k^+}(h)=1\).

For a clause \(C_r=(\ell_1,\ell_2,\ell_3)\), its two periods require

\[ \sum_{a=1}^{3}b_{j(\ell_a)}(h)\geq1, \qquad \sum_{a=1}^{3}b_{j(\neg\ell_a)}(h)\geq1. \]

The variable-pair equalities make the second sum equal to three minus the first. Hence the first sum belongs to \(\{1,2\}\): the clause has both a true and a false literal. The selected history therefore yields a satisfying assignment for \(\Phi\).

5. Satisfiability implies a threshold-achieving plan

Conversely, let \(A\) satisfy \(\Phi\). Construct two constant histories, one encoding \(A\) and the other its global complement:

Every resource then has mass-weighted count \(\tfrac12=q_j\) at every period, so the plan is feasible.

At every variable period, both histories have utility one. At a clause period, the utilities are one and two, because \(A\) satisfies the not-all-equal clause and complementation reverses its literal truth values. The same holds for the complementary clause period. Thus every period minimum is one.

Each history retains its entire bundle of \(n\) resources across every transition. Therefore

\[ F(x)=T+n(T-1)=B. \]

Together with the previous section, this proves the equivalence

\[ \Phi\text{ is satisfiable} \quad\Longleftrightarrow\quad \text{a feasible finite-support plan satisfies }F(x)\geq B. \]

6. Running times and conclusion

The Boolean transformation increases the numbers of variables and clauses only linearly. The society construction has

\[ \tau=1,\qquad m=2n,\qquad T=n+2c. \]

Writing the dense value and compatibility tables takes \(O(m\tau T)\) time. Including reading the source instance and computing the threshold, the reduction takes \(O(L_{\Phi}+m\tau T)\) bit operations. Under the standard explicit table encoding, its output length satisfies \(L=O(mT+\log(mT))\). Thus the reduction is polynomial.

All numerical inputs except \(B\) are fixed constants, and \(B=O(mT)\). The hardness therefore does not depend on large numerical magnitudes.

For the constructed family, enumerating Boolean assignments gives an exact algorithm in \(O(L+2^{m/2}mT)\) time. For the general problem, an algorithm polynomial in \(m,\tau,T,L\) would imply \(\mathrm{P}=\mathrm{NP}\).

The requested classification is therefore \(\mathrm{NP}\)-hard.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The proof establishes the claimed \(\mathrm{NP}\)-hardness. The reduction respects the precise mass-and-history model, including arbitrary real masses, finite support, and unbounded integer bundles. No major or minor mathematical issues were found.

The decisive argument is valid: achieving the chosen threshold forces every supported history to have a constant bundle, and the variable-period constraints then force that bundle to encode a Boolean assignment.

Step-by-step verification

1. Boolean source problem

The external premise is the standard theorem that satisfiability of Boolean formulas in conjunctive normal form with three literals per clause is \(\mathrm{NP}\)-complete. The prover cites [Schaefer’s satisfiability paper](https://doi.org/10.1145/800133.804350).

The normalization to clauses with three distinct variables is correct:

Freshness ensures that every resulting clause has three distinct variables. The replacements increase the numbers of variables and clauses by at most a constant factor.

The not-all-equal transformation is also correct. The two cases given exhaust all possibilities for the truth values of \(a,b\):

Thus the stated equivalence with four values not all being equal holds. Setting \(z=0\) makes this condition equivalent to satisfaction of the original disjunction. Global complementation preserves not-all-equal satisfaction even for negated literals, because it reverses every literal’s truth value.

The transformation therefore establishes the required source hardness. Its fresh variables also preserve the distinct-variable condition.

2. Validity of the constructed input

The construction satisfies the task’s hypotheses:

Distinct variables in a clause guarantee that its three valued resources are distinct. Consequently, each clause-period average is indeed \(\tfrac32\). This hypothesis is used correctly.

3. Universal upper bound

Finite support and total mass \(1\) ensure that the supported histories form a nonempty finite set. Therefore each period minimum exists.

Every history utility is a nonnegative integer. Feasibility gives average utility \(1\) at a variable period and \(\tfrac32\) at a clause period. Since the minimum is an integer no larger than that average, the conclusion \(r_t\leq1\) is valid in both cases.

The retention identity is correct. For each resource and transition, both endpoint mass-weighted counts equal \(\tfrac12\). Applying the stated identity for the minimum therefore gives exactly
\(R=n(T-1)-\tfrac12\sum_{t,h,j}x_h|b_{t,j}(h)-b_{t+1,j}(h)|\).

All sums are finite, so there is no convergence or interchange-of-sums issue. The resulting bound \(F(x)\leq B\) is valid.

4. Equality conditions

If \(F(x)\geq B\), the universal upper bound forces equality. Each period deficit \(1-r_t\) and the retention deficit is nonnegative, so every deficit must vanish.

The retention deficit is a finite sum of nonnegative terms. Every supported history has strictly positive mass; hence its bundle difference must vanish for every resource and adjacent pair of periods.

It follows that every supported history has a constant bundle throughout the horizon. This inference remains valid for arbitrary real masses: no rationality or lower bound on positive masses is needed.

5. Extracting a satisfying assignment

At a variable period, minimum utility \(1\) implies that every supported history has variable-pair count at least \(1\). Its mass-weighted average is exactly \(1\).

Because all supported masses are positive, no supported history can have pair count strictly greater than \(1\). Thus every pair count equals \(1\). Nonnegative integrality then restricts each pair to \((1,0)\) or \((0,1)\).

This correctly excludes large bundles at the threshold without imposing an extra bundle-size restriction.

Selecting any supported history is legitimate. Its pair choices define a Boolean assignment. The two periods for each clause require at least one selected literal resource and at least one selected complementary literal resource. The pair equalities make these counts sum to \(3\), so the literal count belongs to \(\{1,2\}\). Every clause is therefore not-all-equal satisfied.

The soundness direction is fully established.

6. Constructing a threshold witness

The assignment and its global complement select opposite resources in every variable pair. Giving their constant histories mass \(\tfrac12\) satisfies every supply equality in every period.

Both histories have utility \(1\) at variable periods. At either period associated with a satisfied not-all-equal clause, their utilities are \(1\) and \(2\). Hence every period minimum equals \(1\).

Each history contains exactly \(n\) resources and retains them across every transition. The total retention is therefore \(n(T-1)\), and the objective equals \(B\).

The witness has two histories and satisfies the required finite-support condition. The completeness direction is fully established.

7. Complexity claims and scope

The source transformation is linear in the numbers of variables and clauses. The dense constructed tables contain \(m\tau T\) entries, all of constant bit length. The threshold has \(O(\log(mT))\) bits.

Accordingly, the stated reduction time \(O(L_{\Phi}+m\tau T)\) and constructed output-length bound \(L=O(mT+\log(mT))\) are consistent with the explicit encoding.

The enumeration bound \(O(L+2^{m/2}mT)\) is valid for deciding the threshold question on the constructed family: the proved equivalence reduces that decision to checking assignments to its \(m/2\) variables.

The prover correctly limits this algorithm to the constructed family. It does not claim a general exponential-time algorithm or membership in \(\mathrm{NP}\). Neither is required to establish the requested hardness classification.

Repair feedback

No repair is required. The proof settles the requested \(\mathrm{NP}\)-hardness alternative for the continuous model as stated.

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