Quantified Constraints and Generalisations

量化约束和概括

• 批准号: EP/G020604/1
• 负责人: Iain Stewart
• 金额: $ 31.54万
• 依托单位: Durham University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2009
• 资助国家: 英国
• 起止时间: 2009 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FG020604%2F1
• 关键词: Quantified; Constraints; 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.

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

项目成果

Mathematical Theory and Computational Practice - 5th Conference on Computability in Europe, CiE 2009, Heidelberg, Germany, July 19-24, 2009. Proceedings

数学理论与计算实践 - 第五届欧洲可计算性会议，CiE 2009，德国海德堡，2009 年 7 月 19-24 日。会议记录

• DOI: 10.1007/978-3-642-03073-4_15
• 发表时间: 2009
• 作者: Dantchev S

Programs, Proofs, Processes

程序、证明、过程

• DOI: 10.1007/978-3-642-13962-8_2
• 发表时间: 2010
• 作者: Altenkirch T

Developing a well-received pre-matriculation program: the evolution of MedFIT.

制定广受好评的预科课程：MedFIT 的演变。

• DOI: 10.1007/978-3-319-11970-0_12
• 发表时间: 2022
• 期刊: Discover education
• 作者: Allen A

Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems

Lovász-Schrijver 和 Sherali-Adams 证明系统的等级复杂度差距

• DOI: 10.1007/s00037-012-0049-1
• 发表时间: 2012
• 期刊: computational complexity
• 影响因子: 1.4
• 作者: Dantchev S

Mathematical Foundations of Computer Science 2010

计算机科学数学基础 2010

• DOI: 10.1007/978-3-642-15155-2_16
• 发表时间: 2010
• 作者: Bodirsky M