The next level of SAT solving for very hard problems

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

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.