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可以被证明是有效解决的。与csp的研究自然对应的是对sat求解的研究，在这种研究中，一个问题被简化为可满足性问题，并使用一些sat求解器来求解，结果被解释为解决原问题。sat求解器非常强大，可以解决许多现实世界问题的大型实例。sat求解自然扩展为qsat求解，其中量化可满足性问题扮演与可满足性问题相同的角色。强大的qsat解题工具现在开始出现。在本提案中，我们打算研究量化约束满足问题（QCSP），其中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.