MOVES Seminar, 14 July 2009, 14:00

 

Parallelisierung in der Terminierungsanalyse

 

Andreas Kelle-Emden

 

Abstract:

 

Seit einigen Jahren ist die Parallelisierung von Algorithmen ein immer wichtiger werdendes Thema der Informatik. Unser Terminierungstool AProVE besitzt bereits viele parallele Techniken, die allerdings bisher sehr schlecht skalierten. So waren wir gezwungen, auf dem letzten Terminierungswettbewerb mehrere Instanzen von AProVE parallel zu betreiben, um die verfügbare Rechenleistung ausnutzen zu können. In diesem Vortrag werde ich einige Techniken präsentieren, durch die es AProVE nun möglich ist, von vielen Prozessorkernen zu profitieren. Dazu gehören neben dem Finden und Beheben üblicher Fehler eine Erweiterung unserer Strategiesprache sowie ein neues Interface für paralleles SAT-Solving. Mithilfe dieser Ansätze ist es uns gelungen, die Version des letzten Wettbewerbs zu übertreffen.