d4-conf-aaai-2006-0090

· ? (d4-conf-aaai-2006-0090)

mirror foundnew result: NP-hard → NP-hard — proved & adversarially reviewed →
paperd4-conf-aaai-2006-0090
authors—
venue?
filed underunclassified
judged bygpt-6-luna / xhigh (triple__luna__xhigh__c6r1)
judge confidencemedium
authors would recognise ityes

The new result

NP-hard→NP-hard discrete result → its continuous mirror

Answer: \(\mathrm{NP}\text{-hard}\) · discrete side: hardness · adjudication: proved

full proof & adversarial review →

The anchor — hardness

Theorem 6

PDF text-layer excerpt — equations and symbol order may be approximateLet B be a bargaining game and ϕ a formula. Deciding whether A(B) ⊢ϕ is ΠP 2 -hard.

statement extracted from the paper’s text layer

Every anchor argued

The continuous mirror question

Given a finite support of bargaining-game types \(B_t\), binary-rational masses \(\mu_t\) summing to \(1\), a common formula \(\varphi\), and a threshold \(q\), compute or decide whether \(\sum_{t:A(B_t)\vdash\varphi}\mu_t\ge q\).

The model it lives in

Each type \(B_t\) is a complete bilateral bargaining profile, including both demand sets and entrenchment orderings; its mass is the fraction of recurring negotiations with that profile. For each type, let \(y_t=1\) exactly when the paper's agreement \(A(B_t)\) entails the common clause \(\varphi\). The output is the weighted prevalence \(\sum_t\mu_t y_t\); each local agreement remains indivisible.

What the mirror covers

The mirror covers agreement-entailment inference from Theorem 6 across recurring negotiation profiles. It leaves the deal and core decision results, the bargaining-solution computation as a whole, and the equilibrium results outside its scope.

Open questions for a prover

The case FOR (proponent)

The strongest case is a population of parallel, independent bilateral negotiations, not a single negotiation with infinitely many parties. Imagine a procurement platform running a very large number \(N\) of contract negotiations at once. On each side, many participants share the same complete logical demand base and entrenchment ordering; standardized contracts and recurring priorities keep the number \(\tau\) of distinct profiles small compared with \(N\). Each local negotiation still has exactly the two parties and the belief-revision procedure in the paper.

Formally, let \(u=(X_1,\preceq_1)\) and \(v=(X_2,\preceq_2)\) be the two parties’ types. A rational matching measure \(\pi(u,v)\) describes the fraction of negotiations between each pair of types, with total mass \(1\); its marginals describe the two role populations. Each supported pair, together with the query being tested, is a complete type for the computation. Mass is the fraction of negotiation participants in that profile. The output is a population statistic: for a predicate \(Q\) on a local negotiation, compute
\[ p_Q=\sum_{(u,v)}\pi(u,v)\,\mathbf{1}[Q(u,v)]. \]
Equivalently, given a threshold \(q\), decide whether \(p_Q\ge q\). The decision variable is the local yes/no indicator, and the objective is the mass of cases for which it is true. No deal is fractional: the continuous object is the population across many separate negotiations, not the agreement inside any one negotiation. This is a high-volume regime with many agents and few recurring complete types.

My lead anchor is Theorem 4, proved in this paper. It says that given a bargaining game \(B=(X_1,X_2)\) and proposed deal sets \(D_1\subseteq X_1\), \(D_2\subseteq X_2\), deciding whether \((D_1,D_2)\) is a deal is DP-complete. In the paper’s hierarchy notation, this means that for each party \(i\) and each level \(k\), \(D_i\cap X_i^k\) is inclusion-maximal among subsets of \(X_i^k\) for which the other party’s demands, together with that party’s retained demands through level \(k\), remain consistent. The continuous mirror is Deal-Validity Prevalence: each supported pair type includes \(B\) and its proposed \((D_1,D_2)\); compute the fraction of the negotiation population in which the proposal is a deal, or test whether that fraction reaches \(q\). This is the strongest anchor because the local predicate is exactly the paper’s deal-membership problem. A one-type society with mass \(1\) recovers it, so hardness transfers (Class B); the weighted aggregation may add complexity, but cannot remove that lower bound.

