← back to the atlas

d4-journals-jair-2017-0001 (d4-journals-jair-2017-0001)

Answer: \(\mathrm{NP}\text{-complete}\)

The anchor (named result in the paper)

Proposition 9 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateDeciding whether a profile of AF’s is rationalisable by an AVAF with a given fixed master attack-relation and a given upper bound (of at least 3) on the number of values is an NP-complete problem.

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

The continuous mirror question, as graded

Given a finite argument set \(\mathcal{A}\), a fixed attack relation \(\alpha\), a bound \(k \ge 3\), and a rational distribution \(\mu\) over reported audience types \(t=(S_t,D_t)\), does there exist a value set \(V\) with \(|V| \le k\), a common labelling \(\lambda:\mathcal{A}\to V\), and a preference preorder \(\succeq_t\) for each \(t\) with \(\mu_t>0\), such that for all \(a,b\in S_t\), \((a,b)\in D_t\) if and only if \((a,b)\in\alpha\) and \(\neg(\lambda(b)\succ_t\lambda(a))\)?

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

Given a finite argument set \(\mathcal A\), put \(m=|\mathcal A|\). The input includes an irreflexive attack relation \(\alpha\subseteq\mathcal A\times\mathcal A\) and a binary-encoded integer \(k\ge3\).
A society is given by its support: a list of \(\tau\) distinct reported types \(t=(S_t,D_t)\), each with a positive binary rational mass \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each \(S_t\subseteq\mathcal A\), each \(D_t\subseteq S_t\times S_t\) is irreflexive, and \(\mathcal A=\bigcup_t S_t\). Argument sets may differ, and empty reported sets are allowed.
A rationalisation consists of a finite value set \(V\) with \(|V|\le k\), a common labelling \(\lambda:\mathcal A\to V\), and a preference preorder \(\succeq_t\) on all of \(V\) for every supported type. Indifference and incomparability are allowed; \(\succ_t\) denotes the strict part.
It must satisfy, for every supported \(t\) and every \(a,b\in S_t\),
\( (a,b)\in D_t\iff (a,b)\in\alpha\ \land\ \neg(\lambda(b)\succ_t\lambda(a)). \)
There are no reporting constraints on pairs outside \(S_t\times S_t\). Let \(L\) be the total binary input length; state running times in \(m,\tau,L,k\).

Is deciding the existence of such a rationalisation for a society given by a rational distribution in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard?

