Answer: Polynomial-time solvable; the exact computation belongs to \(\mathrm{FP}\).
Proposition 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateUnder UN, the length of the dialogue resulting from the protocol is at most: 7 |P| + 2 |O| (|O| −1) + 1 where P is the knowledge base of the DM. The size of P depends on the number of criteria. One can easily derive bounds of |P| from the type of models that the DM is expected to follow.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given shared options \(O\), criteria \(H\), and model family \(\Pi\), let \(T\) be a finite support of complete decision-maker types with binary rational masses \(\mu_t\) summing to one. Each type specifies a consistent preference base and an efficiently evaluable response policy; the instance also specifies a deterministic decision-aider move-selection policy so the dialogue is determined. Execute the paper's protocol under UN independently for each type. Compute each type's terminal state \(z_t\) (success or failure, and the recommendation if successful), the exact mass of each terminal state, and the average number of moves \(\bar{\ell}=\sum_{t\in T}\mu_t\ell_t\).
The input has finite nonempty sets of options \(O\), criteria \(H\), and models \(\Pi\), with \(m=|O|\), and explicitly listed finite evaluation and importance scales \(S_O,S_H\). A society is given by its support: the list of the \(\tau\) types with positive binary rational masses \(\mu_t\), summing to one; \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total input bit length.
Preference information consists of atoms \([c:x=\alpha]\), \([x\succ_c y]\), and \([c=\beta]\), where \(x\ne y\), \(\alpha\in S_O\), and \(\beta\in S_H\). A base is consistent when evaluations and importance assignments are single-valued and each criterion's strict comparisons are acyclic. Global comparison atoms are \([x\succ y]\); their negations mean \([y\succ x]\), extended elementwise to sets.
Each model supplies its allowed information atoms \(\mathcal P(\pi)\), a property set \(Q_\pi\), and an evaluator producing a strict total order from any consistent allowed base, including incomplete bases. Property sets identify models uniquely, include the empty set, are intersection-closed, and every nonempty property set has a one-property deletion in the family. The model at an intersection allows exactly the intersection of the two models' allowed atoms. Every base contained in a type's base has a compatible model; \(\pi[B]\) denotes the compatible model with inclusion-smallest property set. Write \(B\models_\pi\phi\) when the model's order contains every comparison in \(\phi\).
The input goal \(G\) is ranking or best-option selection. The current recommendation \(R\) contains all ordered pairs of the model's order for ranking, or all comparisons of its top option against the others for selection. Defaults and tie-breaking are part of the model evaluator, whose output must be a strict total order.
Each type supplies an explicit fixed consistent base \(P_t\), an initial aider base \(B_t\subseteq P_t\), and a deterministic response policy. The instance supplies a deterministic aider policy resolving every permitted choice, including explanations and commitment revisions. Model evaluators and both policies are uniformly polynomial-time evaluable in their descriptions and the encoded dialogue history, with a fixed polynomial bound. Policies are promised legal; information supplied by a type belongs to \(P_t\). Initially the accepted-comparison store \(A\) and both commitment stores \(D,E\) are empty.
A nonterminal iteration starts with the aider's Assert or Question of a nonempty comparison set. The maker may Accept a nonempty subset, Challenge a nonempty subset, or Contradict a nonempty subset. A Challenge receives an aider Argue of a nonempty subset with an explanation \(p\subseteq B\) entailing it under \(\pi[B]\); the maker then Accepts, Contradicts, or Argues a nonempty subset or a conflicting comparison set, supplying \(p'\subseteq P_t\). A Contradict receives an aider Challenge of a nonempty subset of the negated comparisons, followed by a maker Argue of a nonempty subset with information from \(P_t\). Maker Accept and Argue return to Update. Conflict means containing opposite comparisons.
Assert and Accept add their comparison atoms to the speaker's commitment store; Contradict adds their negations; Argue adds its comparison and information atoms; Question and Challenge do not alter commitments. Maker commitments are retained throughout. Aider commitments may be revised at Update by its policy. Let \(E^-\) be the aider store immediately before the preceding iteration.
At Update, except initially, Fail if \(D\subseteq B\cup A\cup E^-\). Otherwise add \(D\cap\bigcup_{\pi\in\Pi}\mathcal P(\pi)\) to \(B\), failing if inconsistent; select \(\pi[B]\), and add to \(A\) every comparison in \(D\) entailed by \(B\) under that model. Compute \(R\); Succeed with \(R\) if \(R\setminus A=\varnothing\). Otherwise, if a maker commitment opposes \(R\), Assert a nonempty set of its negations; otherwise Question a nonempty subset of \(R\setminus A\) if \(R\) is unchanged, and Assert such a subset if it changed or this is the first iteration. Repeating a proposal requires newly supplied preference information; otherwise Fail. Update itself is not a move; each utterance, including the terminal one, is a move.
Run an independent dialogue for each type. Its terminal state \(z_t\) is failure or success together with its recommendation, and \(\ell_t\) is its move count. The requested output is every \(z_t\), every nonzero terminal-state mass \(M_z=\sum_{t:z_t=z}\mu_t\), and the exact rational average \(\bar\ell=\sum_t\mu_t\ell_t\).
Is this exact computation polynomial-time solvable, or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L,|H|,|\Pi|,|Q|,|S_O|,|S_H|\), where \(Q=\bigcup_{\pi\in\Pi}Q_\pi\).
For an individual discrete dialogue, the established move bound under the update rule is \(7|P_t|+2m(m-1)+1\), implying termination but not classifying computational time. [Verified source](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p959.pdf). No result settling this exact distributional computation was identified in the search.
Proven result. The exact computation is polynomial-time solvable under the stated promises. In particular, it belongs to \( \mathrm{FP} \). The proof combines deterministic simulation, polynomial-time model selection, a polynomial bound on encoded histories, and exact rational aggregation.
Write \( h=|H| \), \( r=|\Pi| \), \( q=|Q| \), \( a=|S_O| \), and \( b=|S_H| \). Define
\( K=m(m-1) \),
\( U=h(ma+K+b) \).
Here \( K \) counts all possible global comparison atoms, and \( U \) counts all possible preference-information atoms.
If \( m=1 \), the initial recommendation is empty for either goal. Every dialogue immediately succeeds with one terminal move, so the computation is immediate. The argument below also covers this case.
Model-selection lemma. For every base encountered during a dialogue, its compatible model with inclusion-smallest property set can be found by scanning the supplied models.
For a base \( B \), define
\( \mathcal C(B)=\{\pi\in\Pi:B\subseteq\mathcal P(\pi)\} \).
First, \( B\subseteq P_t \) throughout the dialogue for type \( t \). This holds initially. Subsequently, the only preference-information atoms added to \( B \) come from maker commitments, and all such information belongs to \( P_t \). Consequently, the compatibility promise makes \( \mathcal C(B) \) nonempty.
Suppose \( \pi_1,\pi_2\in\mathcal C(B) \). The model \( \pi_{12} \) associated with their property-set intersection satisfies
\( Q_{\pi_{12}}=Q_{\pi_1}\cap Q_{\pi_2} \),
\( \mathcal P(\pi_{12})=\mathcal P(\pi_1)\cap\mathcal P(\pi_2) \).
Because both allowed-atom sets contain \( B \), their intersection contains \( B \). Thus \( \pi_{12}\in\mathcal C(B) \).
Repeatedly applying this argument to the finite nonempty family \( \mathcal C(B) \) produces a compatible model \( \pi_* \) satisfying
\( Q_{\pi_*}=\bigcap_{\pi\in\mathcal C(B)}Q_\pi \).
Therefore \( Q_{\pi_*}\subseteq Q_\pi \) for every compatible model \( \pi \). Property sets identify models uniquely, so \( \pi_* \) is the unique inclusion-smallest compatible model.
It follows that an algorithm can test compatibility for every supplied model and retain one whose property set has minimum cardinality. Every other compatible property set contains \( Q_{\pi_*} \), and a proper superset has larger cardinality. Hence this procedure returns precisely \( \pi[B] \).
With bit vectors for allowed atoms and properties, this scan takes \( O(r(U+q+1)) \) elementary bit-vector operations. No enumeration of subsets of \( Q \) is needed.
Simulation and history-size bounds. Let \( p_t=|P_t| \). Consistency gives the useful bound
\( p_t\leq C:=h\left(m+\binom m2+1\right) \).
Indeed, each criterion permits at most one evaluation assignment per option and one importance assignment. Its strict comparisons contain at most one orientation of each unordered option pair: both orientations would constitute a directed cycle.
Use the supplied move bound
\( T_t:=7p_t+2K+1 \).
This is the bound stated in Proposition 1 of the [cited dialogue paper](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p959.pdf); the present argument uses it as a premise of the task.
For each type, simulate the protocol while maintaining \( B,A,D,E \), the required snapshot \( E^- \), the current and preceding recommendations, the dialogue history, and the move counter. Each transition is computable as follows.
There are \( O(T_t+1) \) updates and policy or evaluator invocations. It remains to check that their inputs have polynomial length.
Every utterance contains only a comparison set, a preference-information set where applicable, and a fixed locution label. The respective atom universes have sizes \( K \) and \( U \). Encoding atoms using identifiers derived from the input gives polynomial-length utterances. Consequently, a history containing at most \( T_t \) utterances has polynomial length. Commitment stores and other recorded state also contain only atoms from these finite universes.
The fixed polynomial bound on policy and evaluator computation therefore applies to polynomial-length inputs. It follows that the entire dialogue is computable in polynomial time.
Correctness follows by induction on transitions: initialization matches the specified initial state; each update performs exactly the specified tests and additions; the lemma returns the prescribed model; and deterministic policies select the prescribed utterances and revisions. Thus the simulation returns the actual \( z_t \) and \( \ell_t \).
Explicit running-time bound. The following conservative bound makes all requested parameter dependencies explicit. Let
\( T=\max_t T_t=7\max_t p_t+2K+1 \),
\( N=1+U+K+q+m+h+r+a+b \).
In particular,
\( T\leq 7h\left(m+\binom m2+1\right)+2m(m-1)+1 \).
Choose a fixed integer \( d\geq 1 \) such that policy and evaluator calls on inputs of length \( s \) cost \( O(s^d) \). Such a \( d \) exists by the uniform fixed polynomial-bound promise.
Histories and call inputs can be encoded in \( O(L(T+1)N) \) bits. After indexing atoms, preprocessing costs at most \( O(L^2+LrN) \) bit operations. Per update or utterance, model scanning, set operations, consistency checks, and a direct history scan cost at most
\( O\!\left(L(r+T+1)N\right) \).
For the consistency term, observe that \( h(m+K)\leq 2hK+h\leq 2U+h \), so it is covered by this bound.
Including aggregation proved below, one valid total bit-operation bound is
\( O\!\left( L^2+LrN+ \tau(T+1)\left[(L(T+1)N)^d+L(r+T+1)N\right] +\tau^2LN +\tau\left(L+\log(T+1)\right)^3 \right) \).
The unspecified exponent \( d \) reflects the supplied policies and evaluators; their hypothesis does not support a universal numerical exponent independent of that bound.
All listed cardinalities are bounded by the explicit input length up to encoding constants. Moreover, \( \max_t p_t=O(L) \), so \( U=O(L^3) \), \( N=O(L^3) \), and \( T=O(L^2) \). Hence the displayed bound is polynomial in \( L \).
Exact rational aggregation. Write each positive input mass as \( \mu_t=u_t/v_t \), with positive integers \( u_t,v_t \), and form the common denominator
\( V=\prod_{t=1}^{\tau}v_t \).
Its binary length is at most a constant plus the sum of the input denominator lengths, hence \( O(L) \). Define the integer weights
\( w_t=u_t(V/v_t) \).
Then \( \mu_t=w_t/V \), and the normalization promise gives
\( \sum_t w_t=V \).
For each terminal state actually encountered, compute
\( W_z=\sum_{t:z_t=z}w_t \),
and compute
\( W_\ell=\sum_t w_t\ell_t \).
The required outputs are exactly
\( M_z=W_z/V \),
\( \bar\ell=W_\ell/V \).
Because the weights are positive and \( \ell_t\leq T \),
\( 0<W_z\leq V \),
\( 0<W_\ell\leq VT \).
Thus every intermediate numerator and denominator has \( O(L+\log(T+1)) \) bits. Integer multiplication, exact division, addition, and reduction by greatest common divisors all take polynomial time. A conservative bound using elementary arithmetic is \( O(\tau(L+\log(T+1))^3) \).
Represent terminal recommendations canonically and group equal states. Even direct pairwise grouping costs only \( O(\tau^2LN) \) bit operations. At most \( \tau \) groups are nonempty, and positivity guarantees that precisely those groups have nonzero mass. This avoids enumerating the potentially much larger universe of possible terminal rankings.
Therefore every individual terminal state, every nonzero terminal-state mass, and the exact average move count are computable in polynomial time. Under standard polynomial-time reductions that produce promised instances, \( \mathrm{NP} \)-hardness would consequently imply \( \mathrm{P}=\mathrm{NP} \).
⟨structured verdict parsed — rendered above⟩
The prover’s polynomial-time conclusion is correct under the promises in USER_TASK. The argument establishes all three requested outputs and supplies a polynomial bit-operation bound. I found no major or minor mathematical issues requiring repair.
The count \(K=m(m-1)\) correctly includes both orientations of every pair of distinct options. The count \(U=h(ma+K+b)\) correctly counts evaluation assignments, criterion-specific comparisons, and importance assignments.
When \(m=1\), both forms of recommendation contain no comparisons. At the initial Update, the noninitial failure test is inapplicable and the success condition holds. Thus each dialogue has exactly one terminal move, as claimed.
Initially, \(B_t\subseteq P_t\). Subsequent additions to \(B\) are preference-information atoms drawn from maker commitments, and the task promises that all information supplied by the maker belongs to \(P_t\). Consequently, the invariant \(B\subseteq P_t\) is valid.
The compatibility promise therefore applies to every base for which model selection is required. In particular, the family \(\mathcal C(B)\) is nonempty. Consistency of \(P_t\) also ensures consistency of its subsets under the stated definition; the simulator nevertheless correctly retains the protocol’s inconsistency test.
The closure argument uses exactly the necessary hypotheses:
Thus the compatible family contains a model whose property set is contained in every other compatible property set. This establishes a *least* compatible property set, rather than merely a minimal one.
Selecting a compatible model of minimum property-set cardinality is consequently correct: every other compatible property set contains the least one, and any distinct such set has strictly greater cardinality. The scan does not require enumerating property subsets.
The bound \(O(r(U+q+1))\) is valid with coordinatewise bit-vector scans. The one-property deletion hypothesis is unused, but unnecessary hypotheses do not invalidate the argument.
The inequality
\(p_t\leq h\left(m+\binom m2+1\right)\)
follows from the specified consistency conditions. For each criterion there are at most \(m\) evaluation assignments, one importance assignment, and one comparison per unordered option pair. Opposite orientations would form a directed cycle.
The prover explicitly treats
\(T_t=7p_t+2K+1\)
as the established premise supplied by USER_TASK. That use is legitimate and requires no independent termination proof.
The numerical expression also matches Proposition 1 of the [cited paper](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p959.pdf), where the proposition is stated under its update axiom UN. The proof here relies on the task’s supplied bound, so it does not require an additional transfer of that theorem to the present formulation.
The listed operations suffice to simulate the specified protocol:
There is no unresolved search problem hidden in explanation selection: the task expressly supplies polynomial-time policies and promises their legality.
The state includes the required snapshot \(E^-\), prior recommendation, and move counter. Counting utterances, including the terminal utterance, while excluding Update matches the task.
The proof does not infer polynomial time from termination alone. It separately checks the lengths of inputs supplied to policies and evaluators.
Utterances consist of finite atom sets and fixed locution labels. Their atom identifiers have polynomial encoding length, and their set sizes are bounded by \(U+K\). With at most \(T_t\) utterances, the history therefore has polynomial length. Commitment stores and other maintained finite sets have the same property.
Consequently, the promised fixed polynomial evaluation bound applies to polynomial-length descriptions and histories. A constant number of calls per utterance or Update yields \(O(T_t+1)\) calls overall. This establishes polynomial-time simulation without overlooking history growth.
The induction on transitions is adequate. Initialization is prescribed, Update uses the specified tests and additions, the selected model is exactly \(\pi[B]\), and deterministic policies specify the subsequent legal utterances and revisions.
Hence the simulator computes the actual terminal state \(z_t\) and actual move count \(\ell_t\), rather than a reachable state or a bound on the count. Running it independently on the explicitly supplied support addresses every requested type.
The proposed bound accounts for preprocessing, all simulations, state grouping, and exact arithmetic. Its use of a fixed exponent \(d\) is consistent with the uniform polynomial-time promise; that promise does not specify a numerical exponent.
The consistency estimate is valid. For \(m=1\), \(h(m+K)=h\). For \(m\geq2\), \(m\leq K\), so the displayed domination by \(2U+h\) holds as well.
Under the explicit finite-set input representation, the cardinalities used in \(N\) are bounded by the input length. Accordingly, \(U=O(L^3)\), \(N=O(L^3)\), and \(T=O(L^2)\) are valid conservative bounds. Substituting them into the displayed running time gives a polynomial in \(L\), with dependencies on all requested parameters stated.
The common denominator \(V=\prod_t v_t\) has \(O(L)\) bits because the denominator bit lengths are included in the input length. Each division \(V/v_t\) is exact.
The integer weights satisfy \(w_t/V=\mu_t\), and normalization gives \(\sum_t w_t=V\). Therefore the expressions for \(M_z\) and \(\bar\ell\) are exact.
Positivity and \(1\leq\ell_t\leq T\) justify the numerator bounds. Intermediate partial sums remain within those bounds, so arithmetic operands have \(O(L+\log(T+1))\) bits. The stated elementary-arithmetic bound is conservative and polynomial.
Canonical grouping of terminal states is sufficient, including a single common failure state and success states distinguished by their recommendations. There are at most \(\tau\) encountered states. Positive masses ensure that precisely the encountered groups have nonzero mass; no enumeration of all possible rankings is necessary.
The conclusion is therefore established for the promised input class. The final observation about NP-hardness is appropriately conditional on \(\mathrm{P}=\mathrm{NP}\). No additional clarification or repair is needed.
⟨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.