An Evaluation of Bit-Parallelization applied to Failed Literal Probing

The satisfiability problem (SAT) can be used to encode many problems of other domains since it is the first one to be proven NP-complete. Powerful SAT solvers have been developed in the last years which can handle large real-world problems in a reasonable amount of time. Today’s significant challenges on SAT solvers include the transition to parallel computer architectures. Various techniques have been developed to utilize multiple cores, but those are limited to multi-core CPU systems. This thesis evaluates another concept of parallelism than what is state-of-the-art today. An algorithm is developed that is based on a ‘streaming’ principle, like it is optimal for massively parallel systems, including modern graphics cards. To take advantage of this principle, major changes to existing algorithms are necessary, first of all to avoid branches whenever possible. This also gives the opportunity to add parallelism in the sense of bit-parallelism. As the evaluation will show, there is a good chance that the implemented algorithm will perform well on massively parallel systems. Even on regular computer systems further optimization potential is conceivable.