Quantified Constraints and Generalisations

点击翻译按钮获取中文摘要

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.