Projekt SAT-Solving

Projekt SAT-Solving

Voraussetzungen

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

Ziele

  • Erweiterungen und Verbesserungen unseres SAT-Solvers hybridGM
  • Erweiterungen und Verbesserungen unserers SAT-Solvers Sparrow
  • Experimenteller Vergleich der eigenen Implementierung mit bestehenden Solvern auf einem der TOP500 Supercomputer (bwGrid)
  • kurze Dokumentation der Herangehensweise und der Ergebnisse in einem Praktikumsbericht.

Themen

Der SLS-solver Sparrow, der kürzlich entwickelt wurde, basiert auf sehr einfache Ideen. Die Performanz des Solvers bei 3-SAT-Problemen ist rekordverdächtig. Es gibt monentan keinen Solver, der besser abschneidet. Diese Performanz kann aber noch weiter verbessert werden. 

EDACC  ist ein System zum Verwalten von SAT-Solvern und Instanzen. Es ermöglicht das Designen von Benchmarks und auch deren Ausführung auf einem Grid oder Supercomputer. Es gibt noch viele Erweiterungen für dieses System, die sich als Praktikumsthema formulieren lassen.

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

SAT Live! - Meldungen rundum das SAT- Problem

SAT for JAVA - SAT Bibliothek für Java

SAT Library - Solver und Benchamrks rundum SAT

SAT Competition - Wettbewerbe der SAT-Solver

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

CSP Library - 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

LSF Link

Termine & Raum

Vorbesprechung am

20.04 Dienstag 16:00-18:00

Raum 531/O27

Verantwortlich

Adrian Balint

Voraussetzungen

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

Weiter Informationen

LSF Link

Ziele

  • Erweiterungen und Verbesserungen unseres SAT-Solvers hybridGM
  • Erweiterungen und Verbesserungen unserers SAT-Solvers Sparrow
  • Experimenteller Vergleich der eigenen Implementierung mit bestehenden Solvern auf einem der TOP500 Supercomputer (bwGrid)
  • kurze Dokumentation der Herangehensweise und der Ergebnisse in einem Praktikumsbericht.

Termine & Raum

Vorbesprechung am

20.04 Dienstag 16:00-18:00

Raum 531/O27

Themen

Der SLS-solver Sparrow, der kürzlich entwickelt wurde, basiert auf sehr einfache Ideen. Die Performanz des Solvers bei 3-SAT-Problemen ist rekordverdächtig. Es gibt monentan keinen Solver, der besser abschneidet. Diese Performanz kann aber noch weiter verbessert werden. 

EDACC  ist ein System zum Verwalten von SAT-Solvern und Instanzen. Es ermöglicht das Designen von Benchmarks und auch deren Ausführung auf einem Grid oder Supercomputer. Es gibt noch viele Erweiterungen für dieses System, die sich als Praktikumsthema formulieren lassen.

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

SAT Live! - Meldungen rundum das SAT- Problem

SAT for JAVA - SAT Bibliothek für Java

SAT Library - Solver und Benchamrks rundum SAT

SAT Competition - Wettbewerbe der SAT-Solver

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

CSP Library - 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.