Complexity measures for solving propositional formulas.

求解命题公式的复杂性度量。

• 批准号: 430150230
• 负责人: Professor Dr. Jacobo Torán
• 金额: --
• 依托单位: Institut für Theoretische Informatik (Theo)
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/430150230?language=en
• 关键词: Complexity; measures; solving; propositional; formulas.

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.

命题逻辑的可满足性问题 SAT 是最著名的 NP 完全问题，它是理论计算机科学许多领域的核心。因此，传统上它被认为很难解决。然而，在过去的几十年里，解决 SAT 实例的程序的开发取得了令人印象深刻的进步。如今，这些程序用数十万个变量来解决现实世界的应用程序。我们打算通过关注根证明系统或现代 SAT 求解器（主要是分辨率）的几种复杂性度量如何转化为 SAT 程序的运行时间估计和搜索策略，更好地理解理论与实践之间的差距。我们计划研究解决方案的不同复杂性度量之间的关系和权衡，并更好地理解 SAT 求解器表现良好的公式。对于证明系统的理论分析和公式类复杂性界限的估计，我们将使用证明复杂性和参数化算法领域的方法。