| paper | d4-conf-ijcai-2022-0304 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
P→P discrete result → its continuous mirror
Answer: Polynomial-time solvable: in \(\mathrm{P}\), with running time \(O(L+m\tau+\tau s+q\tau^3)\) in the standard word-RAM model. · discrete side: polynomial · adjudication: proved
full proof & adversarial review →
Theorem 1
statement extracted from the paper’s text layer
Given a finite support \(T\) with rational masses \(\mu_t>0\) summing to \(1\), a formula \(\phi\), and a designated type \(t^\star\), decide whether \(t^\star\models\phi\). Each type records its propositional labels, humbled and egotistic status, friend types \(F(t)\), and strict partial preference order \(\prec_t\) over types; require \(t\in F(t)\) and the paper's compatibility, humbleness, and egotism conditions lifted to whole cohorts. Interpret \(F\phi\) over friend types and \(L\phi\) by requiring every supported type \(u\not\models\phi\) to satisfy \(u\prec_t v\) for every supported type \(v\models\phi\).
A society is partitioned into homogeneous cohorts represented by types \(t\in T\), with mass \(\mu_t\) per type. Friend and preference relations are cohort-level and satisfy the paper's network constraints. The query is model checking at one type; masses represent multiplicity, while the answer depends on the supported relational structure. The translated bound is \(O(|\phi|(\tau^3+\tau R))\), where \(\tau=|T|\) and \(R\) is the total number of supplied preference edges.
The exact cohort structure required for \(F\) is demanding, and the paper's grouped examples establish shared preferences rather than cohort-uniform friendship neighborhoods; the proponent names such a regime but gives little evidence for its prevalence.
fatal: False
The mirror covers Theorem 1's model-checking algorithm; it does not extend the axiomatization or the paper's illustrative propositions.
The strongest honest anchor is Theorem 1, proved in this paper. It says that, given a formula \(\phi\), a social network, and a designated agent, model checking takes \(O\!\left(|\phi|(|A|^3+|A|\cdot|\{\prec_a\}_{a\in A}|)\right)\) time in the worst case. Here the preference relations are supplied by compact edge sets whose transitive closures define the relations. This is a polynomial-time result for the underlying problem of deciding whether the agent satisfies the formula.
My lead mirror is Continuous Egocentric Model Checking. An instance is a finite support \(T\) of complete agent types, each with positive rational mass \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\); a formula \(\phi\); and a designated type \(t^\star\). A type records its truth values for the propositional variables, whether it is humbled or egotistic, its set \(F(t)\) of friend types, and its strict partial preference order \(\prec_t\) over types. It must satisfy the paper’s network conditions: \(t\in F(t)\); friends’ preferences are compatible; and the humbleness and egotism constraints hold. Interpret \(F\phi\) over the friend types and \(L\phi\) by the paper’s pairwise condition: every positive-mass type not satisfying \(\phi\) must be below every positive-mass type satisfying \(\phi\) in \(\prec_t\). The question is whether \(t^\star\models\phi\); the solution is a yes or no. There is no action variable or optimization objective in this mirror, because the anchor is model checking.
A fitting regime is a large, role-structured online or professional community whose relevant relations are cohort-level. For example, millions of members may fall into a few dozen types defined by role, stance, and other properties; members of each type share their preferences over cohorts and the same cohort-level friend circle. Those shared features make the type a complete description for this problem, rather than a compression that hides distinctions the logic uses. This is close to the paper’s own class-based examples: its Lilliput and hiring scenarios assign common preference structures to groups of agents.
The continuous model has an exact finite-support bridge to the paper’s semantics. Replace each positive-mass type by one representative agent, using the type’s friend set, preferences, and labels. Formula truth is constant within a type, and each clause for \(F\) and \(L\) then agrees with the original clause on representatives. Conversely, a finite network can be represented by one type per agent, with rational masses summing to one. Thus the continuous question is the same model-checking problem on the support network, and Theorem 1’s algorithm gives a bound of \(O\!\left(|\phi|(\tau^3+\tau R)\right)\), where \(\tau=|T|\) and \(R\) is the total number of supplied preference edges across types. Reading and checking the binary rational masses adds polynomial input-processing time. The expected outcome is tractable.
The main limitation is that the mass values do not affect this anchor’s truth answer: only which types have positive mass matters. The mirror therefore offers support-size compression when the number of agents is large relative to the number of complete types, but it does not make a hard discrete problem easy—the paper’s named model-checking result is already polynomial. The authors should still recognize the mirror as their problem: it preserves the semantics and asks the same satisfaction question, with agents represented by homogeneous positive-mass cohorts.
A natural further question is to compute the exact population share satisfying \(\phi\), \(\sum_{t:t\models\phi}\mu_t\). The model-checking algorithm can determine truth for every supported type, after which this share is a rational sum. That would use the population distribution in a way the designated-agent query does not.
The only strong computational anchor is Theorem 1, and it is real: model checking a formula at a designated agent is a named polynomial-time result. I would not dismiss it as merely an axiomatic paper.
The proponent’s exact quotient works when agents form homogeneous blocks: every member of a block has the same preference order and friend set. But that condition is demanding here. Since each agent must be their own friend, two agents with identical friend sets must be friends with each other; any friendship between blocks must also include the whole block. So the proposed cohort model is a block graph of exact twins, not simply a large population sharing preferences. Such networks can be imagined, but the paper’s examples establish shared preference structures, not shared friendship neighborhoods. Most arbitrary networks will have support close to the number of agents.
More fundamentally, the mirror’s designated-agent answer does not depend on the masses. The clauses for \(F\) and \(L\) use universal or existential membership and pairwise comparisons, not population weights. Thus, for fixed support and relational structure, changing \(\mu\) without changing its support cannot change whether \(t^\star\models\phi\). In the homogeneous regime, this is model checking on the quotient network: a legitimate high-multiplicity compression, but no computation about the continuous population distribution.
The stronger proposed variant—reporting the fraction of society satisfying \(\phi\)—does use the masses, but it changes the output of the problem. The paper asks whether a particular agent satisfies a formula. The fraction can be obtained by model checking each supported type and summing its mass. That may be a useful population statistic, but it is a separate aggregate query, not a continuous version of Theorem 1’s result.
There is also a scope gap for ChoCo: agents here order other agents in individual partial orders; they do not submit preferences over a common set of alternatives to a collective choice rule. The paper studies logical properties of relational networks, with no winner, allocation, or collective outcome. A weighted network-logic project could be worthwhile in its own right, but the paper supplies no computational social-choice problem for ChoCo’s population-distribution machinery to take up.
So the negative case is strongest as a claim about fit and contribution, not impossibility. Exact-twin networks give a coherent finite-support mirror, and the authors might recognize it. If support compression alone counts as worthwhile for the programme, this anchor survives. My case is that the masses are semantically inert for the paper’s actual computational result, while making them matter requires adding a different population-level query.
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.