d4-conf-atal-2021-0227 (d4-conf-atal-2021-0227)

Given a finite agenda \(\Phi\), a target formula \(\phi^\star\), and a rational distribution \(\mu\) over complete, consistent judgment types \(t\), does there exist an order \(\pi\) of \(\Phi^+\) such that \(\phi^\star\) belongs to the sequential outcome? At each step, use logical entailment from earlier decisions when it determines the formula's value; otherwise select \(\phi\in\Phi^+\) when \(\mu(\phi)>1/2\), and select its complement when \(\mu(\phi)\le 1/2\), where \(\mu(\phi)=\sum_{t:\phi\in t}\mu_t\).

The input agenda \(\Phi\) is a finite, nonempty set of explicitly encoded propositional formulas, closed under complement and containing no tautologies or contradictions. Write \(\sim\phi=\neg\phi\), cancelling an existing outer negation. The input specifies \(\Phi^+\), containing exactly one representative of each complement pair; let \(m=|\Phi^+|\). Require two formulas \(a,b\in\Phi\) for which all four choices of their signs are jointly satisfiable.
A society is given by its support: a list of \(\tau\) distinct complete, consistent judgment types \(t\subseteq\Phi\), each with positive binary rational mass \(\mu_t\), with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Types are explicitly listed; these input conditions are promises. Let \(L\) be the total input bit length, including formulas and masses; state running times in \(m,\tau,L\).
Given a target \(\phi^\star\in\Phi\), an order \(\pi\) processes every member of \(\Phi^+\) exactly once. Start with \(J=\varnothing\). When processing \(\phi\), append whichever of \(\phi,\sim\phi\) is logically entailed by \(J\), if either is entailed; otherwise append \(\phi\) if \(\mu(\phi)=\sum_{t:\phi\in t}\mu_t>1/2\), and append \(\sim\phi\) otherwise. Entailment uses unrestricted propositional semantics; the distribution stays fixed.

Is deciding whether some order \(\pi\) yields a final judgment containing \(\phi^\star\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finite lists of judges, this single-formula order-design problem is \(\Sigma_2^p\)-complete for every quota rule, including strict majority with ties resolved toward complements of \(\Phi^+\). [Baumeister, Boes and Weishaupt (2021)](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p187.pdf).
No complexity result for exactly the rational-support distribution formulation was located in the literature search.

Result

The rational-support problem is \(\Sigma_2^p\)-complete under polynomial-time many-one reductions, and therefore is \(\mathrm{NP}\)-hard. In particular, a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{NP}\).

The key observation is that an explicitly listed finite society can be converted into a rational-support society by merging repeated judgment types. This preserves the outcome for every processing order.

Exact arithmetic and the upper bound

Enumerate the representatives as \(\Phi^+=\{\phi_1,\ldots,\phi_m\}\). Define the preferred sign of each representative by
\[ d_i= \begin{cases} \phi_i,&\mu(\phi_i)>1/2,\\ \sim\phi_i,&\mu(\phi_i)\leq 1/2. \end{cases} \]
Here and below, the distribution remains fixed throughout processing.

Write the input masses as \(\mu_t=p_t/q_t\), with positive binary integers \(p_t,q_t\). Set
\[ D=\prod_t q_t, \qquad w_t=p_t(D/q_t). \]
These are integers, and the normalization promise gives
\[ \sum_t w_t=D. \]
Consequently,
\[ \mu(\phi_i)>1/2 \quad\Longleftrightarrow\quad 2\sum_{t:\phi_i\in t}w_t>D. \]
Thus every preferred sign, including the prescribed handling of ties, can be computed exactly.

The bit length of \(D\) is at most the sum of the denominator bit lengths, hence is \(O(L)\). Also, \(0<w_t\leq D\), and every partial support sum is at most \(D\). Using ordinary quadratic-time integer arithmetic, constructing the incidence table and computing all preferred signs takes at most \(O(m\tau L^2)\) bit operations. This is a conservative polynomial bound.

For a fixed order, maintain the conjunction \(C\) of the judgments already appended. The sequential rule is equivalent to the following operation when processing \(\phi_i\):

• If \(C\wedge d_i\) is satisfiable, append \(d_i\).
• Otherwise, append \(\sim d_i\).

To justify this equivalence, first observe that \(C\) stays satisfiable. Initially it is the empty conjunction. If \(C\wedge d_i\) is satisfiable, appending \(d_i\) preserves satisfiability. If it is unsatisfiable, every model of \(C\) satisfies \(\sim d_i\), so appending \(\sim d_i\) also preserves satisfiability.

