Answer: \(\mathrm{NP}\text{-hard}\), already for always-feasible instances with one type, one resource, and a satisfiable normal program; \(\mathrm{NP}\text{-complete}\) when all programs are normal.
Theorem 1 — class: algorithmic
Given finitely many types \(T\) with rational masses \(\mu_t\), a local ASP program for each type with feasible integral packages \(\mathcal S_t\), package resource vectors \(h_{t,S}\), weighted scores \(u_t(S)\), and rational per-capita resource bounds \(b\), compute a feasible allocation \(x_{t,S}\ge 0\) minimizing \(\sum_{t\in T}\sum_{S\in\mathcal S_t}x_{t,S}u_t(S)\), subject to \(\sum_{S\in\mathcal S_t}x_{t,S}=\mu_t\) and \(\sum_{t,S}x_{t,S}h_{t,S}\le b\), or report infeasibility.
A society is given by its support: a list \(T\) of \(\tau\ge1\) 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.
For each type, the input contains a finite ground normal or disjunctive ASP program \(P_t\) over an atom set \(A_t\); its integral packages are \(\mathcal S_t=\operatorname{SM}(P_t)\), represented implicitly by \(P_t\). No satisfiability promise is imposed.
The score is \(u_t(S)=\sum_{(w,\ell)\in E_t,\ S\models\ell}w\), where \(E_t\) is an input list of weighted literals and \(w\in\mathbb Q\); smaller scores are preferred, with equal scores tied.
There are \(r\ge1\) resources. Polynomial-size input Boolean circuits, evaluated on the characteristic vector of \(S\), output binary-rational vectors \(h_{t,S}\in\mathbb Q_{\ge0}^r\); bounds \(b\in\mathbb Q_{\ge0}^r\) are per capita.
An allocation assigns real masses \(x_{t,S}\ge0\), satisfying \(\sum_{S\in\mathcal S_t}x_{t,S}=\mu_t\) and \(\sum_{t,S}x_{t,S}h_{t,S}\le b\) componentwise. Compute one minimizing \(\sum_{t,S}x_{t,S}u_t(S)\), or report infeasibility; represent the answer by its positive-mass packages and rational masses.
Let \(m=|\bigcup_t A_t|\) and let \(L\) be the total binary input length, including programs, circuits, weights, masses, and bounds.
Is this exact allocation problem solvable in time polynomial in \(m,\tau,r,L\), or is deciding whether a feasible allocation has objective at most an input binary rational \(q\) NP-hard?
Discrete: successive ASP solves compute a preferred stable model for any strict partial-order preference, or detect unsatisfiability; this is a correctness guarantee, not a polynomial-time bound ([source](https://ojs.aaai.org/index.php/AAAI/article/download/9398/9257)).
Continuous: no result for this exact implicit-package mass-allocation problem was identified in the literature search.
The decision problem is \(\mathrm{NP}\)-hard, even with one type, one resource, a satisfiable normal program, and an allocation instance that is always feasible. All numerical data in the reduction are constants.
Consequently, computing an exact optimal allocation in time polynomial in \(m,\tau,r,L\) would imply \(\mathrm{P}=\mathrm{NP}\). For normal programs, the decision problem is also in \(\mathrm{NP}\), hence is \(\mathrm{NP}\)-complete.
The absence of a satisfiability promise already permits hardness through stable-model existence. The proof below establishes the stronger result with both program satisfiability and allocation feasibility guaranteed.
Let \(F=C_1\land\cdots\land C_k\) be an instance of Boolean \(3\)-satisfiability over variables \(z_1,\ldots,z_n\). We construct an allocation instance in polynomial time.
There is one type of mass \(\mu_1=1\). Its atom set is
\[
\]
\(A=\{p_i,n_i:1\leq i\leq n\}\cup\{d,e,v\}.\)
Here \(p_i\) and \(n_i\) are distinct atoms representing the two truth values of \(z_i\). The atoms \(d\) and \(e\) distinguish a fallback package from an assignment package.
The ground normal program contains the rules
\(p_i\leftarrow\operatorname{not} n_i,\qquad n_i\leftarrow\operatorname{not} p_i\qquad(1\leq i\leq n),\)
and
\(d\leftarrow\operatorname{not} e,\qquad e\leftarrow\operatorname{not} d.\)
For a Boolean literal \(\ell\), define its falsity atom by
\(f(z_i)=n_i,\qquad f(\neg z_i)=p_i.\)
For each clause \(C_j=\ell_{j1}\lor\ell_{j2}\lor\ell_{j3}\), add
\(v\leftarrow e,f(\ell_{j1}),f(\ell_{j2}),f(\ell_{j3}).\)
Thus \(v\) records that an assignment package falsifies at least one clause.
We use the usual reduct definition: a stable model is the least model of its positive normal reduct.
Every stable model contains exactly one of \(p_i,n_i\), for each \(i\), and exactly one of \(d,e\). To verify this, consider any such pair. If neither atom belongs to a candidate model, both corresponding rules become facts in the reduct. If both belong to it, both rules are removed, and neither atom has another defining rule. In either case, the candidate differs from the reduct’s least model.
Now fix a truth assignment \(\alpha\) and select either \(d\) or \(e\). The reduct contains the selected atoms as facts. Its only possible additional consequence is \(v\). By the clause rules, \(v\) is derived exactly when \(e\) was selected and \(\alpha\) falsifies a clause of \(F\).
It follows that the stable models are exactly:
This proves both directions of the characterization: every stable model has this form, and each listed set equals the least model of its reduct. In particular, the program always has stable models.
Set the weighted-literal list to \(E=\{(1,d)\}\). Thus
\(u(S)=\mathbf{1}_{d\in S}.\)
Use one resource, with consumption
\(h(S)=1+\mathbf{1}_{v\in S},\)
and bound \(b=1\). A constant-size Boolean circuit implements this function by reading the characteristic-vector bit for \(v\). The threshold is \(q=0\).
The packages therefore have the following values:
| Package | Score | Resource consumption |
|---|---:|---:|
| \(S_{\alpha,d}\) | \(1\) | \(1\) |
| \(S_{\alpha,e}\), where \(\alpha\models F\) | \(0\) | \(1\) |
| \(S_{\alpha,e}\), where \(\alpha\not\models F\) | \(0\) | \(2\) |
The allocation instance is always feasible: assigning mass \(1\) to any fallback package \(S_{\alpha,d}\) satisfies the resource bound.
Let \(x_S\) be any feasible allocation. Since its total mass is \(1\),
\(\sum_S x_Sh(S)=\sum_Sx_S+\sum_{S:v\in S}x_S=1+\sum_{S:v\in S}x_S.\)
The resource bound requires this quantity to be at most \(1\). Nonnegativity therefore implies
\(\sum_{S:v\in S}x_S=0.\)
Consequently, every assignment package corresponding to an unsatisfying assignment receives zero mass.
The objective is
\(\sum_Sx_Su(S)=\sum_{S:d\in S}x_S.\)
It is nonnegative, and it is at most \(q=0\) exactly when fallback packages also receive zero mass.
If \(F\) is satisfiable, choose a satisfying assignment \(\alpha\) and allocate mass \(1\) to \(S_{\alpha,e}\). This allocation has resource consumption \(1\) and objective \(0\).
Conversely, suppose a feasible allocation has objective at most \(0\). It gives zero mass to fallback packages and to unsatisfying assignment packages. Because its total mass is \(1\), some satisfying assignment package must exist. Hence \(F\) is satisfiable.
We have proved
\(F\text{ is satisfiable}\quad\Longleftrightarrow\quad\text{the constructed instance has a feasible allocation of objective at most }0.\)
Indeed, its optimum is exactly \(0\) when \(F\) is satisfiable and exactly \(1\) otherwise.
The construction has \(m=2n+3\), \(\tau=r=1\), and input length polynomial in the formula length. Its masses, bounds, weights, resource values, and threshold are constants. This is a polynomial-time many-one reduction from \(3\)-satisfiability, proving \(\mathrm{NP}\)-hardness for normal programs and therefore also for the permitted normal-or-disjunctive input class.
The implicit package representation creates computational hardness, but it does not force exponentially large optimal answers.
Claim. Every feasible instance has an optimal allocation with at most \(\tau+r\) positive package masses, all rational with polynomial encoding length.
Proof. Each atom set is finite, so each stable-model set is finite. Introduce one variable for each type-package pair. The feasible allocations form a finite-dimensional rational polytope \(K\).
For every variable, nonnegativity and its type’s mass equation imply
\(0\leq x_{t,S}\leq\mu_t.\)
Thus \(K\) is bounded. It is closed because it is defined by finitely many linear equalities and weak inequalities. If nonempty, it is compact, so the linear objective attains its minimum. A bounded nonempty polytope has an optimal vertex for every linear objective.
Let \(x\) be such a vertex, and suppose it has \(s>\tau+r\) positive coordinates. For each positive coordinate, form its column consisting of its \(\tau\) type-incidence entries followed by its \(r\) resource entries. These columns lie in a vector space of dimension \(\tau+r\), so they are linearly dependent.
There is therefore a nonzero vector \(d\), supported on the positive coordinates, that preserves all type totals and all resource totals. For sufficiently small \(\varepsilon>0\), both \(x+\varepsilon d\) and \(x-\varepsilon d\) remain nonnegative and feasible. They are distinct, and their midpoint is \(x\), contradicting that \(x\) is a vertex. Hence \(s\leq\tau+r\).
It remains to bound the encoding length of the masses. Let \(B\) bound the binary lengths of all resource coefficients, type masses, and resource bounds. Since the circuits output explicitly encoded binary rationals, \(B\) is polynomially bounded by \(L\).
Restrict the type equations and tight resource inequalities to the \(s\) positive coordinates. Their coefficient matrix has column rank \(s\). Otherwise a nonzero null direction would preserve these active constraints; sufficiently small perturbations in both directions would also preserve nonnegativity and the finitely many resource inequalities with positive slack, again contradicting extremality.
Select \(s\) independent rows, obtaining a nonsingular rational system
\(Dx=a.\)
In each row, clear the denominators of its \(s\) coefficients and its right-hand side. The resulting integer entries have binary length \(O(sB)\). By the determinant expansion, their determinants, including the determinants used in Cramer’s rule, have binary length \(O(s^2B+s\log s)\). Cramer’s rule therefore gives rational coordinates of polynomial encoding length.
Together with \(s\leq\tau+r\), this proves the claim. \(\square\)
Suppose all input programs are normal and the threshold answer is yes. An optimal vertex supplied by the preceding claim has objective at most \(q\). It provides a certificate containing at most \(\tau+r\) typed packages and their polynomial-size positive rational masses.
A verifier performs the following polynomial-time checks:
For completeness, the stable-model check remains valid with integrity constraints. The least model of the headed positive rules is contained in every model of those rules. If a larger model satisfies a positive integrity constraint, its least submodel also satisfies that constraint. Thus a candidate is a minimal model of the reduct precisely when it equals this least model and satisfies the constraints.
All certificate lengths and arithmetic lengths are polynomial in the input parameters. The decision problem for normal programs therefore belongs to \(\mathrm{NP}\). Combined with the reduction, it is \(\mathrm{NP}\)-complete. This membership argument is not asserted for disjunctive programs.
A polynomial-time exact allocation algorithm could be run on the constructed instances, which are always feasible. Computing the returned allocation’s objective and comparing it with \(0\) would decide \(3\)-satisfiability in polynomial time. Therefore such an algorithm would imply \(\mathrm{P}=\mathrm{NP}\).
The stated discrete correctness guarantee is compatible with this hardness result. The cited [asprin paper](https://ojs.aaai.org/index.php/AAAI/article/download/9398/9257) describes repeated solver calls and explicitly makes algorithmic complexity dependent on dominance tests; that guarantee supplies no polynomial-time bound for the present allocation problem.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The reduction establishes the requested \(\mathrm{NP}\)-hardness, including the stronger guarantees of program satisfiability and allocation feasibility. The additional polynomial certificate bound and \(\mathrm{NP}\)-membership argument for normal programs are correct. No substantive gaps or false steps were found.
The prover addresses the intended continuous allocation problem directly. Its construction uses implicitly represented stable-model packages, permits real-valued allocations, and respects all input restrictions:
Hardness for this restricted subclass establishes hardness for the full class allowing normal or disjunctive programs. The prover appropriately limits its \(\mathrm{NP}\)-completeness claim to normal programs.
The reduct argument is correct.
For each pair \(p_i,n_i\), selecting neither makes both rules facts in the reduct; selecting both removes both rules. Since neither atom has another defining rule, neither choice can equal the reduct’s least model. The same reasoning applies to \(d,e\).
After fixing exactly one atom from every pair, the selected atoms become facts. The only remaining possible derived atom is \(v\). Its rules have positive bodies, and their assignment atoms express precisely the falsity of the corresponding Boolean literals. Consequently:
The description of both families \(S_{\alpha,d}\) and \(S_{\alpha,e}\) therefore covers every stable model, and every listed set equals the least model of its own reduct. Both directions are justified.
This also verifies the satisfiability guarantee: every Boolean assignment yields a fallback stable model, independently of whether \(F\) is satisfiable.
Repeated literals, tautological clauses, and an empty clause list do not invalidate the stated characterization.
The weighted-literal list \(E=\{(1,d)\}\) yields exactly the stated score: fallback packages have score \(1\), and assignment packages have score \(0\).
The resource function \(h(S)=1+\mathbf{1}_{v\in S}\) has values \(1\) and \(2\), both nonnegative binary rationals. A circuit reading the bit for \(v\) can output either constant using a fixed number of gates and output bits. Thus the circuit representation meets the task’s requirements.
The package table follows correctly from the stable-model characterization. Every fallback package has resource consumption \(1\), so assigning it the entire mass produces a feasible allocation under \(b=1\). The claimed feasibility guarantee is established.
The critical resource calculation is correct:
\[ \sum_S x_Sh(S)=1+\sum_{S:v\in S}x_S. \]
The first term is \(1\) by the type-mass equation. The resource bound then forces the second term to be zero. Since the package set is finite and each mass is nonnegative, every package containing \(v\) individually receives zero mass.
The objective is exactly the total fallback mass. All scores are nonnegative, so objective at most \(0\) forces every fallback mass to be zero.
The forward implication is valid: a satisfying assignment supplies an assignment package with score \(0\) and resource consumption \(1\).
The reverse implication is also valid: after excluding fallback packages and unsatisfying assignment packages, the mass equation still requires total mass \(1\). Therefore a satisfying assignment package must exist.
This checks the effect of arbitrary real-valued mixing, rather than only integral or single-package allocations.
The claimed optimum values follow:
The program has \(2n+3\) atoms, \(2n+2+k\) rules, and polynomial encoding length. All allocation-related numerical values are constants. The reduction is therefore polynomial and proves the announced \(\mathrm{NP}\)-hardness.
The claim is correctly conditional on feasibility. If some type has no stable models, its positive mass equation makes the instance infeasible; this does not create an exception to the claim.
For a feasible instance, the number of variables is finite because all atom sets are finite. Each variable is bounded between \(0\) and its type mass. The resulting feasible set is a nonempty bounded rational polytope.
The invoked theorem—that a linear objective on a nonempty bounded polytope has an optimal vertex—is stated sufficiently precisely, and its hypotheses are verified. Arbitrary signed score weights do not cause a problem because the objective is linear and the feasible set is compact.
The linear-dependence argument is valid. If a vertex had more than \(\tau+r\) positive coordinates, the corresponding columns would admit a nonzero dependence preserving all type totals and resource totals. Restricting the perturbation to positive coordinates allows sufficiently small perturbations in both directions to preserve nonnegativity.
Both perturbed allocations remain feasible, are distinct, and have the original allocation as their midpoint. This contradicts extremality and establishes the support bound.
The active-row rank argument is also correct. A null direction on the positive coordinates would preserve all type equations and tight resource constraints. Each other resource inequality has positive slack, and there are finitely many such inequalities, so sufficiently small perturbations preserve them as well.
Selecting independent rows consequently produces the stated nonsingular rational system.
The arithmetic bounds check out:
The circuit output encoding explicitly bounds resource coefficient lengths by a polynomial in the input length. Together with \(s\leq\tau+r\), the argument establishes the claimed polynomial-size answer representation.
The certificate argument is sound. A yes-instance has an optimal vertex meeting the threshold, with polynomially many packages and polynomial-length rational masses.
A package characteristic vector has polynomial length in the input parameters. Forming a normal reduct and computing the least model of its headed positive rules are polynomial-time operations.
The treatment of integrity constraints is correct. Positive constraint satisfaction is preserved when passing to a subset. Thus, if any model of the headed positive reduct satisfies its constraints, the least model does as well. A candidate is a minimal model of the complete reduct exactly when it equals that least model and satisfies the constraints.
Circuit evaluation, literal evaluation, and the listed allocation checks take polynomial time. Exact rational arithmetic remains polynomial because both the number of certificate entries and their bit lengths are polynomial. The threshold’s binary encoding is included in the decision input.
Accordingly, the normal-program decision problem belongs to \(\mathrm{NP}\), and the reduction proves \(\mathrm{NP}\)-completeness.
The optimization consequence follows directly from the reduction. A polynomial-time algorithm returning an exact optimal allocation on these always-feasible instances would permit polynomial-time objective evaluation and distinguish optimum \(0\) from optimum \(1\), deciding \(3\)-satisfiability.
The final literature statement is accurate: the cited paper describes repeated solver calls and states that its algorithms depend on the complexity of dominance tests. This supports the claimed compatibility between its correctness guarantee and the present hardness result. [asprin paper](https://ojs.aaai.org/index.php/AAAI/article/download/9398/9257)
No mathematical repairs or additional clarifications are required. The output resolves the requested hardness alternative and rigorously establishes its supplementary claims.
⟨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.