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 in
https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force

The 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.

The project will develop, implement, apply and analyse the Cube-and-Conquer (C&C) method, a technology for solving hard computational problems, especially suited for distributed systems with many computational units.

The problems solved are called "SAT problems", and can be considered as big logical puzzles. SAT problems are fundamental for the three main application areas:
- verification and correctness on the industrial side experienced a revolution through SAT solving over the last two decades; especially computer hardware, as based on Boolean logic, can be analysed successfully;
- also in automated theory proving (ATP), proving mathematical theorems, SAT solving is used as the underlying "logical engine" (handling the basic logical structure), and has become a fundamental technology;
- more concretely, many combinatorial problems in computer science and mathematics can be directly expressed as SAT problems and solved (this is the essence of the "NP-completeness" of SAT), where an example is the recent solution of the boolean Pythagorean Triples problem
https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem
which demonstrated the strength of C&C.

The project considers applications as an essential aspect of it. Big mathematical problems are attacked, as well as hard industrial problems, encoding verification and correctness of complicated hardware and software systems. These applications are valuable on their own, and they provide important feedback for theory, algorithms and implementations. First the theory and software is shaped by feedback only from the various mathematical applications, but then adaption mechanisms are developed specifically for industrial problems (which are larger, but intrinsically easier).

In mathematics, this technology will help to bring proof/solver technology into common mathematical practice. Delivery will use all available channels: from electronic platforms for providing source code to workshop participation to direct personal contact. So we will make sure, that besides our own application agenda we will consider as many other applications as possible --- the (general-purpose) open-source software developed will enable us to do this.

The novel algorithms (based on a new theoretic approach) will be made available as open-source software. So applicants world-wide can easily use the tool-box ("out of the box"). Furthermore the code itself can be used, which is important for research labs in industry, and this together with the documentation and underlying publications enhances the research capacity of businesses and organisations concerned with the safety and security of computer systems. The much increased performance on hard problems will boost efficiency and performance, and will enable to tackle very hard problems, which otherwise could not have been handled.

International collaboration will ensure wide applicability and dissemination. Especially we engage with specialists for mathematical and for industrial applications.

We will make a strong effort for popularisation: Besides web pages and popular accounts, we will make available games for specific applications (mathematical and industrial). These games will introduce in a playful way the combinatorial "puzzles" at the heart of the specific applications.
Overall, we aim at substantially increasing public awareness of the importance of logical methods to understand and control the ever-increasing complexity of systems.
Especially the revolution of the (intelligent) Brute-Force method, as brought by SAT technology, deserves a much wider attention.