The next level of SAT solving for very hard problems

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

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.