← back to the atlas

d4-journals-jair-2022-0011 (d4-journals-jair-2022-0011)

Answer: \(\mathrm{NP}\text{-complete}\), already for \(\tau=1\) and \(\rho=1\).

The anchor (named result in the paper)

Theorem 25 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximate$DI^S$-WO-Orderability is \NP-complete.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite object set \(X\), an explicit menu \(\mathcal{X}\subseteq 2^X\setminus\{\emptyset\}\), a finite support \(T\) of linear-ranking types with positive rational masses \(\mu_t\) summing to \(1\), and a threshold \(\rho\in[0,1]\), decide whether types of total mass at least \(\rho\) admit weak orders on \(\mathcal{X}\) satisfying dominance and strict independence relative to their rankings; return those types and witnessing orders.

Packaged proof task (what the prover saw — nothing else)

Let \(X\) be a finite object set, with \(m=|X|\), and let \(\mathcal X\subseteq 2^X\setminus\{\emptyset\}\) be an explicitly listed menu, with \(q=|\mathcal X|\).
A society is given by its support: the list \(T\) of \(\tau\) distinct linear-ranking types with positive masses \(\mu_t\) encoded as binary rationals, where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible rankings. Each type supplies a linear order \(<_t\) on \(X\), with larger objects preferred.
The threshold \(\rho\in[0,1]\) is a binary rational. Let \(L\) be the total input bit length; state running times in \(m,\tau,q,L\).
For each selected type \(t\), a witnessing order \(\preceq_t\) is a weak order on \(\mathcal X\), with strict part \(\prec_t\); indifference is allowed.
Dominance: for every \(A\in\mathcal X\) and \(x\in X\) with \(A\cup\{x\}\in\mathcal X\), require \((\forall y\in A,\ y<_t x)\Rightarrow A\prec_t A\cup\{x\}\) and \((\forall y\in A,\ x<_t y)\Rightarrow A\cup\{x\}\prec_t A\).
Strict independence: for every \(A,B\in\mathcal X\) and \(x\in X\setminus(A\cup B)\) with both enlarged sets in \(\mathcal X\), require \(A\prec_t B\Rightarrow A\cup\{x\}\prec_t B\cup\{x\}\).
Decide whether there exists \(S\subseteq T\) with \(\sum_{t\in S}\mu_t\geq\rho\) such that every \(t\in S\) has such a witnessing order; on yes-instances, return \(S\) and its witnessing orders. Orders are chosen separately for each type; there are no further axioms or restrictions between types.

Is this mass-threshold decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard?

For one specified linear ranking and an explicit menu, existence of a weak order satisfying dominance and strict independence is \(\mathrm{NP}\)-complete. [Maly (2022)](https://arxiv.org/pdf/2104.05425)
No result specifically treating the stated distributional mass-threshold problem was located in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The decision problem is \(\mathrm{NP}\)-complete, already when \(\tau=1\) and \(\rho=1\). Consequently, a polynomial-time algorithm for the stated decision-and-witness task exists only if \(\mathrm P=\mathrm{NP}\).

1. Separability of the types

Call a type \(t\) feasible if its specified object ranking admits a weak order on \(\mathcal X\) satisfying both axioms. Define \(F=\{t\in T:t\text{ is feasible}\}\).

The instance is a yes-instance exactly when \(\sum_{t\in F}\mu_t\geq\rho\).

Indeed, every admissible selection \(S\) must satisfy \(S\subseteq F\), so its mass is at most the mass of \(F\). Conversely, if \(F\) has sufficient mass, select \(S=F\) and choose a witness separately for each type. These choices are compatible because the task imposes no conditions between types.

Thus selecting the types introduces no additional combinatorial obstruction. The difficulty lies in determining individual feasibility. For \(\rho=0\), the empty selection always suffices; the positive-threshold problem remains hard.

2. Polynomial certificates and verification

Index the explicitly listed menu as \(\mathcal X=\{A_1,\ldots,A_q\}\). For each selected type, a certificate supplies integers \(r_t(A_i)\in\{1,\ldots,q\}\), interpreted by
\(\displaystyle A_i\preceq_t A_j\iff r_t(A_i)\leq r_t(A_j)\).

This relation is reflexive, transitive, and total, hence a weak order. Its strict part satisfies
\(\displaystyle A_i\prec_t A_j\iff r_t(A_i)<r_t(A_j)\).
Equal ranks represent indifference.

Conversely, every weak order on a finite menu has such a representation: its indifference classes are linearly ordered, and assigning consecutive integers to those classes preserves all weak and strict comparisons. Consequently, these certificates lose no possible witnesses.

A certificate consists of the selected-type indicators and the rank assignments. Its length is \(\mathrm O(\tau+\tau q\log(q+1))\).

The verifier performs the following checks.

These checks enumerate every instance of the stated axioms, so acceptance is equivalent to certificate validity.

For an explicit running-time bound, encode menu sets as incidence vectors and precompute, for every \((A,x)\), the menu index of \(A\cup\{x\}\), when present. Scanning the menu for each lookup takes \(\mathrm O(m^2q^2)\) elementary bit comparisons. There are at most \(\tau mq\) dominance checks and \(\tau mq^2\) independence checks.

Exact mass arithmetic is also polynomial. A common denominator formed from the input denominators, including that of \(\rho\), has \(\mathrm O(L)\) bits: its bit length is bounded by the sum of their encoded lengths. Numerators and cross-products likewise have \(\mathrm O(L)\) bits. Schoolbook arithmetic therefore suffices.

A conservative bound for the entire verifier is
\(\displaystyle V(m,\tau,q,L)=\mathrm O\!\left((\tau+1)(m+1)^2(q+1)^2L^2+L^3\right)\).
This proves membership in \(\mathrm{NP}\). If \(q=0\), the empty menu has its unique weak order and needs no rank assignment.

3. Polynomial-time hardness reduction

The cited single-ranking theorem is precisely the required source problem: given a finite ground set, an explicit menu of nonempty subsets, and one specified linear object ranking, decide whether a weak order satisfies dominance and strict independence. Maly’s Theorem 25 establishes its \(\mathrm{NP}\)-completeness; the paper’s definitions allow indifference and use the same restricted-menu axioms. [Maly (2022), Sections 2.1–2.2 and Theorem 25](https://arxiv.org/pdf/2104.05425)

Given an instance \((X,\mathcal X,<)\) of that problem, retain its ground set and menu and construct:

This satisfies all input requirements: the single type is distinct, its mass is positive, the masses sum to one, and both numerical parameters have constant-length rational encodings. The construction takes linear time in the source input length.

Since the empty selection has mass zero, the only selection meeting the threshold is \(S=\{t\}\). Therefore the constructed instance is a yes-instance if and only if the original ranking admits the required weak order.

This is a polynomial-time many-one reduction, proving \(\mathrm{NP}\)-hardness. Together with Section 2, it proves \(\mathrm{NP}\)-completeness. The same reduction works for every fixed rational threshold satisfying \(0<\rho\leq1\).

4. Returning selections and witnessing orders

A concrete deterministic algorithm can enumerate all functions \(\mathcal X\to\{1,\ldots,q\}\) separately for each type, checking each assignment as above. Retain the first valid assignment for every feasible type. After all searches finish, compute their total mass.

If the mass reaches \(\rho\), return those types and their retained rank assignments, which explicitly specify their witnessing weak orders. Otherwise return no. Exhaustiveness follows from the representation proved in Section 2.

Writing \(Q=\max\{1,q\}\), this algorithm takes \(\mathrm O(Q^qV(m,\tau,q,L))\) time. It searches each type independently, so it does not require a joint enumeration of all types’ orders.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

Verdict: proved. The output correctly establishes \(\mathrm{NP}\)-completeness, including hardness when \(\tau=1\) and \(\rho=1\). It also provides a correct exhaustive algorithm for returning the requested witnesses. No major or minor mathematical issues were found.

1. Separability

The equivalence between a yes-instance and \(\sum_{t\in F}\mu_t\geq\rho\) is correct.

Every admissible selection consists exclusively of feasible types. Since all masses are positive, its mass cannot exceed the mass of \(F\). Conversely, selecting all feasible types works whenever their combined mass reaches the threshold: the menu and support are finite, and witnesses are chosen independently.

The observation about \(\rho=0\) is also correct. The empty selection satisfies the threshold and requires no witnesses.

2. Certificates and axiom verification

The integer-rank representation correctly describes precisely the weak orders on a finite menu:

The certificate length \(\mathrm O(\tau+\tau q\log(q+1))\) is a valid upper bound.

The dominance verifier checks both required implications for every applicable pair \((A,x)\). Allowing \(x\in A\) causes no problem: because \(A\) is nonempty, both antecedents then fail at \(y=x\).

The independence verifier retains all required applicability conditions, including \(x\notin A\cup B\) and membership of both enlarged sets in the menu. Its rank comparison is exactly the stated strict implication. Cases with \(A=B\) have a false antecedent.

Thus the verifier checks every required axiom instance without strengthening or weakening the task.

3. Running times and rational arithmetic

The lookup preprocessing bound is valid. There are \(mq\) enlargement lookups, each of which can scan \(q\) incidence vectors of length \(m\), giving \(\mathrm O(m^2q^2)\) bit comparisons.

The stated counts of at most \(\tau mq\) dominance instances and \(\tau mq^2\) independence instances are correct. Testing the dominance antecedents may additionally scan the objects in a set; the final verifier bound accommodates this cost.

The rational-arithmetic argument is sound. The product of the input denominators has bit length bounded by their aggregate encoded length. The mass sum and threshold comparison therefore involve integers of \(\mathrm O(L)\) bits. The normalization and nonnegativity of the masses also bound partial mass sums.

Consequently,
\[ V(m,\tau,q,L)=\mathrm O\!\left((\tau+1)(m+1)^2(q+1)^2L^2+L^3\right) \]
is a sufficiently conservative polynomial bound. Membership in \(\mathrm{NP}\) follows.

The empty-menu case is correctly handled: there is a unique relation on the empty menu, its weak-order properties and axioms hold vacuously, and no ranks are needed.

4. Cited hardness theorem

The citation is accurate. Maly’s definitions use weak orders with indifference permitted, a specified linear object ranking, and exactly the restricted-menu dominance and strict-independence conditions in the task. Theorem 25 establishes \(\mathrm{NP}\)-completeness of the corresponding single-ranking problem. It does not require the additional extension axiom. [Maly, Sections 2.1–2.4 and Theorem 25](https://arxiv.org/pdf/2104.05425)

Accordingly, the cited theorem supplies the source problem claimed by the prover. There is no mismatch between weak and linear witnessing orders or between specified-ranking and universally quantified ranking problems.

5. Reduction

The construction preserves the ground set, menu, and specified ranking, and adds one supported type with mass \(1\) and threshold \(1\). All distributional input requirements are satisfied.

There are exactly two selections. The empty selection fails the threshold, and the singleton selection meets it. Hence the constructed instance is accepted precisely when the source instance has a witnessing weak order.

The numerical additions have constant encoding length, and copying the source data takes linear time. This is a valid polynomial-time many-one reduction.

The extension to any fixed rational threshold \(0<\rho\leq1\) is also correct: the empty selection still fails, and the singleton still meets the threshold.

Together with membership, this establishes \(\mathrm{NP}\)-completeness. The stated consequence for a polynomial-time decision-and-witness algorithm follows from its decision component.

6. Witness-returning algorithm

For \(q>0\), there are exactly \(q^q\) functions from the menu to the rank set. The established representation ensures that this enumeration includes a witness for every feasible type.

Retaining one valid assignment per feasible type and subsequently testing their combined mass correctly implements the separability criterion. Returned rank assignments explicitly specify the required weak orders.

The bound \(\mathrm O(Q^qV(m,\tau,q,L))\), where \(Q=\max\{1,q\}\), is valid: \(V\) already accommodates verification across all supported types. For \(q=0\), the unique empty assignment is the sole candidate and \(Q^q=1\).

Required feedback

None. The argument resolves the assigned task and needs no mathematical repair.

⟨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.