Komplexitätsmaße für die Lösung von aussagenlogischen Formeln.

• Antragsteller: Professor Dr. Jacobo Torán
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2019 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 430150230

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Das Erfüllbarkeitsproblem der Aussagenlogik, SAT, ist das bekannteste NP-vollständige Problem und wurde traditionell als sehr schwer lösbar angesehen. In den letzten Jahrzehnten gab es jedoch beeindruckende Fortschritte bei der Entwicklung von Programmen zur Lösung von SAT-Instanzen (SAT-Solver). Heute lösen diese Programme reale Anwendungen mit buchstäblich Hunderttausenden von Variablen. Die Beweiskomplexität bietet die notwendigen Werkzeuge, um SAT-Solver aus einer theoretischen Perspektive zu analysieren. Ziel des Projekts war es, diese Lücke zwischen Theorie und Praxis besser zu verstehen, indem wir uns darauf konzentrierten, wie sich verschiedene Komplexitätparameter für die Beweissysteme, die modernen SAT-Solvern zugrunde liegen (hauptsächlich Resolution), in Schätzungen für Laufzeiten und Suchstrategien für die SAT-Solver umsetzen lassen. Wir haben mehrere zentrale Familien widersprüchlicher Formeln betrachtet, hauptsächlich Pebble- und Graphisomorphismusformeln, und verschiedene Komplexitätsparameter für diese Formeln analysiert, um sie in einigen wichtigen Beweissystemen zu widerlegen: Resolution, Cutting Planes und algebraische Beweissysteme. Wir haben herausgefunden, dass kombinatorische Parameter für die in den Formeln beschriebenen Graphen sich direkt in Komplexitätsparameter der Widerlegungen in den verschiedenen Systemen übersetzen lassen. Dies ermöglicht es, eine Schätzung der Komplexität der Widerlegungen direkt aus den Graphen zu erhalten, ohne auf die konkreten Widerlegungen einzugehen. Wir haben auch mehrere Beziehungen und Tradeoffs zwischen den verschiedenen Komplexitätsmasen analysiert und ein besseres Verständnis der Formeln gewonnen, für die SAT-Solver gut funktionieren. Auf einer praktischeren Seite haben wir auch Stochastic Local Search Solver (SLS) untersucht und ihre Leistung unter Verwendung von Platzkomplexitätsmaßen für Resolution analysiert. Dazu haben wir einen SLS-Löser und mehrere Softwaretools implementiert, die experimentelle Leistungsergebnisse ermöglichten.

Projektbezogene Publikationen (Auswahl)

• Cops-Robber Games and the Resolution of Tseitin Formulas. ACM Transactions on Computation Theory, 12(2), 1-22.
  Galesi, Nicola; Talebanfard, Navid & Torán, Jacobo
  
• Dataset for “On the effect of learned clauses on stochastic local search” and source code of the GapSAT solver. Zenodo, February 2020.
  Jan-Hendrik Lorenz & Florian Wörz
  
• On the Effect of Learned Clauses on Stochastic Local Search. Lecture Notes in Computer Science, 89-106. Springer International Publishing.
  Lorenz, Jan-Hendrik & Wörz, Florian
  
• Reversible pebble games and the relation between tree-like and general resolution space. In 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France, volume 154 of LIPIcs, pages 60:1–60:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020
  Jacobo Torán & Florian Wörz
  
• concealSATgen
  Jan-Hendrik Lorenz & Florian Wörz
  
• Evidence for long-tails in SLS algorithms. In 29th Annual European Symposium on Algorithms, ESA 2021, September 6-8, 2021, Lisbon, Portugal (Virtual Conference), volume 204 of LIPIcs, pages 82:1–82:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  Florian Wörz & Jan-Hendrik Lorenz
  
• Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. computational complexity, 30(1).
  Torán, Jacobo & Wörz, Florian
  
• Statistical evaluation for “Evidence for long-tails in SLS algorithms”. Zenodo, June 2021
  Florian Wörz & Jan-Hendrik Lorenz
  
• Supplementary data for “Evidence for long-tails in SLS algorithms”. Zenodo, April 2021
  Florian Wörz & Jan-Hendrik Lorenz
  
• Dataset for “Too much information: Why CDCL solvers need to forget and perform restarts”. Zenodo, January 2022
  Tom Krüger, Jan-Hendrik Lorenz & Florian Wörz
  
• Number of variables for graph differentiation and the resolution of GI formulas. In 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14- 19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 36:1–36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022
  Jacobo Torán & Florian Wörz
  
• Too much information: Why CDCL solvers need to forget learned clauses. PLOS ONE, 17(8), e0272967.
  Krüger, Tom; Lorenz, Jan-Hendrik & Wörz, Florian
  
• Toward an Understanding of Long-tailed Runtimes of SLS Algorithms. ACM Journal of Experimental Algorithmics, 27, 1-38.
  Lorenz, Jan-Hendrik & Wörz, Florian
  
• Cutting planes width and the complexity of graph isomorphism refutations. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 26:1–26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023
  Jacobo Torán & Florian Wörz
  
• Kombinatorische Spiele als Schlüssel in der Komplexitätsanalyse aussagenlogischer Formeln. In Rüdiger Reischuk, Sven Apel, Abraham Bernstein, Maike Buchin, Anna Förster, Felix C. Freiling, Jan Mendling, Gustaf Neumann, Kay Uwe Römer, Björn Scheuermann, Ingo Scholtes, Nicole Schweikardt, and Klaus Wehrle, editors, Ausgezeichnete Informatikdissertationen 2023, volume D-24 of LNI, pages 331–340. GI, 2023
  Florian Wörz
  
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas. ACM Transactions on Computational Logic, 24(3), 1-25.
  Torán, Jacobo & Wörz, Florian
  
• On the Complexity of Solving Propositional Formulas. PhD thesis, Universität Ulm, Germany, August 2023.
  Florian Wörz
  
• Cutting Planes Width and the Complexity of Graph Isomorphism Refutations. ACM Transactions on Computational Logic, 25(4), 1-25.
  Torán, Jacobo & Wörz, Florian
  
• Pebble games and algebraic proof systems. In Rastislav Královic and Anton´ın Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, August 26-30, 2024, Bratislava, Slovakia, volume 306 of LIPIcs, pages 64:1– 64:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024
  Lisa-Marie Jaser & Jacobo Torán
  
• Towards Deterministic Compilation of Binary Decision Diagrams From Feature Models. 28th ACM International Systems and Software Product Line Conference, 136-147. ACM.
  Heß, Tobias; Semmler, Sean Niklas; Sundermann, Chico; Torán, Jacobo & Thüm, Thomas