paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Tractable Combinations of Temporal CSPs

时间 CSP 的可处理组合
LMCS vol.Volume 18, Issue 22022匹配度 1/10 · 该论文研究时间约束满足问题(CSP)的理论计算复杂性,属于逻辑与约束编程领域,与用户关注的静态分析、LLM/Agentic程序、浮点程序分析、贝叶斯程序分析等方向无直接关联。引用 1 inbox
Manuel Bodirsky, Johannes Greiner, Jakub Rydval
crossref: 2026-09-10

AI 速览

一句话:证明两个时间结构理论的 CSP 并集要么多项式时间可解,要么 NP 完全。

论文研究两个签名不相交的时间理论 T1 与 T2 的并 T1∪T2 的约束满足问题 CSP(T1∪T2) 的计算复杂度。时间结构指所有关系均可在一阶逻辑中由 (Q;<) 定义的结构。作者证明:若 T1、T2 均为时间结构理论,则 CSP(T1∪T2) 要么在 P 中,要么是 NP 完全的。证明核心是一个纯代数结论:刻画了 Q 上包含 Aut(Q;<) 的局部闭克隆格的结构,从而排除中间复杂度。该结果为时间结构理论的组合 CSP 给出了 P 与 NP 完全之间的二分性。

问题
研究两个签名不相交的时间结构理论 T1、T2 的并 CSP(T1∪T2) 的计算复杂度分类。
方法
通过分析 Q 上包含 Aut(Q;<) 的局部闭克隆格,给出纯代数刻画,并据此判定组合 CSP 的复杂度。
评估
以数学证明表明:若 T1 和 T2 都是时间结构理论,则 CSP(T1∪T2) 属于 P 或为 NP 完全。
原文摘要(Abstract)

The constraint satisfaction problem (CSP) of a first-order theory T is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of T. We study the computational complexity of CSP$(T_1 \cup T_2)$ where $T_1$ and $T_2$ are theories with disjoint finite relational signatures. We prove that if $T_1$ and $T_2$ are the theories of temporal structures, i.e., structures where all relations have a first-order definition in $(Q;<)$, then CSP$(T_1 \cup T_2)$ is in P or NP-complete. To this end we prove a purely algebraic statement about the structure of the lattice of locally closed clones over the domain $Q$ that contain Aut$(Q;<)$.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1700,
  title = {Tractable Combinations of Temporal CSPs},
  author = {Manuel Bodirsky and Johannes Greiner and Jakub Rydval},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 2},
  year = {2022},
  doi = {10.46298/lmcs-18(2:11)2022}
}