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
  • Pebbling (und die Querbezüge zu Resolution)

Kurz CV

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

Publikationen

  • Jan-Hendrik Lorenz and Florian Wörz. On the Effect of Learned Clauses on Stochastic Local Search. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020), pages 89-106, Juli 2020. (Link)
    Earlier Version in arXiv:2005.04022 [cs.AI]. (pdf)
  • Jan-Hendrik Lorenz and Florian Wörz. Implementation and Statistical Tests of GapSAT. (Link)
  • Jacobo Torán and Florian Wörz. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. In Proceedings of the 37th Symposium on Theoretical Aspects of Computer Science (STACS '20), pages 60:1-60:18, March 2020. (Link)
    Earlier Version in 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

Talks given

  • On the Effect of Learned Clauses on Stochastic Local Search. Vortrag auf der "SAT", Juli 2020. (slides)
  • Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Vortrag auf der "STACS", März 2020.
  • Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Vortrag in der "Komplex-Serie" an der Universität Ulm, März 2020.
  • Reversible Pebbling. Vortrag auf dem Schloss Dagstuhl Seminar "SAT and Interactions", Februar 2020. (pdf)
  • Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Vortrag auf der 25. Jahrestagung der GI-Fachgruppe "Logik in der Informatik" in Jena, Oktober 2019. (pdf)

Konferenzen und Workshops

DFG-Projekt

Gefördert von der Deutschen 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 erzielen. 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'

Sprechzeiten

Generell nur nach vorheriger Vereinbarung per E-Mail!

Funktion

Wissenschaftlicher Mitarbeiter

Kontakt

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