Îçҹ̽»¨

Project SAT-Solving

Voraussetzungen

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

Ziele

  • Erweiterungen und Verbesserungen für unseren SAT-Solver hybridGM
  • Experimenteller Vergleich der eigenen Implementierung mit bestehenden Solvern auf einem der TOP500 Supercomputer ()
  • kurze Dokumentation der Herangehensweise und der Ergebnisse in einem Praktikumsbericht.

Themen

Unser Solver hybridGM ist einer der besten SAT-solver für random Probleme. Es gibt ein paar einfache Ideen wie dieser Solver noch effizienter gemacht werden kann. Jede solche Idee stellt ein Praktikumsthema dar. Diese werden dann in der Vorbesprechung vorgestellt. 

 

Interessante Links

- 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

Weiter Informationen

Termine & Raum

Vorbesprechung am

14.10 Mittwoch 14:15-16:00

Raum 531/O27