M.Sc. Florian Wörz

Interessen

  • Beweiskomplexität (vor allem Resolution)
  • SAT-Solving (hauptsächlich aus theoretischer Sicht), vor allem Querbezüge zur Beweiskomplexität

Kurz CV

  • M.Sc. in Mathematik (3-faches Talanx-Stipendium)
  • Aufenthalt an der University of Helsinki
  • B.Sc. in Mathematik
  • Praktikum in Dublin

DFG-Projekt

Gefördert von der Deutsche Forschungsgemeinschaft (DFG) unter Projektnummer 430150230: Komplexitätsmaße für die Lösung von aussagenlogischen Formeln.

Das Erfüllbarkeitsproblem der Aussagenlogik, SAT, ist das am besten bekannte NP-vollständige Problem und wird als solches als ein sehr schwer zu lösendes Problem angesehen. In den letzten Jahrzehnten waren jedoch einige beeindruckende Fortschritte in der Entwicklung von Programmen zur Lösung von SAT-Instanzen zu beobachten, wodurch heutzutage reale Anwendungen mit hunterttausenden Variablen gelöst werden können. Wir haben vor, ein besseres Verständnis für diese Lücke zwischen Praxis und Theorie zu erlangen. Dabei fokussieren wir uns darauf, wie mehrere Komplexitätsmaße für die grundlegenden Beweissysteme moderner SAT-Solver (hauptsächlich Resolution) in Schätzungen bezüglich Laufzeit und Suchstrategien von SAT Programmen übersetzt werden können. Wir beabsichtigen die Zusammenhänge und trade-offs zwischen den verschiedenen Komplexitätsmaßen für Resolution zu untersuchen, als auch ein besseres Verständnis über Formeln zu erlangen, auf denen SAT-Solver gute Leistungen erziehlen. Wir haben auch vor, probabilistische local search Algorithmen für unerfüllbare Formeln zu entwickeln und die Zusammenhänge zwischen deren Analyse und der Untersuchung von Platzkomplexitätsmaßen für Resolution zu erforschen. Wir werden auch die klassische und parametrisierte Komplexität von mehreren Beweiskomplexitätsfragen untersuchen.

Lehrtätigkeiten

Als Doktorand:

Als Student:

  • SoSe 18: Repetitor für die Vorlesung 'Analysis I für Informatiker und Ingenieure'
  • SoSe 18: Tutor für die Vorlesung 'Analysis I für Informatiker und Ingenieure'
  • WS 17/18: Kolloquiumstutor für die Vorlesung 'Analysis I'
  • SoSe 17: Korrektor für die Vorlesung 'Kryptologie: Algorithmen und Methoden'
  • SoSe 16: Korrektor für die Vorlesung 'Analysis I'
  • WS 15/16: Übungsleiter für die Vorlesung 'Analysis IIa und IIb für Informatiker und Ingenieure'
  • SoSe 15: Tutor für die Vorlesung 'Gewöhnliche Differentialgleichungen'
  • SoSe 14: Korrektor für die Vorlesung 'Funktionentheorie'
  • SoSe 14: Korrektor für die Vorlesung 'Gewöhnliche Differentialgleichungen'
  • WS 13/14: Tutor für die Vorlesungen 'Analysis IIa für Informatiker und Ingenieure' sowie 'Analysis IIb für Informatiker und Ingenieure'
  • WS 13/14: Repetitor für die Vorlesung 'Analysis I für Informatiker und Ingenieure'
  • SoSe 13: Gruppentutor des 'Mathematik-Trainingscamps 2013'
  • SoSe 13: Repetitor für die Vorlesung 'Analysis I für Informatiker und Ingenieure'
  • SoSe 12: Gruppentutor des 'Mathematik-Trainingscamps 2012'

Publikationen

  • Jacobo Torán und Florian Wörz. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Electronic Colloquium on Computational Complexity (ECCC), TR19-097, Juli 2019. (pdf)
  • Florian Wörz. Zeit-Platz Tradeoffs im Beweissystem der Resolution. Masterarbeit, Universität Ulm, 2018. (pdf

Konferenzen und Workshops

Sprechzeiten

(Ich biete in der vorlesungsfreien Zeit keine Sprechstunden an.)

Sprechzeiten WiSe 2019/20:

Generell nur nach vorheriger Vereinbarung per E-Mail!

Funktion

Wissenschaftlicher Mitarbeiter

Kontakt

vorname nachname_mit_oe at uni minus ulm dot de
Raum: O27/534
Telefon: +49 (0)731 50 24104
Fax: +49 (0)731 50 1224101