The Computational Complexity of Quantified Constraint Satisfaction
The Computational Complexity of Quantified Constraint Satisfaction
复制标题
量化约束满足的计算复杂性
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Hubie Chen
中科院分区：
文献类型：
--
作者：
Hubie Chen
约束满足问题(CSP)是一个用于模拟搜索问题的框架。CSP的一个实例由一组变量和一组对变量的约束组成；问题是决定是否对满足所有约束的变量进行赋值。量化约束满足问题(QCSP)是对CSP问题的推广，其中变量可以是普遍量化的，也可以是存在性量化的。CSP和QCSP的一般难解性促使人们寻找这些问题的多项式时间可处理的受限情况。
在本文中，我们研究了QCSP情形的计算复杂性，其中可能出现的约束类型是受限的。我们的主要工具之一是研究CSP复杂性的代数方法，它也可以用于研究QCSP复杂性。我们首先给出了两个新的QCSP可处理性结果；其中一个可处理性结果是通过开发具有某种形式的QCSP的健全和完整的证明系统而得到的。然后，我们引入了一个新的概念来证明QCSP可处理性结果，称为折叠性。可折叠性背后的关键思想是，对于QCSP的某些情况，确定一个实例可以简化为确定一个实例集合，所有这些实例都具有有限数量的通用量化变量，并且是通过将通用量化变量“折叠”在一起从原始实例派生出来的。折叠性为导出QCSP可处理性结果提供了统一的证明技术，我们使用该技术来给出初始可处理性结果对的替代证明，以及给出进一步的可处理性结果。
The constraint satisfaction problem (CSP) is a framework for modelling search problems. An instance of the CSP consists of a set of variables and a set of constraints on the variables; the question is to decide whether or not there is an assignment to the variables satisfying all of the constraints. The quantified constraint satisfaction problem (QCSP) is a generalization of the CSP in which variables may be both universally and existentially quantified. The general intractability of the CSP and QCSP motivates the search for restricted cases of these problems that are polynomial-time tractable.
In this dissertation, we investigate the computational complexity of cases of the QCSP where the types of constraints that may appear are restricted. One of our primary tools is the algebraic approach to studying CSP complexity, which can also be used to study QCSP complexity. We first present a pair of new QCSP tractability results; one of these tractability results is arrived at by developing a sound and complete proof system for QCSPs having a certain form. We then introduce a new concept for proving QCSP tractability results called collapsibility. The key idea behind collapsibility is that for certain cases of the QCSP, deciding an instance can be reduced to deciding an ensemble of instances, all of which have a bounded number of universally quantified variables and are derived from the original instance by “collapsing” together universally quantified variables. Collapsibility provides a uniform proof technique for deriving QCSP tractability results which we use both to give alternative proofs of the initial pair of tractability results, as well as to give further tractability results.