将一致性和其他约束属性推广到量化约束
Generalizing Consistency and other Constraint Properties to Quantified Constraints
摘要：
量化约束和量化布尔公式通常比经典约束更难推理，因为量词交替使得通常的解概念不合适。因此，约束满足问题（CSP）的基本属性，如一致性或可替代性，在量化的情况下，不完全理解。这些属性很重要，因为它们是大多数用于解决经典（存在量化）约束的推理方法的基础，并且人们希望在量化约束的解决中受益于类似的推理方法。在本文中，我们表明，大多数的CSP求解器使用的属性可以推广到量化CSP。这需要重新思考一些基本概念，特别是，我们提出了一个概念的结果，概括了经典的解决方案的概念，所有的定义都是基于。我们提出了一个系统的研究这些属性之间的关系，以及复杂性的结果，这些属性的决定。最后，由于这些问题通常是棘手的，我们推广了CSP中使用的方法，并提出了较弱的，更容易检查的概念的基础上的局部性，允许检测这些属性不完全，但在多项式时间。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
