Answer: NP-complete, even for \(\tau=1\) and \(\Gamma=\top\), with either strictly positive or strictly negative formula weights.
Theorem 3.1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateSW-VAL-CHECK (resp., SW-INT-CHECK) is NP- complete (resp., co-NP-complete). Hardness holds on posi- tive and negative single-agent scenarios without constraints. Moving to the egalitarian social welfare, we have to ob- serve that according to Definition 2.2, even just checking whether some given interpretation is α-fair requires the com- putation of the maximum utilitarian social welfare associated with each of the individual goalbases. We show below that this problem is F∆P 2-hard.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite variable set \(V\), a feasible-outcome constraint \(\Gamma\), complete goalbases \(G_1,\ldots,G_\tau\) with positive rational masses \(\mu_1,\ldots,\mu_\tau\) summing to \(1\), and a rational threshold \(\gamma\), is there an interpretation \(\sigma\models\Gamma\) such that \(\sum_{t=1}^{\tau}\mu_tG_t(\sigma)\ge\gamma\)?
Let \(V\) be a finite set of Boolean variables, with \(m=|V|\). A goalbase \(G\) is an explicitly listed finite set of pairs \(\langle\varphi,w\rangle\), where \(\varphi\) is a propositional formula over \(V\) and \(w\in\mathbb{Q}\) may have either sign or be zero; define \(G(\sigma)=\sum_{\langle\varphi,w\rangle\in G:\,\sigma\models\varphi}w\).
A society is given by its support: the list of \(\tau\geq1\) distinct goalbase types \(G_1,\ldots,G_\tau\) with positive binary rational masses \(\mu_1,\ldots,\mu_\tau\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types; each goalbase is supplied in full.
The input also contains a satisfiable propositional constraint \(\Gamma\) over \(V\) and a binary rational threshold \(\gamma\in\mathbb{Q}\). Outcomes are Boolean interpretations \(\sigma:V\to\{\top,\bot\}\) satisfying \(\Gamma\).
Let \(L\) be the total input bit length, including formulas, weights, masses, and threshold; state running times in \(m,\tau,L\).
Is deciding whether there exists a feasible interpretation \(\sigma\) with \(\sum_{t=1}^{\tau}\mu_tG_t(\sigma)\geq\gamma\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
For a finite list of agents with unweighted utilitarian aggregation, the corresponding threshold decision problem is NP-complete, even with one agent and \(\Gamma=\top\), both when all formula weights are positive and when all are negative.
No separate result for the distribution-over-types formulation is supplied.
The decision problem is NP-complete, even when the support size is \(\tau=1\), the constraint is \(\Gamma=\top\), and all formula weights are strictly positive. It remains NP-complete when all formula weights are strictly negative.
Thus a polynomial-time algorithm in \(m,\tau,L\) exists if and only if \(\mathrm{P}=\mathrm{NP}\).
A certificate is an interpretation \(\sigma\), represented by \(m\) Boolean values. We verify that \(\sigma\models\Gamma\), evaluate the explicitly listed goal formulas, and compare the resulting utility with \(\gamma\).
The rational comparison can be performed exactly with polynomial bit complexity. Write the weights, masses, and threshold as
\(w_{t,j}=a_{t,j}/b_{t,j}\), \(\mu_t=c_t/d_t\), and \(\gamma=e/f\),
where all denominators are positive. Let \(N\) be the total number of listed goal pairs and define
\(D=f\left(\prod_{t=1}^{\tau}d_t\right)\left(\prod_{t,j}b_{t,j}\right)\).
For every pair \((t,j)\), the integer \(d_tb_{t,j}\) divides \(D\). Consequently, the required comparison is equivalent to the integer comparison
\(\displaystyle \sum_{t,j:\,\sigma\models\varphi_{t,j}} a_{t,j}c_t\,\frac{D}{d_tb_{t,j}}\ \geq\ e\,\frac{D}{f}.\)
The total bit length of all input denominators is at most \(L\), so \(D\) has \(O(L)\) bits. Each summand also has \(O(L)\) bits: its numerator factors and \(D\) each have bit length bounded by the input length. Summing at most \(N\leq L\) terms adds only \(O(\log L)\) bits. Thus every integer used in this calculation has \(O(L)\) bits.
There are \(O(L)\) arithmetic operations. Using elementary integer arithmetic, they take \(O(L^3)\) bit operations. Formula evaluation is polynomial as well. A conservative total verifier bound is \(O((m+\tau+L)^3)\).
This proves membership in NP. Exhaustively checking all interpretations also gives a deterministic upper bound of \(O(2^m(m+\tau+L)^3)\).
We give a polynomial-time reduction from propositional satisfiability.
Given a propositional formula \(F\), use its variables as \(V\), and construct the instance
\(\tau=1,\qquad \mu_1=1,\qquad G_1=\{\langle F,1\rangle\},\qquad \Gamma=\top,\qquad \gamma=1.\)
This is a valid society: its sole mass is positive and sums to \(1\). The constraint is satisfiable, and the sole formula weight is strictly positive.
For any interpretation \(\sigma\), the aggregate utility is \(1\) if \(\sigma\models F\), and \(0\) otherwise. Therefore,
\(\displaystyle \exists\sigma\models\Gamma:\ \sum_{t=1}^{\tau}\mu_tG_t(\sigma)\geq\gamma \quad\Longleftrightarrow\quad F\text{ is satisfiable}.\)
The construction has size \(O(|F|)\). Since propositional satisfiability is NP-complete, this establishes NP-hardness.
For the strictly negative restriction, instead construct
\(\tau=1,\qquad \mu_1=1,\qquad G_1=\{\langle\neg F,-1\rangle\},\qquad \Gamma=\top,\qquad \gamma=0.\)
If \(\sigma\models F\), the sole goal formula is false, so the utility is \(0\). If \(\sigma\not\models F\), the sole goal formula is true, so the utility is \(-1\). Hence a feasible interpretation has utility at least \(0\) exactly when it satisfies \(F\).
This is again a polynomial-time reduction satisfying every input requirement.
The support representation permits a society containing exactly one type with mass \(1\). On such an instance, \(\sum_t\mu_tG_t(\sigma)=G_1(\sigma)\). It therefore contains the one-agent problem as a special case, without any encoding expansion. No separate hardness theorem for distributions over types is needed.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly. Both reductions satisfy every input requirement, and the certificate verification establishes membership in NP with the claimed polynomial running time. No major or minor issues were found.
\[
D=f\left(\prod_{t=1}^{\tau}d_t\right)\left(\prod_{t,j}b_{t,j}\right)
\]
is positive. Each \(d_tb_{t,j}\) divides \(D\): the displayed product includes both factors with their required multiplicities. Multiplication by \(D\) therefore preserves the inequality and gives exactly the integer comparison written in the proof. Negative and zero weights, and either sign of the threshold, cause no problem.
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.