Boolean satisfiability (SAT) is a fundamental and well-studied problem in computer science. Many practical applications in industry and in other areas of computer science rely on the speed of SAT solvers and other related propositional logic solvers. When running SAT solvers, one can often observe a lot of repeated com- putations and redundancy during the solvers’ execution. Although there have been many ideas to address this redundancy and make SAT solvers more effective throughout the years, there still remains a lot of redundant work that can be easily observed and identified in state-of-the-art solvers, such as repeated propagation steps, finding cores extremely similar to one another, etc. In this thesis, we set out to identify some of this redundant work and then propose methods to eliminate it. Aside from proving our techniques work in theory, we also demonstrate their effectiveness empirically, by implementing them in multiple state-of-the-art solvers and improving their performance on a wide set of benchmarks that are standard in the field.

The first technique addresses assumption-based SAT, and more specifically the redundancy in the unit propagation process of the assumptions. Our technique was to make a simple change from the standard way of unit propagating assumptions and unit propagate them all at once. This led to a dramatic improvement in the performance of mutliple complete MaxSAT solvers.

The next main technique addresses the redundancy that occurs every time a SAT solver backtracks and continues its redescent down the search tree, where it will reconstruct most of the same assignment trail again. In order to address this, we introduced a simple technique to store the assignment trail separately and used it to re-construct the trail without doing all of the unit propagation steps that otherwise would have occurred. This improved multiple state-of-the-art SAT solvers.

Our last technique addresses the redundancy that occurs during anytime MaxSAT solving, where it turns out what incomplete MaxSAT solvers often do is find multiple MaxSAT solutions consecutively that are extremely similar to one another. By using the Large Neighbourhood Search (LNS) framework, we devel- oped an algorithm for anytime MaxSAT which sets up the MaxSAT problem as an instance of incremental MaxSAT and searches an entire neighbourhood of solutions exhaustively, while removing some redundant computations. This technique managed to improve the performance of the best performing anytime MaxSAT solvers.