For finite lists of audiences, the same rationalisation problem with a fixed attack relation and a value bound \(k\ge3\) is \(\mathrm{NP}\)-complete, including when preferences must be complete. [Airiau et al.](https://helios2.mi.parisdescartes.fr/~bonzon/Publis/JAIR17_AiriauBEMR.pdf)
No prior result explicitly treating the stated distribution version was located in the search.

Modeling choices made when packaging the task

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

Result

The stated decision problem is \(\mathrm{NP}\)-complete. Hardness already holds when \(k=3\) and all supported types have equal rational mass. Thus a polynomial-time algorithm for the general problem would imply \(\mathrm P=\mathrm{NP}\).

The distribution encoding does not change feasibility: only its support matters. Below, I prove this observation, give the reduction, and establish a polynomial verification algorithm that handles incomplete preorders and binary-encoded \(k\).

1. Masses and repeated reports do not affect feasibility

Fix \(\mathcal A,\alpha,k\) and a collection of supported types.

Every rationalisation constraint is indexed by a supported type and a pair of its reported arguments. No constraint involves \(\mu_t\). Consequently, changing the positive masses while preserving the support preserves rationalisability.

Repeated occurrences of the same reported type in an audience list can also be merged without changing feasibility:

These operations are valid because different audiences are allowed to have identical preferences.

2. Polynomial reduction from audience lists

Use the known \(\mathrm{NP}\)-hard audience-list problem stipulated in the question, with a supplied common attack relation and value bound \(k=3\). Its reporting condition is exactly the condition here: constraints apply only within each audience’s reported argument set. This is the model in Definition 4 and Proposition 9 of [Airiau et al.](https://helios2.mi.parisdescartes.fr/~bonzon/Publis/JAIR17_AiriauBEMR.pdf).

Given an instance with reports
\[ (S_1,D_1),\ldots,(S_n,D_n), \]
perform the following transformation:

The resulting masses are positive binary rationals summing to one. Removing duplicates preserves the union of reported argument sets, so the coverage requirement remains satisfied. Irreflexivity is preserved as well.

By Section 1,
\[ \text{the audience-list instance is rationalisable} \iff \text{the constructed distribution instance is rationalisable}. \]

Let \(N\) be the source instance’s binary length. Canonicalising and comparing the explicitly listed reports can be done in \(O(N^2)\) bit operations. Each mass \(1/\tau\) requires \(O(\log(\tau+1))\) bits, so the output length is
\[ O\!\left(N+\tau\log(\tau+1)\right). \]
Thus this is a polynomial many-one reduction. It proves \(\mathrm{NP}\)-hardness, already for uniform masses and \(k=3\).

3. Polynomial verification for a fixed labelling

I now prove membership in \(\mathrm{NP}\), without requiring preference matrices in the certificate.

First reject if some \(D_t\) contains a pair outside \(\alpha\); such a reported defeat cannot satisfy the required equivalence.

Fix a proposed labelling \(\lambda:\mathcal A\to V\). For each type define two relations on \(V\):
\[ R_t= \left\{ (\lambda(b),\lambda(a)): a,b\in S_t,\ (a,b)\in\alpha\setminus D_t \right\}, \]
and
\[ F_t= \left\{ (\lambda(b),\lambda(a)): (a,b)\in D_t \right\}. \]

A pair in \(R_t\) is a required strict preference. A pair in \(F_t\) is a forbidden strict preference. Let \(R_t^+\) denote reachability by paths of positive length.

Lemma. The proposed labelling admits the required preorders if and only if, for every supported type,
\[ R_t^+\cap\{(v,v):v\in V\}=\varnothing \quad\text{and}\quad R_t^+\cap F_t=\varnothing. \]

Proof: necessity. The strict part of any preorder is irreflexive and transitive. To verify the latter, suppose \(x\succ y\) and \(y\succ z\). Transitivity gives \(x\succeq z\). If \(z\succeq x\), then \(z\succeq y\), contradicting \(y\succ z\). Hence \(x\succ z\).

Any satisfying preorder must therefore contain \(R_t^+\) in its strict part. Its irreflexivity rules out diagonal pairs in \(R_t^+\), and the reporting constraints rule out its intersection with \(F_t\).

Proof: sufficiency. Suppose both conditions hold. Define
\[ \succeq_t\;=\;\{(v,v):v\in V\}\ \cup\ R_t^+. \]
This relation is reflexive and transitive. Moreover, \(R_t^+\) cannot contain both \((x,y)\) and \((y,x)\), since transitivity would then give a diagonal pair. Consequently, the strict part of \(\succeq_t\) is exactly \(R_t^+\).

Every omitted attack gives a pair in \(R_t\subseteq R_t^+\), so it is cancelled. Every reported defeat gives a pair in \(F_t\), which is absent from the strict part, so that attack is retained. Pairs outside \(\alpha\) are unreported by the initial rejection check. These are all required cases; there are no constraints outside \(S_t\times S_t\). This proves the lemma.

4. Certificate size and running times

If \(m=0\), the instance is immediately rationalisable using a singleton value set: all reporting constraints are vacuous.

Suppose \(m\ge1\), and put
\[ q=\min\{k,m\}. \]
Any rationalisation can be restricted to the values actually used by \(\lambda\). Restricting a preorder preserves reflexivity, transitivity, and all comparisons between used values. Thus at most \(q\) values are needed, regardless of the magnitude of binary-encoded \(k\).

A certificate consists of a labelling
\[ \lambda:\mathcal A\to\{1,\ldots,q\}, \]
requiring \(O(m\log(q+1))\) bits. Allowing unused labels causes no problem.

For each type, construct \(R_t,F_t\), compute \(R_t^+\) by Boolean transitive closure, and apply the lemma. After indexing the input relations, this takes
\[ O\!\left(L+\tau(m^2+q^3)\right) \]
time on a word RAM with \(O(\log(L+2))\)-bit words. A conservative bit-operation bound, including validation of the rational masses if desired, is
\[ O\!\left( L^3+\tau(m^2+q^3)\log(L+2) \right). \]
For mass validation, successive exact additions have intermediate numerator and denominator lengths \(O(L)\); schoolbook arithmetic gives the stated \(O(L^3)\) bound.

The certificate and verification time are polynomial in \(L\), proving membership in \(\mathrm{NP}\). Together with Section 2, this establishes \(\mathrm{NP}\)-completeness.

For completeness, enumerating the \(q^m\) labellings and applying the verifier gives a deterministic upper bound
\[ O\!\left( L^3+ q^m\tau(m^2+q^3)\log(L+2) \right) \]
in bit operations. All dependence on \(k\) is through \(q=\min\{k,m\}\) and reading its binary encoding.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the stated problem: deciding rationalisability is \(\mathrm{NP}\)-complete, including when \(k=3\) and the distribution is uniform on its support. The reduction and verification argument are correct. I found no major or minor mathematical issues.

1. Independence from masses and multiplicities

The feasibility condition contains no occurrence of \(\mu_t\). Because every supported type has positive mass, changing those masses while keeping the support leaves exactly the same constraints. The claimed independence from masses follows directly.

The treatment of duplicate reports is also correct in both directions:

This uses only the permitted independence of audiences’ preferences. No constraint requires different audiences to have different preferences.

2. The cited hardness result and reduction

The citation matches the required source problem. Definition 4 of [Airiau et al.](https://helios2.mi.parisdescartes.fr/~bonzon/Publis/JAIR17_AiriauBEMR.pdf) imposes the defeat equivalence only on pairs within each audience’s reported argument set and defines the global argument set as their union. Its preferences are preorders, allowing incomparability. Proposition 9 establishes hardness with a supplied master attack relation and a value bound of at least three; its construction applies with bound three.

Thus the prover is using hardness for the same preference model, rather than inferring hardness for unrestricted preorders solely from hardness under complete preferences.

The transformation satisfies every relevant target requirement:

The hardness source supplies nonempty audience lists, so division by \(\tau\) is well-defined.

The equivalence of source and target feasibility follows from the duplicate-removal argument and mass independence. Both directions preserve the common labelling and use admissible audience preorders.

The encoding bounds are valid. Explicit reports can be canonicalised and deduplicated in polynomial time, with the stated conservative \(O(N^2)\) bit bound. Each mass requires \(O(\log(\tau+1))\) bits. Consequently, the transformation is a polynomial many-one reduction.

3. Fixed-labelling verification

Preliminary rejection and relation definitions

Rejecting a report containing a defeat outside \(\alpha\) is necessary: the right-hand side of the required equivalence is then false irrespective of preferences.

After that rejection:

Both definitions therefore translate the reporting constraints correctly.

Necessity of the closure conditions

The proof that the strict part of a preorder is transitive is correct. Given \(x\succ y\) and \(y\succ z\), transitivity gives \(x\succeq z\). If \(z\succeq x\), then \(z\succeq y\), contradicting \(y\succ z\).

Accordingly, every satisfying strict preference relation contains \(R_t^+\). Its irreflexivity excludes diagonal pairs, while the retained-defeat constraints exclude intersection with \(F_t\). Both necessary conditions follow.

Sufficiency of the closure conditions

The proposed relation
\[ \succeq_t=\{(v,v):v\in V\}\cup R_t^+ \]
is reflexive and transitive.

The absence of diagonal pairs in \(R_t^+\) also excludes opposite directed pairs: their composition would yield a diagonal pair. Hence the strict part of the proposed preorder is exactly \(R_t^+\).

The resulting comparisons cancel every omitted attack and retain every reported defeat. For pairs outside \(\alpha\), the initial rejection ensures that no defeat is reported. These cases exhaust the required equivalence inside \(S_t\times S_t\).

The lemma is therefore proved in both directions. It also correctly handles empty reports, unused values, and required comparisons between arguments receiving the same label.

4. Certificate size and edge cases

For \(m=0\), all reporting constraints are vacuous. A singleton value set respects \(k\ge3\), and the empty labelling is valid.

For \(m\ge1\), restricting a rationalisation to values used by the labelling preserves every relevant comparison and preserves the preorder axioms. Thus at most
\[ q=\min\{k,m\} \]
values are needed.

Renaming those values gives the stated certificate. Its size \(O(m\log(q+1))\) is polynomial in the explicit input length. Unused labels are harmless because the constructed preorders are defined on the entire proposed value set.

Binary encoding of \(k\) introduces no oversized certificate: the algorithm compares \(k\) with \(m\) and never constructs a value set of size greater than \(m\).

5. Running times

For each type, scanning argument pairs and building the two relations costs \(O(m^2)\); Boolean transitive closure costs \(O(q^3)\). Checking the two closure conditions fits within these bounds. Thus the stated word-RAM bound
\[ O\!\left(L+\tau(m^2+q^3)\right) \]
is valid after indexing the input relations.

The conservative bit bound
\[ O\!\left(L^3+\tau(m^2+q^3)\log(L+2)\right) \]
is also valid. Exact successive additions of the input rational masses can use intermediate integers of \(O(L)\) bits, and schoolbook arithmetic gives the claimed conservative preprocessing bound.

The enumeration bound follows by applying the verifier to all \(q^m\) labellings, with input and mass preprocessing performed once.

Required feedback

No mathematical repair or additional clarification is needed. The proof establishes membership in \(\mathrm{NP}\) and the claimed hardness under the specified support encoding.

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