Stochastische Lokale Suche bei SAT-Solvern

• Antragsteller: Professor Dr. Uwe Schöning
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2011 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 206226417

In diesem Projekt wird die Algorithm Engineering Methode auf SAT-Solving angewandt, und zwar speziell auf solche SAT-Algorithmen, die auf dem Konzept der lokalen Suche beruhen. Die Ziele des Projekts gliedern sich in 3 Punkte: Zum ersten sollen effizientere SAT-Solver entwickelt und implementiert werden. Diese werden der internationalen Szene auf der SAT-Konferenz präsentiert bzw. bei dem SAT-Kontest 2013 eingereicht. Zweitens, die Lücke zwischen den bei Algorithmen-Experimenten beobachteten Laufzeiten und den theoretischen Analysen derartiger Algorithmen soll weiter geschlossen werden; und dies ebenso auf der praktischen wie auf der theoretischen Seite. Zum dritten, wegen des generischen Charakters des SAT-Problems als ein NP-vollständiges Problem, und ebenso, wegen des generischen Charakters der Lokale Such-Methode, sollen die erzielten Resultate es ermöglichen, auch auf andere Problemstellungen angewandt zu werden.

• DFG-Verfahren: Schwerpunktprogramme
• Teilprojekt zu: SPP 1307: Algorithm Engineering