Dr. Florian Wörz

I have successfully defended my PhD thesis.

• Beweiskomplexität (vor allem Resolution; hier insbesondere Variable Space)
• Komplexitätstheorie
• SAT-Solving (hauptsächlich aus theoretischer Sicht), vor allem Querbezüge zur Beweiskomplexität
• Data Science angewandt auf SAT-Solving
• Pebbling (und die Querbezüge zu Resolution)

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

See also my dblp page.

• On the Complexity of Solving Propositional Formulas.
  Florian Wörz.
  PhD Thesis. (To appear shortly on Oparu)
   
• Cutting Planes Width and the Complexity of Graph Isomorphism Refutations.
  Jacobo Torán and Florian Wörz.
  • Accepted for Publication and Presentation at SAT 2023 in Alghero.
  • Full-length conference version in Electronic Colloquium on Computational Complexity (ECCC), TR23-063, May 2023. (Link)
     
• Toward an Understanding of Long-tailed Runtimes of SLS Algorithms.
  Jan-Hendrik Lorenz and Florian Wörz.
  • ACM Journal of Experimental Algorithmics (ACM JEA), 27:1.14:1-1.14:38, December 2022. (Link)
  • Full-length version in arXiv:2210.13159 [cs.DS]. (Link)
     
• Too Much Information: CDCL Solvers Need to Forget and Perform Restarts.
  Tom Krüger, Jan-Hendrik Lorenz, and Florian Wörz.
  • PLOS ONE, 17(8), August 2022. (doi:10.1371/journal.pone.0272967)
  • Full-length version in arXiv:2202.01030 [cs.AI]. (Link)
     
