SAT in Master Class Recent Advances in Optimisation Paradigms and Solving Technology
Sprache des Vortragstitels:
17th Intl. Conf. on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR'20)
Sprache des Tagungstitel:
Tools for automating decision-making, commonly referred to as solvers, have seen tremendous improvement over the past decades. Nevertheless, as the problems of today are becoming increasingly complex, the limits of solving technology is constantly being challenged, warranting further advancement of the state-of-the-art. The master class gathers the leading experts to present and discuss the latest techniques incorporated in modern solving technology and to explain their remarkable efficiency in solving large and complex problems. A series of talks is planned, each addressing a particular decision/optimisation paradigm. This tutorial covers algorithmic aspects of conflict-driven clause learning and important extensions developed in recent years, including decision heuristics, restart schemes, various pre- and inprocessing techniques as well as proof generation and checking. Programmatic incremental usage of SAT solvers is discussed next. The talk closes with an overview on the state-of-the-art in parallel SAT solving and open challenges in general.
Sprache der Kurzfassung:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung