paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Promises Make Finite (Constraint Satisfaction) Problems Infinitary

承诺使有限（约束满足）问题无穷化
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 1/10 · 论文研究 Promise CSP 的复杂性理论归约，属于纯理论计算机科学（逻辑与约束编程），与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析等方向没有直接联系。虽然涉及约束满足，但未触及程序分析或形式化验证的实际应用。引用 4 inbox
Libor Barto
逻辑与自动机逻辑与约束编程
crossref: 2026-09-12

AI 速览

一句话：证明 (1-in-3-SAT, Not-All-Equal-3-SAT) 不能自然归约到可解有限域 CSP，除非 P=NP。

承诺约束满足问题（PCSP）是固定模板 CSP 的重要推广，涵盖可满足性与图着色等问题的近似变体。目前已知所有有限模板上多项式可解的 PCSP 都能以某种自然方式归约到可解的 CSP，但这些 CSP 往往定义在无穷域上。本文研究这种无穷性是否必要。作者聚焦一个具体的有限域 PCSP，即 (1-in-3-SAT, Not-All-Equal-3-SAT)，通过复杂性理论论证与归约分析，证明除非 P=NP，否则该 PCSP 不能自然归约到任何可解的有限域 CSP。这一结果说明，对有限域 PCSP 而言，归约目标出现无穷域并非技术偶然，而是本质需要；它为 PCSP 的代数/复杂性分类划定了边界。

问题
研究有限模板 PCSP 到可解 CSP 的自然归约是否必然引入无穷域，即无穷域在已知可解 PCSP 的归约中是否不可避免。
方法
以具体的有限域 PCSP (1-in-3-SAT, Not-All-Equal-3-SAT) 为对象，分析其到可解有限域 CSP 的自然归约，并结合复杂性假设进行论证。
评估
证明若该 PCSP 能自然归约到可解有限域 CSP，则会推出 P=NP；因此除非 P=NP，这种归约不存在。
原文摘要（Abstract）

The fixed template Promise Constraint Satisfaction Problem (PCSP) is a recently proposed significant generalization of the fixed template CSP, which includes approximation variants of satisfiability and graph coloring problems. All the currently known tractable (i.e., solvable in polynomial time) PCSPs over finite templates can be reduced, in a certain natural way, to tractable CSPs. However, such CSPs are often over infinite domains. We show that the infinity is in fact necessary by proving that a specific finite-domain PCSP, namely (1-in-3-SAT, Not-All-Equal-3-SAT), cannot be naturally reduced to a tractable finite-domain CSP, unless P=NP.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4976,
  title = {Promises Make Finite (Constraint Satisfaction) Problems Infinitary},
  author = {Libor Barto},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785671}
}