Now suppose \(C\wedge d_i\) is satisfiable. Then \(C\) cannot entail \(\sim d_i\). Whether \(C\) entails \(d_i\) or entails neither sign, the specified rule appends \(d_i\). Conversely, if \(C\wedge d_i\) is unsatisfiable, then \(C\) entails \(\sim d_i\), so the rule appends that sign. These exhaust the cases.

A nondeterministic algorithm can therefore guess a permutation of the \(m\) representatives and simulate it with at most \(m\) queries to a satisfiability oracle. Each query has length \(O(L)\): it contains at most one chosen sign from each processed complement pair.

The ordinary computation takes \(O(m\tau L^2+mL+m\log m)\) bit operations, in addition to those oracle queries. Hence, on the promised inputs, the problem belongs to \(\mathrm{NP}^{\mathrm{NP}}=\Sigma_2^p\).

Reduction from explicitly listed finite societies

We use the stated finite-society hardness result. Specifically, Theorem 5.9 of [Baumeister, Boes and Weishaupt (2021)](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p187.pdf) establishes \(\Sigma_2^p\)-hardness for single-formula winner design under their quota rule with \(q=1/2\). Their agenda definition includes complement closure, absence of tautologies and contradictions, and the existence of two formulas admitting all four sign combinations.

Let a source instance have an explicitly listed profile
\[ P=(P_1,\ldots,P_r), \]
where \(r\geq 1\), and target \(\phi^\star\). Its agenda and chosen representatives satisfy the promises in the question.

Keep the agenda, representatives and target unchanged. For every distinct judgment type \(t\) occurring in the profile, let
\[ c_t=\bigl|\{j\in\{1,\ldots,r\}:P_j=t\}\bigr| \]
and assign it the rational mass
\[ \mu_t=\frac{c_t}{r}. \]

This produces a valid rational-support instance:

• The support types are distinct by construction.
• Each type is complete and consistent because it is one of the source judgments.
• Each mass is positive.
• The masses sum to one because \(\sum_t c_t=r\).
• Every agenda promise is preserved because the agenda is unchanged.

For every agenda formula \(\psi\),
\[ \mu(\psi) =\frac{|\{j:\psi\in P_j\}|}{r}. \]
The source quota rule selects a representative \(\phi_i\) exactly when its approval count reaches
\[ \left\lceil\frac{r+1}{2}\right\rceil =\left\lfloor\frac r2\right\rfloor+1. \]
For an integer approval count, this is equivalent to strict majority. Thus the preferred signs agree in the two instances, including when an even-sized society produces a tie.

Preservation of every order and polynomial size

Fix any order \(\pi\). We prove by induction over its processing steps that the source instance and the constructed rational-support instance append exactly the same judgments.

Initially both judgment sets are empty. Suppose their judgments agree before processing a representative. Since the formulas and accumulated judgments agree, both instances have identical entailment relations. If either sign is entailed, both append that sign. If neither is entailed, both append the same preferred sign, by the support-count calculation above. This proves the inductive step.

Their final judgments therefore agree for every order. In particular,
\[ \exists\pi:\phi^\star\in J_{\mathrm{finite}}(\pi) \quad\Longleftrightarrow\quad \exists\pi:\phi^\star\in J_{\mathrm{support}}(\pi). \]

Let \(N\) be the source input bit length. Because the judges are explicitly listed, \(r\leq N\). Each numerator and denominator used in the reduction has \(O(\log(r+1))\) bits, and the output support size satisfies \(\tau\leq r\). Retaining one copy of each distinct judgment therefore gives output length
\[ L=O\bigl(N+\tau\log(r+1)\bigr). \]
Direct comparisons suffice to merge repeated judgments in polynomial time; a conservative bound is \(O(N^3)\) bit operations. No enumeration of unlisted possible types is required.

This is a polynomial-time many-one reduction from the \(\Sigma_2^p\)-hard finite-society problem. Combined with the upper bound, it proves \(\Sigma_2^p\)-completeness.

For completeness, a deterministic exhaustive algorithm can compute the preferred signs once and then simulate all \(m!\) orders. Enumerating truth assignments for each satisfiability query gives the conservative running-time bound
\[ O\bigl(m\tau L^2+m!\,mL\,2^L\bigr). \]
The polynomial oracle bound above is the relevant upper bound for the complexity classification.

