SNIC
SUPR
SNIC SUPR
Analyzing and Improving State-of-the-Art SAT Solvers
Dnr:

SNIC 2017/12-44

Type:

SNAC Large

Principal Investigator:

Jakob Nordström

Affiliation:

Kungliga Tekniska högskolan

Start Date:

2018-01-01

End Date:

2019-01-01

Primary Classification:

10201: Computer Sciences

Allocation

Abstract

The purpose of this project is to design efficient algorithms for proving logic formulas. This problem is widely believe to be theoretically intractable in the worst case, although proving this is a major challenge in modern mathematics (one of the famous Millennium Prize Problems). On the applied side, however, dramatic developments in the last two decades have led to so-called SAT solvers that perform very well in many special cases, and these solvers are routinely used today in a wide range of application areas (such as hardware and software verification, artificial intelligence, cryptography, bioinformatics, and operations research, just to name a few examples). A surprising aspect of this development is that the best current SAT solvers are still based on the resolution method from the early 1960s, which can often handle huge formulas but may also get hopelessly stuck on tiny ones. The fundamental question of when and why SAT solvers perform well or badly remains poorly understood. Another intriguing fact is that although today other, much stronger methods than resolution are known---in particular, methods based on algebra and geometry---attempts to harness the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. Our goal in this project is twofold. Firstly, we want to perform extensive experiments on state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Our aim is to use carefully chosen benchmarks to obtain a more rigorous understanding of how different heuristics affect performance. Our belief is that if we can obtain such a principled understanding, this will also enable us to search more systematically for ways to further improve CDCL solvers. Secondly, we want to go beyond resolution and build solvers on stronger methods of reasoning. More specifically, our focus is on so-called pseudo-Boolean solvers that essentially implement a special case of integer linear programming over the Boolean hypercube. Such solvers exist, but are quite far from being competitive with CDCL solvers. Of particular interest here is to understand why they perform so poorly in some cases where the underlying methods of reasoning can be proven to be exponentially more efficient than resolution, a phenomenon that our research group has recently uncovered. We plan to try out a number of different new ideas, inspired by mathematical research, that have not been implemented before in practice. To evaluate how well they perform, we will need to run extensive experiments and measure resources such as running time, memory usage, and other statistics. Ultimately, we are aiming to gain a better mathematical understanding of geometric methods of reasoning, and to harness this understanding to develop SAT solvers that have the potential to go significantly beyond the current state of the art. This research is part of an ERC Starting Grant and is also supported by a "Breakthrough Research Grant" and a Consolidator Grant from the Swedish Research Council (VR). Obtaining sufficient computational resources is absolutely crucial for reaching the ambitious goals set out in these grant proposals.