Complexity measures for solving propositional formulas.

• Applicant: Professor Dr. Jacobo Torán
• Subject Area: Theoretical Computer Science
• Term: since 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 430150230

The satisfiability problem for propositional logic, SAT, is the best known NP-complete problem and it is central to manyareas of theoretical computer science. As such it has been traditionally considered to be very hard to solve. In the last decades however, there has been an impressive advance in the development of programs solving SAT instances. Nowadays these programs solve real-world applications with literally hundreds of thousands of variables.We intend 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 or modern SAT solvers (mainly resolution) translate into estimations for running times and search strategies for the SAT programs. We plan to investigate the relationships and trade-offs between the different complexity measures for resolution, as well as to gain a better understanding of the formulas for which SAT solvers perform well. For the theoretical analysis of the proof systems and for the estimation of complexity bounds on the formula classes we will use methods from the areas of proof complexity and parameterized algorithmics.

• DFG Programme: Research Grants