Îçҹ̽»¨

Projekt SAT und CSP-Solving

Voraussetzungen

  • Programmierkenntnisse
  • Interesse an Algorithmen für NP-harte Probleme
  • Vordiplom / Bachelor

Themen

  1. Parallel zur Vorlesung SAT Solving können verschiedene Algorithmen die dort vorgestellt werden implementiert und mit Hilfe des EDACC Systems evaluiert werden.
  2. Innerhalb des EDACC System werden sogenannte Konfiguratoren eingebungen, die in der Lage sind für eine gegebenen Algorithmus die optimalen Parameter zu finden bezogen auf eine Menge von Zielprobleme die gelöst werden sollen. Für einen Konfiguratot steht eine API zur Verfügung die es ermöglicht schnell Algorithem zu entwicklen und zu testen. Dabei spiele parallele Algorithmen eine sehr große Rolle, da die Ausführungsebene von EDACC bis zu mehreren hunderten von CPU's gleichzeitig bereitstellen kann.

Interessante Links

- Experiment Design and Adminstration for Computer Cluster

- Meldungen rundum das SAT- Problem

- SAT Bibliothek für Java

- Solver und Benchamrks rundum SAT

- Wettbewerbe der SAT-Solver

SAT in Ulm - lokale Seite der Mitarbeiter die sich mit dem SAT-Problem beschäftigen

- Solver und Benchmarks rundum das CSP - Problem

 

Literatur

  1. Stochastic Local Search Foundations and Applications - Hoos, Holger H.; Stützle, Thomas
  2. Handbook of Satisfiability - Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T.;

Die Bücher stehen in der Abteilung zur Verfügung.

 

Verantwortlich

Adrian Balint

Termine & Raum

Vorbesprechung am

12.04 Dienstag 16:00-18:00

Raum 531/O27