Answer: Polynomial-time solvable
Proposition 7 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThere is an algorithm that runs in time O(|W| ×||ϕ||) to check, given any set W ⊆2Φ0, any world w ∈W and any formula ϕ ∈L, whether W, w |= ϕ, where ||ϕ|| denotes the size of ϕ, i.e., the number of symbols occurring in ϕ.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given an explicit finite alternative set \(W\), a support \(T_+\) of \(\tau\) complete, equal-depth RCL formula types \(\varphi_t=A^t_1\triangledown\cdots\triangledown A^t_d\), binary-rational masses \(\mu_t>0\) summing to \(1\), and a rational quota \(\alpha\in(0,1]\), define \(h_t(w)=\min\{j:w\models A^t_j\}\) and \(q_\alpha(w)=\min\{k:\sum_{t:h_t(w)\le k}\mu_t\ge\alpha\}\). Compute the alternatives \(w\in W\) minimizing \(q_\alpha(w)\). When \(\mu_t=n_t/n\) and \(\alpha=\tau_0/n\), this agrees with the finite \(F_{\tau_0}\) choice rule on equal-depth profiles.
Let \(W\) be an explicitly listed nonempty set of \(m\) distinct truth assignments over a finite nonempty propositional vocabulary. A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types.
Each type is an explicitly written priority list \(\varphi_t=A^t_1\triangledown\cdots\triangledown A^t_d\), with common depth \(d\ge1\), where each \(A^t_j\) is a propositional formula and every \(w\in W\) satisfies at least one \(A^t_j\). Earlier positions have higher priority; formulas may overlap, and empty levels retain their positions.
Given a binary-rational quota \(\alpha\in(0,1]\), define \(h_t(w)=\min\{j\in\{1,\ldots,d\}:w\models A^t_j\}\) and \(q_\alpha(w)=\min\{k\in\{1,\ldots,d\}:\sum_{t:h_t(w)\le k}\mu_t\ge\alpha\}\). The output is \(\operatorname*{arg\,min}_{w\in W}q_\alpha(w)\), including every tie. Let \(L\) be the total binary input length; state running times in \(m,\tau,d,L\).
Is computing this choice set solvable in polynomial time in \(m,\tau,d,L\), or is it NP-hard?
Known discrete result: RCL model checking, including computing the truth set of an explicitly supplied formula \(\psi\), takes \(O(m\lVert\psi\rVert)\) time, where \(\lVert\psi\rVert\) is its symbol count ([source](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p979.pdf)). This bound measures the supplied formula, including any expanded aggregate formula.
No result settling this exact support-encoded rational-mass problem was located in the search.
Computing the entire choice set is polynomial-time solvable. A conservative bound, including exact rational arithmetic, is \(O((m+\tau+1)L^2+m(\tau+d)L)\) bit operations.
The proof uses the explicitly listed assignments and support directly.
Write the input rationals as \(\mu_t=a_t/b_t\) and \(\alpha=a_0/b_0\), with positive integer numerators and denominators encoded in binary. Explicit terminating binary fractions can also be converted to this representation within polynomial time.
Define
\(D=\prod_{i=0}^{\tau}b_i,\qquad M_t=a_t(D/b_t),\qquad Q=a_0(D/b_0).\)
Every division is exact. For any subset \(T\subseteq\{1,\ldots,\tau\}\),
\(\sum_{t\in T}\mu_t\ge\alpha\quad\Longleftrightarrow\quad\sum_{t\in T}M_t\ge Q,\)
because multiplication by the positive integer \(D\) preserves inequalities.
The total bit length of the input denominators is \(O(L)\), so
\(\log_2 D=\sum_{i=0}^{\tau}\log_2 b_i=O(L).\)
Thus \(D\) has \(O(L)\) bits, even if its numerical value is large. Moreover, the hypotheses give
\(\sum_{t=1}^{\tau}M_t=D,\qquad 0<Q\le D.\)
Consequently, all weights, quota values, and partial weight sums used below have \(O(L)\) bits. Schoolbook multiplication and division compute these integers in \(O((\tau+1)L^2)\) bit operations.
Process each \(w\in W\) as follows.
For correctness, the bucket construction gives, for every position \(k\),
\(C_k(w)=\sum_{t:h_t(w)\le k}M_t =D\sum_{t:h_t(w)\le k}\mu_t.\)
Therefore,
\(C_k(w)\ge Q\quad\Longleftrightarrow\quad \sum_{t:h_t(w)\le k}\mu_t\ge\alpha.\)
The first position found by the scan is consequently exactly \(q_\alpha(w)\). The scan always succeeds: every type contributes to some bucket, so \(C_d(w)=D\ge Q\).
Overlapping formulas cause no double counting, because each type contributes only at its first satisfied position. Empty levels retain their indices and simply receive zero bucket weight.
Maintain a current minimum rank and a list of assignments attaining it. When processing an assignment with a smaller rank, replace the list by that assignment; when its rank equals the current minimum, append it.
After any nonempty prefix of the assignment list, this procedure stores exactly the assignments attaining the minimum rank within that prefix. This follows inductively from the three possibilities: smaller, equal, or larger rank. After all assignments have been processed, the stored list is therefore precisely
\(\operatorname*{arg\,min}_{w\in W}q_\alpha(w),\)
including every tie.
Let \(S=\sum_{t=1}^{\tau}\sum_{j=1}^{d}\lVert A^t_j\rVert\), so \(S=O(L)\).
Under the usual indexed-variable representation, bottom-up propositional evaluation takes \(O(S)\) Boolean operations per assignment: each formula node is evaluated once from its children, with atomic values supplied by the assignment. For a conservative bit-operation bound that also allows identifier lookup by scanning the explicit assignment, \(O(L^2)\) per assignment suffices. Thus all formula evaluation and rank extraction cost \(O(mL^2)\).
For each assignment, bucket initialization, the \(\tau\) weight additions, and the scan through \(d\) positions cost \(O((\tau+d)L)\) bit operations. Tracking the minimum and writing the explicitly listed winners fit within the resulting bound. Together with integer preprocessing, the total is
\(O((m+\tau+1)L^2+m(\tau+d)L).\)
This is polynomial in all requested parameters. Since the assignments, types, and levels are explicitly listed, \(m,\tau,d=O(L)\); the displayed bound is also \(O(L^3)\).
The supplied [RCL model-checking result](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p979.pdf) measures the size of the supplied formula. The algorithm above establishes the result directly, without requiring construction of an expanded aggregate formula.
⟨structured verdict parsed — rendered above⟩
The output proves that the entire choice set is computable in polynomial time. The algorithm matches the support-encoded input model, handles overlapping formulas and empty levels correctly, and includes every minimizing assignment. No major or minor issues were found.
The representations \(\mu_t=a_t/b_t\) and \(\alpha=a_0/b_0\) use positive denominators, so \(D>0\). Every denominator divides the product \(D\), making the divisions defining \(M_t\) and \(Q\) exact.
Multiplying the quota comparison by \(D\) preserves its direction. Thus the claimed equivalence between rational-mass comparisons and integer-weight comparisons is correct for every subset of supported types.
The bit-length estimate is also correct: the sum of the encoded denominator lengths is bounded by the total input length, so \(D\) has \(O(L)\) bits. The normalization and quota assumptions imply
\[
\sum_{t=1}^{\tau}M_t=D,\qquad 0<Q\le D.
\]
All weights are positive; consequently, each bucket and each partial sum is at most \(D\). The stated \(O(L)\)-bit bound covers the arithmetic used by the algorithm.
The preprocessing bound \(O((\tau+1)L^2)\) is valid with schoolbook arithmetic. It accommodates the denominator multiplications, exact divisions, and numerator multiplications. The possible intermediate products also have \(O(L)\) bits.
Evaluating each type’s formulas in their original order and recording the first satisfied position implements exactly the definition of \(h_t(w)\).
The coverage hypothesis ensures that this search succeeds for every assignment and every supported type. Neither mutual exclusivity nor nonemptiness of individual levels is assumed or needed.
Each supported type contributes its integer weight to exactly one bucket, indexed by \(h_t(w)\). Therefore, for every \(k\),
\[
C_k(w)=\sum_{t:h_t(w)\le k}M_t
=D\sum_{t:h_t(w)\le k}\mu_t.
\]
This identity justifies the quota test at every scanned position. Scanning in increasing order and stopping at the first successful comparison computes the minimum in the definition of \(q_\alpha(w)\).
The termination argument is valid: at position \(d\), all supported types have contributed, giving \(C_d(w)=D\ge Q\).
Overlapping formulas cannot double count a type because only its first satisfied position receives its weight. Empty levels preserve their positions and contribute zero.
The stated prefix invariant is correct. A smaller rank replaces the previous winners, an equal rank appends another winner, and a larger rank leaves the list unchanged.
Since \(W\) is nonempty, initializing the procedure from the first processed assignment is routine. The resulting list contains precisely every assignment attaining the global minimum. The distinctness assumption on \(W\) ensures there are no duplicate input assignments to propagate.
The total formula symbol count \(S\) is \(O(L)\). The stated linear Boolean-operation evaluation bound applies under the explicitly identified indexed-variable representation. Allowing scans of the explicit assignment gives the conservative \(O(L^2)\) bit-operation bound per assignment.
Bucket initialization, weight additions, prefix sums, and quota comparisons use \(O((\tau+d)L)\) bit operations per assignment. Maintaining the winners and writing their explicit assignments fit within the overall bound.
Combining these costs yields the claimed
\[
O((m+\tau+1)L^2+m(\tau+d)L).
\]
Because the assignments, supported types, and formula levels are explicitly listed, \(m,\tau,d=O(L)\); hence the further \(O(L^3)\) bound is valid.
The proof does not depend on the cited RCL theorem or an expanded aggregate formula. It directly resolves the exact input model in the task.
None 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.