权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

The next level of SAT solving for very hard problems

SAT 的新水平解决非常困难的问题

基本信息

批准号：
EP/S015523/1
负责人：
Oliver Kullmann
金额：
$ 107.02万
依托单位：
Swansea University
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2018
资助国家：
英国
起止时间：
2018 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FS015523%2F1
关键词：
next level SAT solving very

项目摘要

We witness a twofold explosion of logical complexity in society and mathematical sciences. In society the computer systems become more complex and more pervasive, and to prove or verify their correctness is urgently needed for safety and security. In the mathematical sciences the use of computer-assisted methods promises to strengthen their outreach, beyond the capacities of paper-based proofs. To tackle these complexities, there is thus a strong need for powerful algorithmic logical reasoning.An essential property here is that this reasoning is complete: even the tiniest weakness in a microprocessor design can lead to catastrophic errors, over the lifetime of a train system any "subtle" error in its design can lead to collisions and loss of life, and likewise a mathematical proof must hold forever and under all circumstances.SAT solving, the algorithmic solution of systems of logical (boolean) equations, has become a game changer here over the last two decades, providing a powerful logical engine for the needs of correctness and verification in industry, and for the needs of Automated Theorem Proving (ATP) in mathematics. The basic method is an intelligent form of Brute Force, and the rise of SAT can be understood as based on the emerging science of brute force, as explained inhttps://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-forceThe older approach for SAT solving is the systematic backtracking approach, enhanced by look-ahead (LA), splitting up of the problem into subproblems by using global statistics gathered from forecasts (the look-aheads). The newer method, mainly responsible for the "SAT revolution", is more chaotic, and follows local statistics to reach a dead-end as soon as possible and learn from it (CDCL -- conflict-driven clause-learning).The method discovered by the applicant, "Cube-and-Conquer" (C&C), can be understood as a reconciliation of the old and the new method: In the first phase the cube-solver, based on LA, plans for splitting the big original problems into (very) many smaller problems, ready to be solved by the conquer-solver, based on CDCL. In this way the strengths of both methods are leveraged: LA uses its global overview to initially split the problem, while CDCL can concentrate on its local solution capabilities. Due to the cube-phase excellent distributed performance for a large number of processors is guaranteed. A strong international success for C&C was the solution of the Boolean Pythagorean Triples Problem (BPTP) in 2016, as explained in the linked article above.This project is about researching, implementing and applying C&C, as summarised by the formula TIA+R+P: Theory, Implementation, Application, + Reflection + Popularisation. The Theory part aims at understanding the "good splitting" of the problem, in the context of this two-phase approach. The Implementation part will provide an open-source ready-to-use software for handling hard problems in (combinatorial) mathematics and correctness/verification. The Application part on the one hand will attack problems like BPTP and bigger, and on the other hand will systematically adapt the methods to industrial contexts. Reflection means two things: on the one hand we reflect on the theory, algorithms and implements developed, learning from the applications. On the other hand we reflect on the applications, especially the mathematical ones, considering them under the algorithmic lense, discovering structures by learning from the algorithms behaviour. Last but not least, Popularisation will be undertaken systematically, to tell about the SAT revolution, the developments in algorithmic logic, and the applications in industry and mathematics.

我们目睹了社会和数学科学中逻辑复杂性的双重爆炸。社会上计算机系统变得越来越复杂和普遍，为了安全和保障迫切需要证明或验证其正确性。在数学科学中，计算机辅助方法的使用有望加强其范围，超出纸质证明的能力。为了解决这些复杂性，强烈需要强大的算法逻辑推理。这里的一个基本属性是这种推理是完整的：即使是微处理器设计中最微小的弱点也可能导致灾难性错误，在火车系统的生命周期中，其设计中的任何“微妙”错误都可能导致碰撞和生命损失，同样，数学证明必须在所有情况下永远有效。逻辑（布尔）方程组的算法解决方案在过去二十年中已成为游戏规则的改变者，为满足工业中的正确性和验证需求以及数学中的自动定理证明（ATP）需求提供了强大的逻辑引擎。基本方法是暴力破解的智能形式，SAT 的兴起可以理解为基于新兴的暴力破解科学，如 https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force 中所述。 SAT 解决的旧方法是系统回溯方法，通过前瞻 (LA) 增强，将问题分解为通过使用从预测（前瞻）中收集的全局统计数据来解决子问题。主要负责“SAT革命”的较新方法，更加混乱，遵循局部统计尽快走进死胡同并从中学习（CDCL——冲突驱动子句学习）。申请人发现的方法“立方体与征服”（C&C），可以理解为新旧方法的和解：在第一阶段，立方体求解器基于LA，计划分裂大原始方法将问题分解为（非常）许多较小的问题，准备由基于 CDCL 的征服求解器来解决。这样就充分利用了两种方法的优势：LA利用其全局概览来初步拆分问题，而CDCL则可以专注于其本地解决能力。由于立方体相位，可以保证大量处理器的出色分布式性能。 C&C 在国际上取得的巨大成功是 2016 年布尔毕达哥拉斯三元组问题 (BPTP) 的解决方案，如上面链接文章中所述。该项目是关于研究、实施和应用 C&C，如 TIA+R+P 公式所概括：理论、实施、应用、+反思 + 普及。理论部分旨在理解问题的“良好分裂”，在这种两阶段方法的背景下。实现部分将提供一个开源的即用型软件，用于处理（组合）数学和正确性/验证中的难题。应用部分一方面将解决 BPTP 等问题，另一方面将系统地使这些方法适应工业环境。反思意味着两件事：一方面我们反思所开发的理论、算法和实现，从应用中学习。另一方面，我们反思应用程序，尤其是数学应用程序，从算法的角度考虑它们，通过学习算法行为来发现结构。最后，系统地进行科普，讲述SAT革命、算法逻辑的发展以及工业和数学中的应用。