一句话：证明在一大类 ω-范畴理论中，Nelson-Oppen 组合条件对并集 CSP 的多项式时间可解性也是必要的（除非 P=NP）。
论文研究一阶理论 T 的 CSP，即判定给定有限原子公式集 S 是否与 T 可满足。设 T1 与 T2 签名不相交且具有可数无限模型；Nelson 与 Oppen 给出条件，在 CSP(T1)、CSP(T2) 可判定或多项式时间可判定时，保证 CSP(T1∪T2) 可判定或多项式时间可判定。本文研究这些条件的必要性，证明对一大类 ω-范畴理论 T1、T2，Nelson-Oppen 条件不仅是充分条件，而且是 CSP(T1∪T2) 多项式时间可解的必要条件，除非 P=NP。该结果刻画了理论组合可处理性的边界，并连接约束满足复杂度、模型论与 SMT 理论组合。
The CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of $\mathrm{CSP}(T_1 \cup T_2)$ under the assumption that $\mathrm{CSP}(T_1)$ and $\mathrm{CSP}(T_2)$ are decidable (or polynomial-time decidable). We show that for a large class of $\omega$-categorical theories $T_1, T_2$ the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of $\mathrm{CSP}(T_1 \cup T_2)$ (unless P=NP).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BodirskyG19,
title = {The Complexity of Combinations of Qualitative Constraint Satisfaction Problems},
author = {Manuel Bodirsky and Johannes Greiner},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:21)2020}
}