Complexity measures for solving propositional formulas.
Final Report Abstract
The satisfiability problem for propositional logic, SAT, is the best-known NP-complete problem and has traditionally been considered very hard to solve. In the last decades, however, there has been an impressive advance in the development of programs that solve SAT instances. Today, these programs solve real-world applications with literally hundreds of thousands of variables. Proof complexity provides the tools necessary to analyze SAT solvers from a theoretical perspective. The goal of the project was to obtain a better understanding of this gap between theory and practice by focusing on how several complexity measures for the proof systems at the root of modern SAT solvers (mainly Resolution) translate into estimations for running times and search strategies for the SAT programs. We have considered several central families of contradictory formulas, mainly pebbling and graph isomorphism formulas, and analyzed different complexity parameters for these formulas for their refutation in some well-known proof systems: Resolution, Cutting Planes, and algebraic proof systems. We found that combinatorial measures on the underlying graphs described in the formulas directly translate into complexity parameters of the refutations in the different systems. This allows to obtain an estimation of the complexity of the refutations directly from the graphs, without going into the concrete refutations. We have also analyzed several relationships and trade-offs between the different complexity measures and gained a better understanding of the formulas for which SAT solvers perform well. On a more practical side, we have also investigated stochastic local search solvers (SLS) and analyzed their performance using space measures for Resolution. For this, we have implemented an SLS solver and several software tools that allowed experimental performance results.
Publications
-
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