• Number of Variables for Graph Identification and the Resolution of GI Formulas.
  Jacobo Torán and Florian Wörz.
  • ACM Transactions on Computational Logic (ACM TOCL), 24(3):23:1-23:25, April 2023. (doi:10.1145/3580478)
  • In Proceedings of the 30th EACSL Annual Conference on Computer Science Logic (CSL '22), pages 36:1-36:18, February 2022. (doi:10.4230/LIPIcs.CSL.2022.36)
  • Earlier version in Electronic Colloquium on Computational Complexity (ECCC), TR21-097, Juli 2021. (Link)
     
• Evidence for Long-Tails in SLS Algorithms.
  Florian Wörz and Jan-Hendrik Lorenz.
  • In Proceedings of the 29th Annual European Symposium on Algorithms (ESA '21), pages 82:1-82:16, September 2021. (doi:10.4230/LIPIcs.ESA.2021.82)
    Winner of the "Best Student Paper Award" of ESA '21, sponsored by the European Association for Theoretical Computer Science (EATCS).
  • Full-length version in arXiv:2107.00378 [cs.DS]. (Link)
  • Supplementary Materials:
    • Supplementary Data (doi:10.5281/zenodo.4715893)
    • Statistical and Visual Evaluations (doi:10.5281/zenodo.5026180)
       
• Source Code of "concealSATgen".
  Jan-Hendrik Lorenz and Florian Wörz.
  GitHub Repository, February 2021. (Link)
   
• On the Effect of Learned Clauses on Stochastic Local Search.
  Jan-Hendrik Lorenz and Florian Wörz.
  • In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT '20), pages 89-106, Juli 2020. (doi:10.1007/978-3-030-51825-7_7)
  • Earlier version in arXiv:2005.04022 [cs.AI]. (Link)
  • Implementation and Statistical Tests of GapSAT, February 2020. (Link)
     
• Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space.
  Jacobo Torán and Florian Wörz.
  • Computational Complexity, 30(1):7, May 2021. (doi:10.1007/s00037-021-00206-1)
  • In Proceedings of the 37th Symposium on Theoretical Aspects of Computer Science (STACS '20), pages 60:1-60:18, March 2020. (doi:10.4230/LIPIcs.STACS.2020.60)
  • Full-length conference version in Electronic Colloquium on Computational Complexity (ECCC), TR19-097-R1, February 2020. (Link)
  • Earlier version in Electronic Colloquium on Computational Complexity (ECCC), TR19-097, Juli 2019.
     
• Zeit-Platz Tradeoffs im Beweissystem der Resolution.
  Florian Wörz.
  Masterthesis, Universität Ulm, July 2018. (pdf) 

• PhD Defense. Ulm, November 2023.
• Cutting Planes Width and the Complexity of Graph Isomorphism Formulas. Talk given at the "SAT" Conference. Alghero, Juli 2023. (Slides)
• On the Complexity of Solving Propositional Formulas. Talk given to present my PhD Project. Ulm, December 2022. (Slides) (Announcement)
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas. Talk given at the "Joint GI Meeting: Logic in Computer Science and Deduction Systems". Erlangen-Nürnberg, April 2022. (Slides)
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas. Talk given at the "CSL" Conference. Göttingen, February 2022. (Slides)
• Complexity Measures in Propositional Resolution. Talk given at the Institute of Artificial Intelligence. Ulm, February 2022. (Slides)
• Evidence for Long-Tails in SLS Algorithms. Talk given at the "ESA" Conference. Lisbon, September 2021. Best Student Paper Award. (Slides) (Poster) (Video)
• On the Effect of Learned Clauses on Stochastic Local Search. Talk given at the "SAT" Conference. Alghero, Juli 2020. (Slides)
• Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Talk given at the "STACS". Montpellier, März 2020. (Slides)
• Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Talk given as part of the "Komplex" series at the University of Ulm. März 2020. (Slides)
• Reversible Pebbling. Talk given at the Seminar "SAT and Interactions". Leibniz-Zentrum für Informatik auf Schloss Dagstuhl in Wadern, Februar 2020. (Slides)
• Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. Talk given at the "GI Meeting Logic in Computer Science". Jena, Oktober 2019. (Slides)

• Theory and Applications of Satisfiability Testing (SAT). Alghero, Sardinien. 2023.
• Joint Logic Workshop: Logic in Computer Science and Deduction Systems. Erlangen-Nürnberg, 2022.
• Computer Science Logic (CSL). Göttingen, 2022.
• European Symposium on Algorithms (ESA). Lisbon*, 2021.
• Satisifiability: Theory, Practice and Beyond. Simons Institue for the Theory of Computing, Berkeley*.
• Theory and Applications of Satisfiability Testing (SAT). Alghero*, Sardinien. 2020.
• Symposium on Theoretical Aspects of Computer Science (STACS). Montpellier, Frankreich, 2020.
• SAT and Interactions. Leibniz-Zentrum für Informatik, Schloss Dagstuhl, Wadern, 2020.
• 25. Jahrestagung of the "Gesellschaft für Informatik"-Fachgruppe "Logik in der Informatik". Jena, 2019.
• Workshop on Proof Complexity, Federated Logic Conference (FLoC 2018). Oxford, 2018.

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.

Als Dozent:

• SoSe 20: Lehrbeauftragter und Dozent für 'Grundlagen der Mathematik' an der Hochschule Aalen (Skript) (Vorlesungsaufzeichnungen)

Als Doktorand:

• SoSe 22: Seminarleitung und Betreuung im 'Seminar Algorithmik: Algorithmen in der Aussagenlogik'
• SoSe 22: Seminarleitung und Betreuung im 'Seminar Einführung in die Algorithmik: Algorithmen in der Aussagenlogik'
• WS 19/20: Übungsleiter für 'Formale Grundlagen'
• WS 19/20: Seminarleitung und Betreuung im 'Seminar Algorithmik: Algorithmische Zahlentheorie'
• WS 19/20: Seminarleitung und Betreuung im 'Seminar Einführung in die Algorithmik: Algorithmische Zahlentheorie'
• SoSe 19: Übungsleiter für 'Kryptologie: Algorithmen und Methoden'
• SoSe 19: Übungsleiter für 'Berechenbarkeit und Komplexität'
• WS 18/19: Seminarleitung und Betreuung im 'Proseminar: Algorithmen zum SAT-Solving'
• WS 18/19: Übungsleiter für 'Analysis IIa für Informatiker und Ingenieure'

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'