Skalierbarkeit und Diversifikation von modernem SAT Solving

Inhalt

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

VortragsspracheDeutsch/Englisch

Informationen

Eine erste Einführungsveranstaltung fand am 27.10.2021 statt. Aufgrund der bisher geringen Teilnehmerzahl findet eine zweite Einführung statt. Interessierte tragen sich bitte schnellstmöglich in folgende Terminfindung ein:

https://doodle.com/poll/a9cm6f2rrzuxpbzi?utm_source=poll&utm_medium=link

Die Folien sind im obigen Infoblock verlinkt. Darin finden sich auch die Themen, die wir dieses Jahr anbieten, sowie weitere organisatorische Informationen.