M.Sc. Florian Wörz

News

Prof. Dr. Jacobo Torán and I will be hosting the 'Seminar: Algorithmik' for master students and the 'Seminar: Einführung in die Algorithmik' for bachelor students in the summer term of 2022. The theme of both seminars will be

Algorithmen in der Aussagenlogik (Algorithms in Propositional Logic).

We will specifically focusing on 'Proof Complexity' (Beweiskomplexität). In Proof Complexity, one tries to understand and analyze the computational resources required to prove or refute logical statements. More intuitively, one is interested in studying how to give short (and efficiently verifiable) proofs of the fact that a given CNF formula is unsatisfiable. The resolution calculus is one method how one can show unsatisfiability. This course will primarily focus on resolution as a proof system. Proof Complexity has not only a deep connection to the P vs. NP problem but also many exciting interrelations to the applied field of SAT Solving.

Interessen

  • 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)

Kurz CV

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

Publications

See also my dblp page.

  • Too Much Information: CDCL Solvers Need to Forget and Perform Restarts.
    Tom Krüger, Jan-Hendrik Lorenz, and Florian Wörz.
    • Accepted in PLOS ONE.
    • In arXiv:2202.01030 [cs.AI]. (Link)
       
  • (Towards an Understanding of Long-Tailed Runtimes.
    Jan-Hendrik Lorenz and Florian Wörz.
    Submitted.)
     
  • Number of Variables for Graph Identification and the Resolution of GI Formulas.
    Jacobo Torán and Florian Wörz.
    • 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)
    • Full-length 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. (Link)
    • Supplementary Materials:
  • 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

Talks given

  • 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)

Konferenzen und Workshops

  • 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.

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 Dozent:

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'

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