Quantified Constraints and Generalisations

计算复杂性是研究计算解决问题所需的资源，这些资源通常是时间和空间(即内存)。这门学科起源于大约40年前，当时人们意识到，仅仅因为计算机在理论上可以解决问题，并不意味着它可以在实践中解决问题。NP-完备性的概念出现了，自从NP-完备性为有效计算提供了障碍，尽管仍然存在所有NP-完全问题都可能都是有效可解的可能性。这个著名的P-NP问题是数学和计算机科学中最重要的开放问题之一。计算机科学家在继续尝试和解决P-NP问题的同时，一直在寻找通过将注意力限制在某些类别的问题来绕过这个问题的方法。这类约束满足问题在NP中形成了一类非常重要的问题，来自这类问题的问题经常被证明可以使用各种启发式方法进行合理的求解。因此，对约束满足问题的研究已经产生了非常强大的工具和技术来很好地解决许多现实世界的问题。最近，对约束满足问题(CSP)进行了更多的理论分析。这一分析背后的驱动力(使用了来自可计算性、组合学、逻辑和代数的各种技术和方法)一直是Feder和Vardi的猜想，即所有(非一致的)约束满足问题要么是P完全的，要么是NP完全的(无论P是否等于NP)。关于NP的情况是非常不同的，因为如果P不等于NP，则在NP中存在不同等价类的问题的无限世界(不同于约束满足问题的世界，如果Feder和Vardi的猜想为真，则只有两个不同的等价类)。这种约束满足的理论分析具有实际的副产品，因为我们正在识别越来越多的可被证明有效地求解的CSP。CSP研究的自然对应于SAT求解的研究，即将问题归结为可满足性问题，并使用一些SAT求解器进行求解，并对结果进行解释，从而解决原始问题。SAT解算器非常强大，可以解决许多现实世界问题的大型实例。Sat求解自然扩展到QSAT求解，其中量化的可满足性问题起到与可满足性问题相同的作用。在这个方案中，我们打算研究量化约束满足问题(QCSPs)，其中QCSP是通过类似于从可满足性问题得到量化可满足性问题的方式从CSP获得的。我们希望更好地理解QCSP的结构和相关概念，特别是关于它们的计算复杂性。

Computational complexity is the study of the resources needed for the computational solution of problems, with these resources usually being time and space (that is, memory). The subject originated about 40 years ago when it was realised that just because a computer can solve a problem in theory, it does not mean to say that it can solve the problem in practice. The concept of NP-completeness arose and ever since NP-completeness has provided a barrier to efficient computation, even though there still remains the possibility that all NP-complete problems might all be efficiently solvable. This famous P versus NP question is one of the most important open problems in mathematics and computer science.Computer scientists, whilst continuing to try and resolve the P versus NP question, have looked at ways of getting round the question by restricting attention to certain classes of problems. The class of constraint satisfaction problems forms a very significant class of problems within NP, and very often problems from this class have been shown to be susceptible to reasonable solution using a variety of heuristic methods. As such, the study of constraint satisfaction problems has resulted in extremely powerful tools and techniques for the good solution of many real-world problems. Fairly recently, a more theoretical analysis of constraint satisfaction problems (CSPs) has been undertaken. The driving force behind this analysis (which uses myriad techniques and methods from computability, combinatorics, logic and algebra) has been Feder and Vardi's conjecture that all (non-uniform) constraint satisfaction problems are either in P or NP-complete (irrespective of whether P is equal to NP). The situation with regard to NP is very different for if P is not equal to NP then there is an infinite world of distinct equivalence classes of problems within NP (unlike the world of constraint satisfaction problems where if Feder and Vardi's conjecture is true then there are just 2 distinct equivalence classes). This theoretical analysis of constraint satisfaction has practical spin-offs, as we are identifying more and more classes of CSPs that can provably be solved efficiently.A natural counterpart to the study of CSPs is the study of SAT-solving, whereupon a problem is reduced to the Satisfiability Problem and solved using some SAT-solver with the results being interpreted so as to solve the original problem. SAT-solvers are extremely powerful and can solve large instances of many real-world problems. SAT-solving has naturally expanded into QSAT-solving where the Quantified Satisfiability Problem plays a role identical to that of the Satisfiability Problem. Powerful QSAT-solvers are now beginning to emerge.In this proposal, we intended to study quantified constraint satisfaction problems (QCSPs), where a QCSP is obtained from a CSP in a manner similar to how the Quantified Satisfiability Problem is obtained from the Satisfiability Problem. We hope to better understand the structure of QCSPs and related concepts, particularly with regard to their computational complexity.