摘要翻译：
量化约束和量化布尔公式通常比经典约束更难推理，因为量词交替使得通常的解概念不合适。因此，约束满足问题(CSP)的基本性质，如一致性或可替换性，在量化的情况下并不完全被理解。这些性质是重要的，因为它们是大多数用于求解经典（存在量化）约束的推理方法的基础，人们希望在求解量化约束时从类似的推理方法中受益。在本文中，我们证明了求解CSP所使用的大多数性质都可以推广到量化的CSP。这需要重新思考一些基本概念；特别地，我们提出了一个结果的概念，它推广了经典的解的概念，所有的定义都建立在它的基础上。我们提出了对这些性质之间的关系的系统研究，以及关于这些性质决定的复杂性结果。最后，由于这些问题通常是难以解决的，我们推广了CSP中使用的方法，提出了基于局部性的更弱的、更容易检查的概念，允许在多项式时间内不完全地检测这些性质。
---
英文标题：
《Generalizing Consistency and other Constraint Properties to Quantified
  Constraints》
---
作者：
Lucas Bordeaux, Marco Cadoli, Toni Mancini
---
最新提交年份：
2007
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic properties of Constraint Satisfaction Problems (CSP), such as consistency or substitutability, are not completely understood in the quantified case. These properties are important because they are the basis of most of the reasoning methods used to solve classical (existentially quantified) constraints, and one would like to benefit from similar reasoning methods in the resolution of quantified constraints. In this paper, we show that most of the properties that are used by solvers for CSP can be generalized to quantified CSP. This requires a re-thinking of a number of basic concepts; in particular, we propose a notion of outcome that generalizes the classical notion of solution and on which all definitions are based. We propose a systematic study of the relations which hold between these properties, as well as complexity results regarding the decision of these properties. Finally, and since these problems are typically intractable, we generalize the approach used in CSP and propose weaker, easier to check notions based on locality, which allow to detect these properties incompletely but in polynomial time.
---
PDF链接：
https://arxiv.org/pdf/0705.3561