Theorem 5, also proved here, anchors a distinct query on the same society. It says that given \(B\) and a pair of formula sets \(\Phi=(\Phi_1,\Phi_2)\), deciding whether \(\Phi\) is the core is NP-hard and coNP-hard. The core is defined from the deals: each deal \(D\) has coverage \(\rho_B(D)=\min\{\rho_{X_1}(D_1),\rho_{X_2}(D_2)\}\), where \(\rho_{X_i}(O)\) is the greatest hierarchy level fully covered by \(O\). The set \(\gamma(B)\) contains the deals with maximum coverage, and the core consists of the unions of each side’s demands over those deals. The mirror, Core-Status Prevalence, supplies a candidate \(\Phi\) for each supported pair type and computes the population mass on which it is the core. Again a single type embeds the paper’s problem, so this is Class B hardness. This anchor is useful because the core is the intermediate object the paper uses to construct its bargaining solution.

Theorem 6, proved here by a reduction that uses Nebel’s earlier result, says that given \(B\) and a formula \(\varphi\), deciding whether \(A(B)\vdash\varphi\) is \(\Pi_2^P\)-hard. Here \(A(B)=(X_1\otimes_1\Phi_2)\cap(X_2\otimes_2\Phi_1)\), with \((\Phi_1,\Phi_2)\) the core. Its mirror, Agreement-Entailment Prevalence, puts a formula query with each supported profile and computes the mass of local agreements that entail it. One profile of mass \(1\) recovers the paper’s inference problem, again giving Class B hardness. The paper’s proof makes the population-independent source of this hardness particularly clear: it reduces from Nebel’s belief-revision inference problem in a restricted bargaining case.

These mirrors cover the paper’s computational decision questions: testing deals, testing the core, and testing consequences of the agreement. They do not claim a continuous analogue of the paper’s equilibrium results or a way to compute every agreement efficiently. I would expect the authors to recognize each local predicate as their problem. They might regard its population-weighted prevalence as a useful deployment-scale question rather than a new bargaining model; that is the limit of the case.

The weakest point is that the continuous computation is separable by negotiation type. Once each supported type has been evaluated, the prevalence is just a weighted sum. Continuization does not expose these logical predicates to an obvious LP or other continuous-optimization method, and the hardness survives even when \(\tau=1\). So this is an honest population mirror with practical meaning in a repeated, standardized-negotiation regime, but it does not suggest that making the population continuous will dissolve the paper’s hardness.

The case AGAINST (opponent, writing after the proponent)

The strongest objection is that these results concern a single bilateral game, while the proposed continuous problems distribute mass over many games. That can be a sensible deployment scenario, but it makes the population a distribution of computational cases, not a society whose collective outcome is determined by its type masses. The measure weights independent local answers; it does not enter the bargaining procedure or create a shared decision.

For Theorem 4, deal validity is a predicate on one game and one proposed pair of deal sets. A population metric could count how often submitted proposals are valid. But to get varied answers, its support must distinguish the games and proposals being audited: the “types” then encode computational instances. A stronger operational version could apply a common proposal policy across recurring negotiation profiles and measure its validity rate. That is a legitimate audit, but it asks whether a policy works across a workload; it does not make deal validity a population-level bargaining problem. The support-one construction recovers Theorem 4, but shows only that the wrapper admits a one-case input.

Theorem 5 has the same limitation. Core status is a property of a candidate pair \(\Phi\) for one game. Aggregating whether supplied candidates are correct is again an audit of cases. A common prediction policy over recurring profiles would make the audit more coherent, but its output is still a weighted accuracy statistic. The masses do not affect any game’s core.

Theorem 6 gives the best version of the case: take a large procurement platform with recurring demand profiles and ask what fraction of agreements entail one shared clause \(\varphi\). This avoids putting a different query into every type, and the scenario is plausible. Still, each local agreement is determined by its own bilateral game. The population statistic reports how often the clause follows; it neither computes a common agreement nor guides a population-level intervention. If one adds a shared budget or a policy that changes bargaining behavior to raise the fraction, that may yield a new continuous optimization problem. But the added coupling and action costs would be the substance of that problem; they are absent from the results being mirrored.

The case against is therefore about the object, not about surviving hardness, altered answers, or literal formalism. Repeated standardized negotiations can make high multiplicity sensible, and a platform may find these prevalence metrics useful. But they are distributional audits of many independent negotiations, rather than continuizations of the paper’s bargaining computation. I would not claim the universal negative is airtight: the common-clause prevalence question is a credible application. I would claim only that it is a weak fit for ChoCo’s central aim of making the population itself the continuous computational object.

The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.