⟨structured verdict parsed — rendered above⟩

Verdict: proved. The output establishes \(\Sigma_2^p\)-completeness, and hence \(\mathrm{NP}\)-hardness, for the promised rational-support inputs. No major or minor mathematical issues were found.

• The cited hardness result applies.

Theorem 5.9 establishes \(\Sigma_2^p\)-completeness of single-formula Winner-Design for every quota rule in the paper’s defined family. Its definition asks whether some order over \(\Phi^+\) produces an outcome containing the target. The paper’s agenda and individual-judgment requirements match the task’s promises, including the independent pair of formulas. Definition 2.2 also uses the same fixed-profile, entailment-first sequential procedure. Thus the source problem is the required finite-society problem. [Baumeister, Boes and Weishaupt (2021), Definitions 2.1–2.2 and Theorem 5.9](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p187.pdf).

• Exact rational arithmetic is valid and polynomial.

Every denominator divides \(D=\prod_t q_t\), so each \(w_t=p_t(D/q_t)\) is an integer. Positivity and normalization give \(\sum_t w_t=D\), hence \(0<w_t\leq D\).

Multiplication adds denominator bit lengths, so \(D\) has \(O(L)\) bits. The support sums also have \(O(L)\) bits. Comparing twice the relevant support sum with \(D\) therefore determines strict majority exactly, including equality.

The claimed \(O(m\tau L^2)\) preprocessing bound conservatively covers ordinary integer arithmetic and construction of the incidence table. No precision or denominator-growth gap occurs.

• The satisfiability-based simulation matches the specified rule.

The consistency invariant is correctly established from the empty conjunction. When \(C\wedge d_i\) is satisfiable, appending \(d_i\) preserves consistency. Otherwise, satisfiability of \(C\) implies that every model of \(C\) satisfies \(\sim d_i\).

In the first case, \(C\) cannot entail the opposite sign. Whether it entails \(d_i\) or neither sign, the original procedure chooses \(d_i\). In the second case, the original procedure chooses the entailed opposite sign. Consistency excludes simultaneous entailment of both signs.

This verifies the equivalence at every step.

• The upper bound follows.

A permutation has polynomial encoding length and can be guessed and checked in polynomial time. Each simulation makes at most \(m\) SAT queries.

Each query contains at most one formula from each relevant complement pair, plus conjunction syntax, so its length is \(O(L)\). The stated ordinary-computation bound is conservative. Consequently, the algorithm belongs to \(\mathrm{NP}^{\mathrm{NP}}=\Sigma_2^p\).

This is correctly scoped to promised inputs; validating the promises is not required.

• The merging reduction produces valid support instances.

Grouping identical source judgments and assigning mass \(c_t/r\) gives distinct support types, positive binary rational masses, and total mass one. Each retained type inherits completeness and consistency.

The agenda, representatives, and target remain unchanged, so all agenda promises are preserved. For every formula, the constructed support probability equals its source approval fraction.

• The quota and tie conventions agree.

For positive integer \(r\), the source threshold at quota \(1/2\) is
\(\lceil(r+1)/2\rceil=\lfloor r/2\rfloor+1\). Reaching this threshold is exactly equivalent to an approval fraction strictly greater than \(1/2\).

For even \(r\), an equal split fails this threshold and selects the complement. The cited quota definition explicitly uses this tie convention. [Definition 2.1](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p187.pdf).

• Preservation holds for every order.

The induction compares the same representative under identical accumulated judgments. Entailment therefore agrees in both instances. When neither sign is entailed, the equality of preferred signs gives identical choices.

Thus final judgments agree for every permutation. The existential target condition is preserved in both directions, including when the target is a complement representative.

• The reduction and exhaustive running-time bounds are sound.

Explicit listing gives \(r\leq N\), while \(\tau\leq r\). Each multiplicity numerator and denominator needs \(O(\log(r+1))\) bits. Retaining only distinct judgments therefore satisfies the stated output-length bound. Direct comparisons can merge judgments within the conservative \(O(N^3)\) bound.

The exhaustive algorithm considers \(m!\) orders and at most \(m\) satisfiability checks per order. Explicit formulas contain at most \(L\) distinct variables; exhaustive assignment evaluation therefore supports the stated \(O(m\tau L^2+m!\,mL\,2^L)\) bound.

Repair feedback: None is required. The reduction settles the requested hardness alternative, and the independent upper bound supports the stronger completeness claim.

⟨structured verdict parsed — rendered above⟩