Answer: \(\mathrm{NP}\text{-complete}\), even for \(m=2\), \(\tau=2\), and \(k\leq2\); the complement is \(\mathrm{coNP}\text{-complete}\).
Theorem 4 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateOur tableau-based calculus is a sound and complete decision procedure to check whether there exists a voting rule that satisfies certain axiom instances and complies with certain outcome statements.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite alternative set \(X\), ranking types \(T=L(X)\), finite rational mass-profile axiom instances \(\alpha=(\mu^1,\ldots,\mu^k,R_\alpha)\) with \(R_\alpha\subseteq\Omega^k\), a rational \(\mu^\star\in\Delta(T)\), and \(X^\star\in\Omega=2^X\setminus\{\emptyset\}\), decide whether every anonymous homogeneous rule \(F_\infty:\Delta(T)\to\Omega\) satisfying all instances must satisfy \(F_\infty(\mu^\star)=X^\star\); equivalently, decide whether a rule satisfying the instances and \(F_\infty(\mu^\star)\in\Omega\setminus\{X^\star\}\) exists, and if not produce a closed tableau over the relevant mass profiles.
Let \(X\) be a nonempty finite alternative set, \(m=|X|\), \(T=L(X)\) the strict ranking types, and \(\Omega=2^X\setminus\{\emptyset\}\). A mass profile belongs to \(\Delta(T)\): its masses are nonnegative and sum to \(1\).
A society is given by its support: the list of its \(\tau\) types with positive mass, each with its mass as a binary rational; \(\tau\) denotes support size, not the number of possible types. For several input profiles, use \(\tau\) for the maximum support size.
An anonymous homogeneous rule is any function \(F_\infty:\Delta(T)\to\Omega\): on an unnormalized nonzero mass vector \(v\), its outcome is \(F_\infty(v/\sum_t v_t)\). No continuity or additional axioms are imposed.
Input consists of a finite family \(\mathcal A\) of instances \(\alpha=(\mu^1,\ldots,\mu^{k_\alpha},R_\alpha)\), with \(k_\alpha\geq1\), rational profiles, and \(R_\alpha\subseteq\Omega^{k_\alpha}\), plus rational \(\mu^\star\) and \(X^\star\in\Omega\). Each relation is an explicit list of allowed tuples, with outcomes encoded as \(m\)-bit subsets. Satisfaction means \((F_\infty(\mu^1),\ldots,F_\infty(\mu^{k_\alpha}))\in R_\alpha\); equal profiles always receive equal outcomes. Inconsistent instance families are allowed.
The decision problem asks whether a satisfying rule exists with \(F_\infty(\mu^\star)\neq X^\star\); its complement asks whether every satisfying rule selects \(X^\star\). In the absence of a counterrule, the associated search problem requests a closed tableau on the distinct input profiles \(Q\).
A tableau is a finite rooted tree of sets \(S\) of statements \(\langle\mu,O\rangle\), where \(\mu\in Q\), \(O\subseteq\Omega\), and \(I(S)\) denotes the rules satisfying every statement. Its root is \(\{\langle\mu^\star,\Omega\setminus\{X^\star\}\rangle\}\); write \(I(\alpha)\) for rules satisfying instance \(\alpha\).
An instance expansion appends \(S\cup\{\langle\mu,O\rangle\}\), for a profile occurring in \(\alpha\), with \(O=\{F_\infty(\mu):F_\infty\in I(S)\cap I(\alpha)\}\), only when this strictly reduces \(I(S)\).
Branching replaces one statement by either part of a partition of its allowed outcomes into two nonempty sets, creating two children; absent profiles may be branched on using the implicit statement \(\langle\mu,\Omega\rangle\). Simplification replaces two distinct statements about the same profile by their intersection. A tableau is closed when every leaf contains \(\langle\mu,\emptyset\rangle\).
Is counterrule existence solvable in polynomial time, or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L,a,q,k\), where \(L\) is total input bit length, \(a=|\mathcal A|\), \(q=|Q|\), and \(k=\max(\{1\}\cup\{k_\alpha:\alpha\in\mathcal A\})\).
For finite electorates, the tableau calculus is a terminating, sound and complete decision procedure for compatibility of finite axiom instances and outcome statements ([Boixel–Endriss–de Haan, 2022](https://staff.science.uva.nl/u.endriss/pubs/files/BoixelEtAlAAAI2022.pdf)).
Related discrete tasks using quantifier-free axiom encodings have \(\mathrm{DP}\)-complete justification verification and \(\Sigma_2^{\mathrm P}\)-complete justification existence; these impose additional justification requirements ([Boixel–de Haan, 2021](https://ojs.aaai.org/index.php/AAAI/article/download/16656/16463)). No result settling exactly the mass-profile problem above was located.
1. Result
Counterrule existence is \(\mathrm{NP}\)-complete, even when \(m=2\), \(\tau=2\), and \(k\leq 2\). Its complement is \(\mathrm{coNP}\)-complete. Thus a polynomial-time algorithm for the general problem exists if and only if \(\mathrm P=\mathrm{NP}\).
The stated tableau calculus is also sound, terminating, and complete on the finite set \(Q\). Below are explicit decision and tableau-construction bounds.
2. Reduction to a finite constraint problem
Write \(D=|\Omega|=2^m-1\), and include \(\mu^\star\) in \(Q\).
An assignment is a function \(f:Q\to\Omega\). Call it feasible when
\(\bigl(f(\mu^1),\ldots,f(\mu^{k_\alpha})\bigr)\in R_\alpha\)
for every \(\alpha\in\mathcal A\), and \(f(\mu^\star)\neq X^\star\).
Extension lemma. A counterrule exists if and only if a feasible assignment exists.
Proof. Restricting a counterrule to \(Q\) gives a feasible assignment. Conversely, fix any \(W_0\in\Omega\). Given a feasible assignment \(f\), define
\(F_\infty(\mu)=f(\mu)\) when \(\mu\in Q\), and \(F_\infty(\mu)=W_0\) otherwise.
This is a function on all of \(\Delta(T)\). It satisfies every input instance and the target inequality. Defining its value on an unnormalized vector by normalization gives the required homogeneous interpretation. No additional axiom restricts this extension. \(\square\)
Consequently, equal profiles must be identified, but distinct profiles impose no additional compatibility conditions beyond the listed relations.
This identification is polynomial-time. Reduce rational masses to canonical fractions, sort each support by its ranking, and compare the resulting lists. Let \(P\) denote the number of profile occurrences, including the target occurrence. Then \(P\leq ak+1\), and each occurrence contains at most \(\tau\) rankings, each encoded using \(O(m\log(m+1))\) bits. Exact arithmetic and naive pairwise comparisons give a conservative \(O(L^3)\) bit-operation bound. No enumeration of \(L(X)\) is needed.
After identification, each instance is an ordinary finite constraint whose variables are profiles in \(Q\). If a profile occurs twice in an instance, delete every listed tuple that assigns different outcomes to those two occurrences: such a tuple cannot be realized by a rule.
3. Membership in \(\mathrm{NP}\) and deterministic running times
A certificate gives one nonempty \(m\)-bit outcome for each of the \(q\) distinct profiles. Check the target inequality and scan each explicit relation for a matching tuple. The certificate has \(qm\) bits, and verification, including profile identification, takes \(O(L^3)\) time. Hence counterrule existence belongs to \(\mathrm{NP}\).
The explicit relation tables also permit a smaller exhaustive search than enumeration of all \(D^q\) assignments.
Let
\(r=\sum_{\alpha\in\mathcal A}|R_\alpha|\), and \(B=\min\{2^m-1,\max\{1,r\}\}\),
where the relation sizes may be measured before deleting unrealizable tuples.
For each profile occurring in an instance, choose one such instance and one occurrence position. Let \(C_\mu\) be the coordinate projection of its surviving relation at that position. Every feasible assignment must select its outcome for \(\mu\) from \(C_\mu\). In particular, \(|C_\mu|\leq B\). Remove \(X^\star\) from \(C_{\mu^\star}\) when the target profile is constrained.
If the target profile occurs in no instance and \(m\geq2\), fix any single outcome different from \(X^\star\). This cannot affect satisfaction of the instances.
Enumerate assignments from these candidate sets and check all relations. Every feasible assignment is represented, except that the unconstrained target outcome has been fixed harmlessly. Thus this algorithm is correct and runs in
\(O\bigl(L^3+B^qL^2\bigr)\)
bit operations. In particular, a simpler bound is
\(O\bigl(L^3+(2^m-1)^qL^2\bigr)\).
Here \(r\leq L\), so fixed \(q\) gives polynomial time even when \(m\) varies. The parameters \(\tau,a,k\) enter through the explicitly encoded input and the preprocessing bound above.
Two boundary cases are polynomial-time:
4. Hardness with two alternatives and binary constraints
We reduce from proper graph three-colourability, which is \(\mathrm{NP}\)-complete. This classical theorem applies to finite simple graphs; see [Garey, Johnson, and Stockmeyer](https://doi.org/10.1016/0304-3975%2876%2990059-1).
Let \(G=(V,E)\), with \(V=\{1,\ldots,n\}\) and \(n\geq1\). Restricting to nonempty graphs preserves hardness, since adding an isolated vertex preserves three-colourability.
Choose \(X=\{x,y\}\). Its three outcomes are
\(c_1=\{x\},\qquad c_2=\{y\},\qquad c_3=\{x,y\}\).
There are two ranking types, \(t_1:x\succ y\) and \(t_2:y\succ x\). Put \(h=\lceil\log_2(n+1)\rceil\), and for each vertex \(i\) define
\(\mu_i(t_1)=i/2^h,\qquad \mu_i(t_2)=(2^h-i)/2^h\).
Because \(1\leq i\leq n<2^h\), both masses are positive and sum to one. The profiles are pairwise distinct, have support size two, and use dyadic masses of \(O(\log(n+1))\) bits.
For every vertex, include a unary instance allowing all three outcomes. This ensures that even isolated vertices occur in \(Q\).
For every edge \(\{i,j\}\), include the binary instance
\(\alpha_{ij}=(\mu_i,\mu_j,R_{\neq})\),
where
\(R_{\neq}=\{(c_s,c_t):s,t\in\{1,2,3\},\ s\neq t\}\).
This relation has exactly six explicitly listed tuples. Finally, set \(\mu^\star=\mu_1\) and \(X^\star=c_1\).
We verify both directions.
If a counterrule exists, colour vertex \(i\) by \(s\) whenever \(F_\infty(\mu_i)=c_s\). Every edge instance requires different colours at its endpoints, so this is a proper three-colouring.
Conversely, suppose \(G\) has a proper three-colouring. Permute the three colour names so that vertex \(1\) does not receive colour \(1\). Such a permutation exists and preserves every edge inequality. Assign each \(\mu_i\) its corresponding outcome \(c_s\). This satisfies all instances and the target inequality. The extension lemma supplies a counterrule.
The reduction has
\(m=2,\quad \tau=2,\quad q=n,\quad a=n+|E|,\quad k\leq2\),
and total encoded length
\(L=O\bigl((n+|E|)\log(n+1)\bigr)\).
It is therefore a polynomial-time reduction. Together with membership in \(\mathrm{NP}\), it proves \(\mathrm{NP}\)-completeness.
The universal-selection question is exactly the logical complement, including when the family is inconsistent. Hence it is \(\mathrm{coNP}\)-complete.
5. Soundness and completeness of the tableau calculus
For a node \(S\), define its effective domain at \(\mu\in Q\) by
\(E_\mu(S)=\bigcap\{O:\langle\mu,O\rangle\in S\}\),
taking the intersection to be \(\Omega\) when no statement about \(\mu\) is present.
By the extension lemma, \(I(S)\neq\emptyset\) precisely when every effective domain is nonempty: statements constrain separate profile values independently.
Soundness. Suppose a counterrule satisfies the root and every instance.
An instance expansion preserves this rule because its selected outcome belongs to the defining projection of \(I(S)\cap I(\alpha)\). A simplification preserves exactly the rules satisfying the two original statements. At a branching step, the rule belongs to exactly one of the two children because the two parts partition the statement’s allowed outcomes.
Thus the counterrule can be followed from the root to a leaf. It cannot satisfy a statement with an empty allowed set. Therefore a closed tableau implies that no counterrule exists.
Completeness. Assume no counterrule exists.
If \(m=1\), the root already contains an empty allowed set. Otherwise, branch first on the target profile, then on every remaining profile, until every effective domain is a singleton. Use binary partitions throughout.
Each resulting leaf specifies exactly one assignment \(f:Q\to\Omega\) with \(f(\mu^\star)\neq X^\star\). Its interpretation is nonempty by the extension lemma. Since there is no counterrule, some instance \(\alpha\) fails under this assignment.
Every rule in \(I(S)\) has the same values at all profiles occurring in \(\alpha\). Consequently,
\(I(S)\cap I(\alpha)=\emptyset\).
Choose any profile occurring in \(\alpha\), which is possible because \(k_\alpha\geq1\). Its prescribed expansion set is empty. Appending this statement strictly reduces the nonempty \(I(S)\) to the empty set and closes the leaf. Repeating this at every leaf produces a closed tableau.
This proves completeness directly for the mass-profile model.
6. Termination and tableau-construction bounds
The calculus terminates on finite \(Q\), even without fixing the preceding branching strategy.
Along a path, every effective domain is nonincreasing. If an instance expansion strictly reduces \(I(S)\), then \(I(S)\) was nonempty and the expansion strictly reduces one effective domain. Once \(I(S)\) is empty, no further strict instance expansion is possible. Thus there are at most \(qD\) instance expansions along a path.
A previously absent profile can be introduced by branching at most once, giving at most \(q\) such steps. Consider the integer
\(W(S)=\sum_{\langle\mu,O\rangle\in S}|O|\).
Every other branching step strictly decreases \(W(S)\). Simplification also strictly decreases it: the two statements are distinct, and their intersection has smaller total cardinality than the two original allowed sets. Each instance expansion or branching on an absent profile increases \(W(S)\) by at most \(D\).
It follows that every path has \(O(qD^2)\) steps. Since every node has at most two children, no infinite tableau construction is possible.
For a more efficient construction, use balanced binary partitions in the completeness proof. For \(m\geq2\), its number of assignment leaves is
\(N=(D-1)D^{q-1}\leq D^q\).
The branching tree has at most \(2N-1\) nodes. One closing expansion per assignment leaf gives at most \(3N-1\) nodes in the closed tableau. The branching depth is at most \(qm\), followed by one closing expansion.
Even when every allowed-outcome set and every node label is written explicitly, a conservative construction-time bound is
\(O\bigl(L^3+D^q(L^2+qmD)\bigr)\),
or equivalently
\(O\bigl(L^3+(2^m-1)^q[L^2+qm(2^m-1)]\bigr)\).
This bound includes scanning the relations to find a violated instance at each assignment leaf and writing the tableau labels. It asserts existence of a closed tableau within that bound whenever no counterrule exists; it makes no assertion about minimum tableau size.
⟨structured verdict parsed — rendered above⟩
The output resolves the task correctly. Counterrule existence is \(\mathrm{NP}\)-complete under the stated explicit encoding, including the claimed restriction \(m=2\), \(\tau=2\), and \(k\leq2\). The tableau claims and running-time bounds also withstand verification. I found no major or minor mathematical issues requiring repair.
Restricting a rule to the distinct input profiles gives exactly the proposed assignment \(f:Q\to\Omega\). Conversely, the piecewise extension is well-defined because equal profiles have been identified and \(\Omega\neq\emptyset\).
All input instances concern profiles in \(Q\), so assigning a fixed outcome elsewhere cannot change their satisfaction. Normalization supplies the required interpretation on unnormalized nonzero mass vectors. No continuity or further compatibility condition is imposed by the task.
Thus the extension lemma establishes the claimed equivalence, including for inconsistent instance families.
Canonical rational fractions and sorted supports correctly recognize equality of the specified probability distributions. Zero-mass types need not be considered because the input lists precisely the positive support.
The bounds \(P\leq ak+1\) and the stated ranking-encoding size are valid. The conservative \(O(L^3)\) preprocessing bound accommodates exact rational arithmetic, sorting, and pairwise comparisons without enumerating all ranking types.
Deleting tuples that assign different outcomes to repeated occurrences of the same profile is valid: such tuples cannot be realized by any function. Tuples remaining after this filtering retain their original coordinate interpretation.
The certificate specifies one \(m\)-bit outcome for each distinct profile. Checking that each outcome is nonempty, checking the target inequality, and finding a matching explicitly listed tuple for every instance verify precisely the required conditions.
The certificate length \(qm\) is polynomial in the explicit input length. Relation scanning and profile preprocessing fit within the asserted \(O(L^3)\) bound. There is no requirement to encode a rule on the entire simplex, because the extension lemma establishes that the certificate suffices.
For each constrained profile, every feasible value must belong to the selected coordinate projection \(C_\mu\). Its cardinality is at most both \(D=2^m-1\) and the total number \(r\) of listed tuples. Consequently, the bound by
\[
B=\min\{2^m-1,\max\{1,r\}\}
\]
is valid, including when some projection is empty.
Removing \(X^\star\) from the constrained target domain implements the target inequality exactly. When the target is unconstrained and \(m\geq2\), fixing one permitted target value preserves existence of a feasible assignment.
The bounds \(O(L^3+B^qL^2)\) and \(O(L^3+D^qL^2)\) are conservative and valid. Since relation tuples are explicitly encoded, \(r\leq L\), establishing the fixed-\(q\) polynomial-time claim.
Both stated boundary cases are correct. For \(m=1\), the target exclusion is impossible. For \(k=1\), domain intersections characterize feasibility, with the target exclusion applied separately. Empty relations and inconsistent unary constraints are covered by the empty-domain test.
The invoked theorem is that proper three-colourability of finite simple graphs is \(\mathrm{NP}\)-complete; the cited paper supports this starting point. [Garey, Johnson, and Stockmeyer](https://www.sciencedirect.com/science/article/pii/0304397576900591)
The numerical construction checks out. For \(h=\lceil\log_2(n+1)\rceil\), one has \(n<2^h\). Hence both displayed masses are strictly positive and sum to one. Different vertex indices give different profiles, each with exactly two supported ranking types and \(O(\log(n+1))\)-bit masses.
The three nonempty subsets of a two-element alternative set are exactly the three proposed colours. Each edge relation lists precisely the six unequal ordered colour pairs. The unary instances include isolated vertices without restricting their colours.
Both reduction directions are valid:
The parameter values and encoded-length estimate are correct under the ordinary explicit graph encoding. Thus the reduction proves the claimed restricted hardness.
Universal selection is exactly the negation of counterrule existence. If the instance family is inconsistent, counterrule existence is false and universal selection is vacuously true, as the prover explicitly recognizes.
Therefore the \(\mathrm{coNP}\)-completeness conclusion follows. The assertion that a general polynomial-time algorithm exists exactly when \(\mathrm P=\mathrm{NP}\) also follows from membership and hardness.
The effective-domain description is valid because statements impose independent restrictions on profile values. A rule satisfying the root and all instances survives each instance expansion and simplification, and follows exactly one child at each branch. An empty-outcome statement cannot be satisfied. This establishes soundness.
The completeness construction uses only permitted operations. Branching on the target and then the other profiles produces singleton assignments satisfying the root exclusion. Each such leaf has nonempty interpretation.
If no counterrule exists, every resulting assignment violates an instance. At that leaf, all profiles occurring in the violated instance already have fixed values, so \(I(S)\cap I(\alpha)=\emptyset\). Its projection at any occurring profile is therefore empty. Appending that statement strictly reduces the nonempty interpretation and closes the leaf.
The condition \(k_\alpha\geq1\) supplies the profile needed for this expansion. The case \(m=1\) is handled separately by the already-closed root.
Effective domains are nonincreasing along each path. Every strict instance expansion reduces one effective domain while the interpretation is nonempty; none is possible once the interpretation is empty. The bound of \(qD\) such expansions is therefore valid.
Branching on an absent profile can introduce it only once. Every other branch strictly decreases \(W(S)\). Simplification also strictly decreases \(W(S)\): two distinct statements about one profile cannot both have the same empty allowed set. Each expansion or absent-profile branch increases \(W(S)\) by at most \(D\). These observations justify the \(O(qD^2)\) path bound and termination.
For the explicit completeness construction, the assignment-leaf count \((D-1)D^{q-1}\), the node bounds, and the depth bound \(qm+1\) are correct. The construction-time bound covers relation scanning, explicit outcome sets, and repeated profile descriptions through its \(L^2\) term. It is correctly stated as an upper bound rather than a minimum-size claim.
No additional lemma or clarification is needed to verify the conclusions.
⟨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.