Skalierbarkeit und Diversifikation von modernem SAT Solving

Bemerkungen

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

Course Details

Welcome! Here is some initial information for this year's seminar about advanced SAT solving.

  • We anticipate the course to take place online and without any in-person meetings.
  • We encourage presentations to be held in English (as that is also the language of the papers we discuss).
  • The first meeting wil take place Thursday, November 5, 2020 at 14:00 where we will discuss the assignment of topics and the further meetings. We will share the URL for the meeting here.
  • If you are interested in participating, you can just join us at the first meeting – preferably after having sent us a short mail saying that you intend to participate.