Answer: \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, hence \(\mathrm{NP}\)-hard under polynomial-time Turing reductions, for every fixed allowed operation \(\oplus\).
Theorem 1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateHCLP-DEDUCTION FOR |=⊕ C(t) is polynomial when t = 1, and is coNP-complete for any t > 1, even if we restrict the language to non-strict preference statements. HCLP-DEDUCTION FOR |=⊕ C(≡) is polynomial for any equiv- alence relation ≡. Example We consider an example with alternatives A = {α, β, γ}, us- ing ⊕as + (ordinary addition), and with evaluations C = {c1, c2, c3}, defined as follows. c1(α) = 0; c1(β) = 2; c1(γ) = 1; c2(α) = 2; c2(β) = 0; c2(γ) = 2; c3(α) = 1; c3(β) = 0; c3(γ) = 0. Suppose that the user tells us that they consider α to be at least as good as β.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite HCLP structure, a query \(\alpha\le\beta\), a rational threshold \(q\), a support bound \(\tau\), and strata \(j\) with rational masses \(w_j\) summing to one and input statements \(\Gamma_j\), consider allocations \(x_{j,H}\ge0\) of each stratum’s mass to HCLP types \(H\in\mathcal C(2)\) satisfying \(\Gamma_j\), with at most \(\tau\) distinct types used overall. Is the minimum, over all such compatible allocations, of \(\sum_{j,H:\,H\models^\oplus\alpha\le\beta}x_{j,H}\) at least \(q\)?
Let \(A\) be a finite set of alternatives and \(C\) a finite set of criteria, with \(m=|C|\ge2\), given by tables \(c:A\to\mathbb Q_{\ge0}\). Fix an associative, commutative, monotone operation \(\oplus\) on nonnegative rationals, with identity \(0\), computable in linear bit time.
An HCLP type \(H=(C_1,\ldots,C_k)\in\mathcal C(2)\) is an ordered partition of any subset of \(C\), with nonempty levels of size at most two; the empty sequence is allowed. Compare alternatives lexicographically by the level costs \(\bigoplus_{c\in C_i}c(a)\), preferring smaller costs. Write \(H\models^\oplus a\le b\) for weak preference and \(H\models^\oplus a<b\) for strict preference; complete ties satisfy only the weak comparison.
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here input types are strata described by finite sets \(\Gamma_j\) of strict or non-strict comparisons; \(\tau\) is the support size, not the number of possible HCLP types. Masses \(w_j>0\) satisfy \(\sum_jw_j=1\).
The remaining inputs are \(\alpha,\beta\in A\), a binary rational \(q\in[0,1]\), and a binary integer \(K\ge1\) bounding the number of distinct HCLP types used overall. Let \(L\) be the total input bit length.
A compatible allocation has nonnegative rational entries \(x_{j,H}\), satisfies \(\sum_Hx_{j,H}=w_j\), and has \(x_{j,H}=0\) unless \(H\models^\oplus\Gamma_j\); moreover \(\left|\{H:\sum_jx_{j,H}>0\}\right|\le K\). Define \(V=\min_x\sum_{j,H:\,H\models^\oplus\alpha\le\beta}x_{j,H}\), with \(V=+\infty\) if no compatible allocation exists.
Is deciding whether \(V\ge q\) in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard under polynomial-time Turing reductions? State running times in \(m,\tau,L,K,|A|\), and \(\sum_j|\Gamma_j|\).
Discrete HCLP deduction with levels of size at most two is \(\mathrm{coNP}\)-complete even with only non-strict statements; singleton levels give polynomial-time deduction ([source](https://arxiv.org/html/2409.11044v1)).
Discrete consistency with levels of size at most two is \(\mathrm{NP}\)-complete ([source](https://cora.ucc.ie/server/api/core/bitstreams/67c3ee36-edd7-40ae-a13d-17bdf96c7120/content)). No result settling this exact allocation problem was located.
For every fixed operation \(\oplus\) satisfying the stated assumptions, deciding whether \(V\ge q\) is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions. Consequently, it is \(\mathrm{NP}\)-hard under polynomial-time Turing reductions, and a polynomial-time algorithm would imply \(\mathrm P=\mathrm{NP}\).
Hardness holds even when \(\tau=K=1\), \(q=1\), and all input statements are non-strict. These restricted instances are always feasible.
Write \(S=\sum_{j=1}^{\tau}|\Gamma_j|\).
For each type \(H\), define \(d(H)=1\) if \(H\models^\oplus\alpha\le\beta\), and \(d(H)=0\) otherwise.
Lemma. Every compatible allocation can be replaced by a compatible allocation assigning each stratum’s entire mass to one type, without increasing its objective or its number of distinct types.
Proof. Let \(x\) be compatible. For each stratum \(j\), its positive mass \(w_j\) implies that some \(x_{j,H}\) is positive. Among those types, choose \(H_j\) minimizing \(d(H)\). Assign all \(w_j\) to \(H_j\).
Compatibility holds because \(x_{j,H_j}>0\) implies \(H_j\models^\oplus\Gamma_j\). Every selected type belonged to the original support, so the number of types cannot increase. Moreover,
\(w_jd(H_j)=\sum_Hx_{j,H}d(H_j)\le\sum_Hx_{j,H}d(H).\)
Summing over \(j\) proves the claim. \(\square\)
There are finitely many HCLP types. Therefore, if an allocation exists, the minimum is attained by such an unsplit allocation, and
\(V=\min\left\{\sum_{j=1}^{\tau}w_jd(H_j): H_j\models^\oplus\Gamma_j,\ \left|\{H_1,\ldots,H_\tau\}\right|\le K\right\}.\)
The minimum of an empty feasible family is understood as \(+\infty\). In particular, any feasible optimum uses at most \(\min\{K,\tau\}\) types. No linear programming is needed.
The complement of the decision problem asks whether \(V<q\).
By the lemma, a certificate consists of one type \(H_j\) for each stratum, satisfying:
Equivalently, the certificate can list at most \(\min\{K,\tau\}\) types and specify which listed type each stratum uses. Duplicate entries in this list cause no difficulty: its length already bounds the number of distinct types.
A type contains at most \(m\) criterion occurrences and has an encoding of length \(O(m\log(m+1))\). Thus the certificate length is polynomial in \(L\), even though \(K\) is binary encoded.
To verify satisfaction, compute the costs at successive levels and inspect the first unequal pair. Each level has at most two criteria. The linear bit-time assumption on \(\oplus\) implies that every level cost has \(O(L)\) bits. Rational comparisons and the final weighted sum can therefore be checked in polynomial bit time. For the weighted sum, a common denominator obtained by multiplying the input denominators has \(O(L)\) bits.
For example, a conservative verification bound is
\(O\!\left(L^2\left[m^2(|A|+S+1)+m(S+\tau)+\tau\right]\right).\)
Here one may first compute costs for every singleton and pair, and comparison signs for all statements appearing in the input or query.
If no allocation exists, then \(V=+\infty\), so the instance is correctly outside the complement. Hence the original problem belongs to \(\mathrm{coNP}\).
The cited deduction theorem states that deciding \(\Gamma\models_{\mathcal C(2)}^\oplus\alpha\le\beta\) is \(\mathrm{coNP}\)-complete even when \(\Gamma\) contains only non-strict statements. Its HCLP structures use precisely the assumptions here: nonnegative rational criterion tables, an associative, commutative, monotone operation with identity \(0\), linear-time computation of that operation, and ordered partitions of possibly empty criterion subsets. Thus it applies to the fixed operation in this question. [Wilson, George, and O’Sullivan, Theorem 1](https://arxiv.org/html/2409.11044v1#S2).
Given such a deduction instance, retain its alternatives, criteria, tables, and query, and construct the allocation instance with
\(\tau=1,\quad \Gamma_1=\Gamma,\quad w_1=1,\quad K=1,\quad q=1.\)
This transformation has polynomial running time and output length. Since all statements in \(\Gamma\) are non-strict, the empty type satisfies them, so the allocation instance is feasible.
With one stratum and \(K=1\), all mass must be assigned to a single compatible type. Consequently:
Therefore,
\(V\ge1\quad\Longleftrightarrow\quad\Gamma\models_{\mathcal C(2)}^\oplus\alpha\le\beta.\)
This proves \(\mathrm{coNP}\)-hardness, and together with Section 2 proves \(\mathrm{coNP}\)-completeness.
For the requested Turing hardness, take a polynomial-time reduction from \(3\)-UNSAT to this problem. On a \(3\)-SAT instance, make the resulting oracle query and negate its answer. This decides \(3\)-SAT using one oracle call, proving \(\mathrm{NP}\)-hardness under polynomial-time Turing reductions.
Let \(N=N_m=|\mathcal C(2)|\). An upper bound sufficient for the algorithm is
\(N\le\sum_{n=0}^{m}\frac{m!}{(m-n)!}\,2^n\le(m+1)2^m m!=2^{O(m\log m)}.\)
Indeed, a type using \(n\) criteria can be represented by an ordered list of those criteria and cuts into blocks of size one or two. There are \(m!/(m-n)!\) possible lists and at most \(2^n\) cut patterns. Multiple representations only enlarge this upper bound.
Set
\(k=\min\{K,\tau,N\},\qquad F(N,k)=\sum_{r=1}^{k}\binom Nr.\)
Enumerate all types and record their compatibility with each stratum and their query indicators \(d(H)\). Then enumerate all nonempty type sets \(T\) with \(|T|\le k\).
For a fixed \(T\), define \(I_j(T)=\{H\in T:H\models^\oplus\Gamma_j\}\). The set \(T\) permits an allocation exactly when every \(I_j(T)\) is nonempty. When it does, its minimum objective is
\(f(T)=\sum_{\{j:\ d(H)=1\text{ for every }H\in I_j(T)\}}w_j.\)
To justify this formula, a stratum contributes zero whenever it has a compatible type with indicator zero; otherwise every compatible type contributes its entire mass. These choices use only types from \(T\). Taking the minimum of \(f(T)\) over feasible enumerated sets gives \(V\), by Section 1.
Using ordinary rational arithmetic, a conservative bit-time bound for this exact algorithm is
\(O\!\left(L^2\left[m^2(|A|+S+1)+Nm(S+\tau)+\tau(k+1)F(N,k)\right]\right).\)
The terms account respectively for preprocessing level comparisons, screening all types, and evaluating all candidate type sets. This bound explicitly handles binary encoded \(K\): only its capped value \(k\) controls enumeration.
Since \(F(N,k)\le(N+1)^k\), the bound is also
\(2^{O(km\log m)}\operatorname{poly}(L,m,\tau,|A|,S).\)
Alternatively, \(F(N,k)\le2^N\) yields
\(2^{\,2^{O(m\log m)}}\operatorname{poly}(L,m,\tau,|A|,S),\)
so the problem is fixed-parameter tractable in \(m\). If \(q=0\), the answer is always yes, including infeasible instances.
⟨structured verdict parsed — rendered above⟩
The prover’s classification is correct. The output resolves the allocation problem and establishes coNP-completeness under polynomial-time many-one reductions, hence NP-hardness under polynomial-time Turing reductions. I found no major or minor mathematical issues requiring repair.
The lemma is valid.
There are finitely many admissible types. For each stratum \(j\), the conditions \(w_j>0\) and \(\sum_H x_{j,H}=w_j\) ensure that at least one entry is positive. Choosing \(H_j\) with minimum indicator among those positive entries is therefore well-defined.
Each selected type satisfies \(\Gamma_j\), and every selected type belongs to the original allocation’s global support. Consequently, assigning the whole mass \(w_j\) to \(H_j\) preserves compatibility and cannot increase the number of distinct types.
The objective inequality is correct: for every positive entry \(x_{j,H}\), the selection guarantees \(d(H_j)\le d(H)\). Zero entries contribute nothing. Thus
\[
w_jd(H_j)\le \sum_H x_{j,H}d(H).
\]
The new entries are rational because the input masses are rational.
The minimum-attainment conclusion also follows. Whenever an allocation exists, the lemma produces a feasible unsplit allocation. The family of unsplit assignments is finite, so its minimum is attained. Every feasible allocation has an unsplit replacement with no greater objective, and every feasible unsplit assignment is itself an allocation. Therefore the displayed characterization of \(V\) is exact.
The bound of \(\min\{K,\tau\}\) on the number of types used by an optimum is justified.
The certificate establishes precisely the complement condition \(V<q\).
If \(V<q\), the preceding lemma supplies an unsplit certificate with objective below \(q\). Conversely, any certificate satisfying the three listed requirements defines a compatible allocation with objective below \(q\).
A type uses each criterion at most once and contains at most \(m\) criterion occurrences. Its stated encoding bound \(O(m\log(m+1))\) is valid. Listing one type per stratum therefore gives a polynomial-size certificate under the explicit input representation. Binary encoding of \(K\) causes no difficulty because no more than \(\tau\) types need be listed.
The satisfaction check correctly uses the first unequal level. A complete tie satisfies a weak comparison and fails a strict comparison, including for the empty type.
The arithmetic claims are sound:
The verification bound
\[
O\!\left(L^2\left[m^2(|A|+S+1)+m(S+\tau)+\tau\right]\right)
\]
is conservative and sufficient. Its terms cover preprocessing singleton and pair costs and comparison signs, scanning the certificate types, and computing the weighted sum. Routine structural checks on the encoded types also fit within this bound.
For infeasible instances, \(V=+\infty\), so no complement certificate exists. This is consistent with membership in coNP.
The citation is applicable. The source defines the same nonnegative rational domain, operation assumptions, lexicographic semantics, and ordered partitions of possibly empty criterion subsets. Its Theorem 1 establishes coNP-completeness for level bound two with non-strict premises and query. Section 3 supplies the corresponding reduction for the permitted fixed operations; it does not restrict hardness to addition. Thus the prover’s universal claim over fixed allowed operations is supported. [Wilson, George, and O’Sullivan, Theorem 1 and Section 3](https://arxiv.org/html/2409.11044v1#S3).
No theorem-hypothesis mismatch was found.
The construction
\[
\tau=1,\qquad \Gamma_1=\Gamma,\qquad w_1=1,\qquad K=1,\qquad q=1
\]
preserves the original tables and query and adds only constant-size allocation data. It is a polynomial-time many-one reduction.
Feasibility is correctly established: the empty type satisfies every non-strict premise and supplies a compatible allocation.
With one stratum of mass one and at most one globally used type, every compatible allocation assigns the entire mass to a single satisfying type. Its objective is therefore either zero or one.
Both reduction directions are correct:
Accordingly,
\[
V\ge1
\quad\Longleftrightarrow\quad
\Gamma\models_{\mathcal C(2)}^\oplus\alpha\le\beta.
\]
This establishes coNP-hardness on feasible instances with all the claimed restrictions. Together with membership, it proves coNP-completeness.
The Turing-hardness argument is also valid. A reduction from 3-UNSAT followed by one oracle call and answer negation decides 3-SAT. The implication that a polynomial-time algorithm would yield \(\mathrm P=\mathrm{NP}\) follows.
The type-count bound is correct. For a type using \(n\) criteria, an ordered list of distinct criteria and a division into blocks of size one or two provide a representation. Counting multiple representations only increases the upper bound. Thus
\[
N\le\sum_{n=0}^{m}\frac{m!}{(m-n)!}2^n
\le(m+1)2^m m!
=2^{O(m\log m)}.
\]
The cap \(k=\min\{K,\tau,N\}\) is justified by the unsplitting lemma and the total number of types.
For a candidate set \(T\), feasibility is equivalent to every \(I_j(T)\) being nonempty. This equivalence uses the absence of capacity constraints on individual types: each stratum may independently choose any compatible type in \(T\).
The formula for \(f(T)\) is exact. A stratum contributes zero if a compatible type with indicator zero is available. Otherwise its entire mass necessarily contributes. The independent choices use at most \(|T|\) types.
Enumerating all nonempty candidate sets suffices. The input normalization implies \(\tau\ge1\), and every compatible allocation has nonempty support. Taking the minimum over feasible sets therefore computes \(V\), with an empty feasible family giving \(+\infty\).
The stated bound
\[
O\!\left(L^2\left[m^2(|A|+S+1)+Nm(S+\tau)+\tau(k+1)F(N,k)\right]\right)
\]
covers preprocessing, type screening, and candidate-set evaluation. It explicitly includes every requested input parameter, with binary \(K\) entering through its capped value.
Both estimates \(F(N,k)\le(N+1)^k\) and \(F(N,k)\le2^N\) are valid. They support the claimed exponential bounds and fixed-parameter tractability in \(m\).
The empty type, strict statements, infeasibility, binary \(K\), and the threshold \(q=0\) are handled correctly. If \(\alpha=\beta\), every type satisfies the query; feasible objectives equal one, while infeasible instances retain \(V=+\infty\), consistently with the argument.
No additional clarification or mathematical 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.