SAT-Solving + CSP (Projektarbeit)

Inhalt

Effiziente Algorithmen für das Sat-Problem und Constraint Satisfaction Problem gewinnen immer mehr an Bedeutung, da mit Hilfe dieser Algorithmen eine sehr breite Klasse an komplexen Problemen erfasst werden kann.

Ziel des Praktikums ist es, einen Algorithmus (auch Solver genannt ) zu implementieren, der eines der oben genannten Probleme löst. Dabei kann es sich um einen schon existierenden Algorithmus handeln oder um einen selbst entwickelten.

Der Ablauf der Arbeit gliedert sich folgendermaßen:

  1. Literaturrecherche und Einarbeiten in das Thema
  2. Auswahl eines Solvers, welcher untersucht und implementiert werden soll ODER Entwicklung eines eigenen Solvers
  3. Implementierung des Solvers
  4. Ausführliche Tests anhand von Benchmarks
  5. Verbessern des Solvers 
  6. Verfassen eines kurzen Abschlussberichts

 

Literatur

  • Holger H. Hoos & Thomas Stützle: Stochastic Local Search - Foundations and Applications. Morgan Kaufmann / Elsevier, 2004
  • U. Schöning: Algorithmik. Spektrum Akademischer Verlag, 2001.
  • http://www.satlive.org/
  • http://www.cs.ubc.ca/~hoos/SATLIB/index-ubc.html
  • http://www.satcompetition.org/

Termine

Vorbesprechung: Di 21.09 um 16:00 in 531

oder nach Vereinbarung