The seminar is a journey through advanced methods of parallelization and diversification in modern solvers for the propositional Satisfiability problem (SAT). Starting at the wells of "ManySAT", we travel the roads of "Painless" to the origins of "HordeSat". We will understand the essence of "Cube-and-Conquer" and its most prominent application [1]. Finally, in the valley of statistical significance, we will learn about the power of "SATzilla" and admire the beauty of "SNNAP".

With selected high-influence papers from the field of SAT solving, we take a close look at how parallel SAT solvers evolved over the last decades and learn about the major cornerstones of modern and efficient large scale SAT solving systems.

[1] https://www.spiegel.de/wissenschaft/mensch/der-laengste-mathe-beweis-der-welt-umfasst-200-terabyte-a-1094920.html