首页    期刊浏览 2024年11月05日 星期二
登录注册

文章基本信息

  • 标题:Quantified Constraints and Containment Problems
  • 本地全文:下载
  • 作者:Barnaby Martin ; Hubie Chen ; Florent Madelaine
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2015
  • 卷号:11
  • 期号:3
  • 页码:1
  • DOI:10.2168/LMCS-11(3:9)2015
  • 出版社:Technical University of Braunschweig
  • 摘要:The quantified constraint satisfaction problem $\mathrm{QCSP}(\mathcal{A})$ is the problem to decide whether a positive Horn sentence, involving nothing more than the two quantifiers and conjunction, is true on some fixed structure $\mathcal{A}$. We study two containment problems related to the QCSP. Firstly, we give a combinatorial condition on finite structures $\mathcal{A}$ and $\mathcal{B}$ that is necessary and sufficient to render $\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$. We prove that $\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$, that is all sentences of positive Horn logic true on $\mathcal{A}$ are true on $\mathcal{B}$, iff there is a surjective homomorphism from $\mathcal{A}^{|A|^{|B|}}$ to $\mathcal{B}$. This can be seen as improving an old result of Keisler that shows the former equivalent to there being a surjective homomorphism from $\mathcal{A}^\omega$ to $\mathcal{B}$. We note that this condition is already necessary to guarantee containment of the $\Pi_2$ restriction of the QCSP, that is $\Pi_2$-$\mathrm{CSP}(\mathcal{A}) \subseteq \Pi_2$-$\mathrm{CSP}(\mathcal{B})$. The exponent's bound of ${|A|^{|B|}}$ places the decision procedure for the model containment problem in non-deterministic double-exponential time complexity. We further show the exponent's bound $|A|^{|B|}$ to be close to tight by giving a sequence of structures $\mathcal{A}$ together with a fixed $\mathcal{B}$, $|B|=2$, such that there is a surjective homomorphism from $\mathcal{A}^r$ to $\mathcal{B}$ only when $r \geq |A|$. Secondly, we prove that the entailment problem for positive Horn fragment of first-order logic is decidable. That is, given two sentences $\varphi$ and $\psi$ of positive Horn, we give an algorithm that determines whether $\varphi \rightarrow \psi$ is true in all structures (models). Our result is in some sense tight, since we show that the entailment problem for positive first-order logic (i.e. positive Horn plus disjunction) is undecidable. In the final part of the paper we ponder a notion of Q-core that is some canonical representative among the class of templates that engender the same QCSP. Although the Q-core is not as well-behaved as its better known cousin the core, we demonstrate that it is still a useful notion in the realm of QCSP complexity classifications.
  • 其他关键词:Quantified Constraints, Finite Model Theory
国家哲学社会科学文献中心版权所有