Answer: \(\mathrm{NP}\text{-hard}\), even for one guaranteed-feasible type with a singleton preference set; polynomial-time solvable if and only if \(\mathrm{P}=\mathrm{NP}\).
Theorem 2 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateLet ϕ be a formula and S, ≺a qualitative preference on literals. PREF-DLL(ϕ, ∅) terminates, and then μopt is empty if ϕ is unsatisfiable, and an optimal model of ϕ wrt S, ≺otherwise. Beside the above, one interesting property of PREF-DLL is its “anytime” property: The sequence of models μ1, μ2, . . . , μn com- puted by PREF-DLL are ensured to be such that μi+1 is preferred to μi, i.e., μi+1 ≺μi (0 < i < n). Thus, PREF-DLL is as fast as DLL to compute the first model of the input set of clauses, and, time permit- ting, from that point on, it can only improve the quality of the model found.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set \(T\) of complete SAT task types, each with a formula \(\varphi_t\) and qualitative preference \((S_t,\prec_t)\), and rational masses \(\mu_t>0\) summing to \(1\), find an allocation \(x_{t,a}\ge 0\) over satisfying total assignments \(a\models\varphi_t\). Require \(\sum_{a\models\varphi_t}x_{t,a}=\mu_t\), with positive mass only on assignments optimal under \((S_t,\prec_t)\); report infeasibility if any positive-mass type has no satisfying model.
A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
Each type specifies a CNF formula \(\varphi_t\) over a common set of \(m\) Boolean variables, a set \(S_t\) of literals, and an explicitly represented strict partial order \(\prec_t\) on \(S_t\); the empty preference set is allowed. Let \(L\) be the total input bit length.
Identify a total assignment with its set of true literals. Assignment \(b\) is preferred to \(a\) for type \(t\) exactly when \(S_t\cap(b\setminus a)\ne\varnothing\) and every \(\ell'\in S_t\cap(a\setminus b)\) has some \(\ell\in S_t\cap(b\setminus a)\) with \(\ell\prec_t\ell'\).
A satisfying assignment is optimal when no satisfying assignment is preferred to it; all such optimal assignments are eligible, without tie-breaking.
Find an allocation, represented by its nonzero binary-rational entries, with \(x_{t,a}\ge 0\), \(\sum_{a\models\varphi_t}x_{t,a}=\mu_t\), and \(x_{t,a}>0\) only for optimal satisfying total assignments. Report infeasibility if any type has no satisfying assignment.
Can this allocation problem be solved in polynomial time in \(m,\tau,L\), or is it NP-hard?
For a single discrete task, a terminating procedure returns an optimal model or detects unsatisfiability, using polynomial space; this is not a polynomial-time guarantee ([verified discrete result](https://doi.org/10.3233/978-1-58603-891-5-510)).
No result settling this exact mass-allocation problem was identified in the literature search.
The allocation problem is \(\mathrm{NP}\)-hard, even with a single type, mass \(1\), a singleton preference set, and a formula guaranteed to be satisfiable. Thus the hardness persists when detecting infeasibility is unnecessary.
Moreover, the problem is solvable in polynomial time with a satisfiability oracle. Consequently, it admits a polynomial-time algorithm if and only if \(\mathrm{P}=\mathrm{NP}\).
Allowing empty preferences already gives a direct reduction from satisfiability: use one type whose formula is the input CNF. The stronger reduction below establishes hardness even when a valid allocation always exists and preferences are nonempty.
Let \(F\) be any CNF formula over variables \(y_1,\ldots,y_n\). Introduce a fresh variable \(z\), and construct a society with one type \(t\), specified by:
This construction has polynomial size. The formula \(\varphi_t\) is always satisfiable: every assignment with \(z=0\) satisfies it. An assignment with \(z=1\) satisfies \(\varphi_t\) exactly when its restriction to the original variables satisfies \(F\).
For this preference set, an assignment \(b\) is preferred to an assignment \(a\) exactly when \(b(z)=1\) and \(a(z)=0\). Indeed, these values make the set of gained preferred literals equal to \(\{z\}\) and the set of lost preferred literals empty, so the required condition on losses holds vacuously. Every other pair has an empty set of gained preferred literals.
There are therefore two cases.
If \(F\) is satisfiable, some satisfying assignment of \(\varphi_t\) has \(z=1\). Such an assignment is preferred to every satisfying assignment with \(z=0\). Every satisfying assignment with \(z=1\) is optimal, because no assignment can gain the literal \(z\) from it. Thus all eligible assignments have \(z=1\).
If \(F\) is unsatisfiable, every satisfying assignment of \(\varphi_t\) has \(z=0\). No satisfying assignment is preferred to any other, so all satisfying assignments are optimal and have \(z=0\).
Now suppose a polynomial-time algorithm solves the allocation problem. Apply it to this constructed society. Its output must contain a positive entry, since the entries sum to \(1\). Read the assignment associated with any such entry. By eligibility, its value of \(z\) is \(1\) exactly when \(F\) is satisfiable.
This decides CNF satisfiability in polynomial time. Hence computing a valid allocation is \(\mathrm{NP}\)-hard, including on the guaranteed-feasible instances just constructed. Allowing the algorithm to split the mass among several assignments does not affect the reduction: every eligible assignment has the same value of \(z\).
We next justify existence and an oracle upper bound for the full stated preference relation.
Fix a type \(t\). Since \(\prec_t\) is a strict partial order on the finite set \(S_t\), its directed graph is acyclic and has a topological ordering. Write such an ordering as \(\ell_1,\ldots,\ell_k\), with \(\ell_i\prec_t\ell_j\) implying \(i<j\).
For a total assignment \(a\), define its preference vector by
\(\displaystyle v_t(a)=\bigl(\mathbf{1}_{\ell_1\in a},\ldots,\mathbf{1}_{\ell_k\in a}\bigr).\)
Compare these vectors lexicographically, with \(1\) larger than \(0\).
Lemma. If \(b\) is preferred to \(a\), then \(v_t(b)\) is lexicographically larger than \(v_t(a)\).
Proof. Preference requires a gained literal in \(S_t\), so the vectors differ. Let \(i\) be their first differing coordinate. Suppose this coordinate were a loss: \(\ell_i\in a\setminus b\). By the definition of preference, some gained literal \(\ell_j\in S_t\cap(b\setminus a)\) satisfies \(\ell_j\prec_t\ell_i\). The topological ordering gives \(j<i\). But coordinate \(j\) then also differs, contradicting the choice of \(i\). Thus the first differing coordinate is a gain, proving the lemma. \(\square\)
If \(\varphi_t\) is satisfiable, its finite nonempty set of satisfying assignments contains an assignment maximizing \(v_t\) lexicographically. The lemma shows that no satisfying assignment can be preferred to this maximizer, so it is optimal. This argument also covers \(S_t=\varnothing\), when every satisfying assignment is optimal.
Consequently, allocation is feasible exactly when every type’s formula is satisfiable. Once an optimal assignment \(a_t\) is chosen for each type, a valid allocation is simply
\(\displaystyle x_{t,a_t}=\mu_t,\qquad x_{t,a}=0\text{ for }a\ne a_t.\)
There are no constraints coupling different types.
For each type, perform the following procedure.
At every step, the retained formula is satisfiable. When the query with \(\ell_i\) fails, every model of the current formula satisfies \(\neg\ell_i\), which justifies retaining the latter clause.
The resulting preference vector is lexicographically maximal. To verify this, suppose a satisfying assignment had a larger vector, and consider its first differing coordinate. At that coordinate, the procedure must have chosen \(0\), while the proposed assignment has \(1\) and agrees with every preceding choice. That assignment would witness satisfiability of the query that failed—a contradiction. By the lemma, \(a_t\) is optimal.
Since \(|S_t|\leq 2m\), the procedure uses at most \(1+3m\) satisfiability queries per type. Each query has polynomial size. Returning \(x_{t,a_t}=\mu_t\) gives at most \(\tau\) nonzero entries, whose masses are copied directly from the input. Thus the output also has polynomial length.
If \(\mathrm{P}=\mathrm{NP}\), these satisfiability queries can be answered in polynomial time, yielding a polynomial-time allocation algorithm. Together with the reduction, this establishes the claimed equivalence.
⟨structured verdict parsed — rendered above⟩
The prover’s output resolves the task correctly. The guaranteed-feasible reduction establishes hardness of computing any valid allocation, and the satisfiability-oracle algorithm establishes the claimed conditional polynomial-time upper bound. No major or minor mathematical issues were found.
The reduction takes an arbitrary CNF formula \(F\), introduces one fresh variable \(z\), and replaces every clause \(C\) with \(\neg z\lor C\). The resulting formula is CNF and has polynomial size. The single mass \(1\) is a valid positive binary rational, and the empty relation on the singleton preference set \(\{z\}\) is a strict partial order.
Every assignment with \(z=0\) satisfies the constructed formula. With \(z=1\), the constructed formula is satisfied exactly when \(F\) is satisfied by the original variables. These claims also hold when \(F\) has no clauses or contains an empty clause.
With \(S_t=\{z\}\), the gained preferred-literal set is nonempty exactly when \(b(z)=1\) and \(a(z)=0\). In that case, there are no lost preferred literals, so the loss condition holds vacuously. Thus the claimed characterization of preference is exact.
If \(F\) is satisfiable, a satisfying assignment with \(z=1\) exists and dominates every satisfying assignment with \(z=0\). No assignment can gain \(z\) from an assignment already having \(z=1\). Consequently, precisely the satisfying assignments with \(z=1\) are optimal.
If \(F\) is unsatisfiable, all satisfying assignments of the constructed formula have \(z=0\), and none is preferred to another. All are therefore optimal.
Because the single type has mass \(1\), every valid output contains at least one nonzero entry. Its associated assignment must be optimal. The preceding characterization shows that reading its value of \(z\) decides whether \(F\) is satisfiable.
This argument applies to every valid allocation, including outputs that split the mass across multiple assignments. A polynomial-time solver necessarily writes a polynomial-length output, so extracting an entry introduces no output-size gap.
The reduction therefore establishes the asserted computational hardness under a polynomial-time oracle reduction from CNF satisfiability to the allocation search problem. The prover appropriately concerns itself with computing an allocation; it does not incorrectly claim that feasibility remains hard on these guaranteed-feasible instances.
A finite strict partial order is acyclic and admits a topological ordering with the stated orientation. The hypotheses required for this standard fact are present.
The lexicographic lemma is correct. Preference guarantees at least one differing coordinate. If the first difference were a loss, the preference definition would supply a gained literal strictly preceding that loss in the partial order. The topological ordering would place this gain at an earlier differing coordinate, a contradiction.
The lemma remains valid when the preference set contains both literals of a variable: each literal still has a well-defined membership coordinate, and the argument does not require those coordinates to vary independently.
A satisfiable formula has a finite nonempty set of total models, so a lexicographic maximum exists. The lemma rules out any satisfying assignment preferred to that maximum. The empty preference set is explicitly and correctly handled.
Hence feasibility is exactly simultaneous satisfiability of all type formulas. Assigning each type’s entire mass to one optimal model satisfies every allocation constraint, since there are no constraints coupling types.
The initial query establishes satisfiability. Each successful literal query preserves it. Each failed query implies that all models of the current formula satisfy the complementary literal, so retaining that complementary unit clause also preserves satisfiability. Here \(\neg\ell_i\) is understood as the complementary literal, including when \(\ell_i\) is already negative.
The first-difference argument correctly proves lexicographic maximality: a purported larger vector would supply a model of a query declared unsatisfiable while respecting every preceding retained preference choice.
Fixing the remaining variables preserves the selected preference vector and produces a total satisfying assignment. The lemma then guarantees optimality.
There are at most \(2m\) preference literals and at most \(m\) remaining variable queries, giving the stated bound of \(1+3m\) queries per type. Each query adds only polynomially many unit clauses. Topological sorting and the remaining bookkeeping are polynomial in the explicit input size.
The output contains at most \(\tau\) entries, with assignments of length proportional to \(m\) and masses copied from the input, so its length is polynomial.
If \(\mathrm{P}=\mathrm{NP}\), the satisfiability queries admit polynomial-time answers. Conversely, a polynomial-time allocation algorithm would decide CNF satisfiability through the reduction. The claimed equivalence follows.
No additional clarification or repair is required.
⟨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.