Fixed-parameter algorithms and satisfiability

固定参数算法和可满足性

• 批准号: EP/E001394/1
• 负责人: Stefan Szeider
• 金额: $ 26.22万
• 依托单位: Durham University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FE001394%2F1
• 关键词: Fixed; parameter; algorithms; satisfiability

Propositional satisfiability (SAT) is the classical computationalproblem that provides a powerful and general formalism for solvingvarious important problems including hardware and softwareverification. SAT is hard to solve in the worst case; it is the firstproblem that was shown to be NP-complete by Cook in his famous 1972paper. The successful performance of today's SAT solvers is usuallyexplained by the presence of a hidden structure in problem instancesthat arise from practical applications.This project will research on algorithmic techniques for identifying ahidden structure in a problem instance, and on possibilities ofexploiting identified hidden structures for solving the instanceefficiently. We will consider a hidden structure in terms of small backdoor sets as proposed by Williams, Gomes, and Selman, 2003. Our research has theoretical and practical objectives. Our theoreticalobjectives entail the design and analysis of algorithms for backdoorset detection. In particular, we will study backdoor set detection inthe framework of parameterized complexity (Downey and Fellows1999). Practical objectives entail the implementation of thealgorithms and empirical studies of benchmark instances. A furtherobjective is to extend the research on backdoor sets to problems thatare related to or generalise SAT; that includes counting problems andconstraint satisfaction problems.

命题可满足性（SAT）是经典的计算问题，它为解决包括硬件和软件验证在内的各种重要问题提供了一种强有力的通用形式。在最坏的情况下，SAT很难求解;这是库克在其著名的1972年论文中证明的第一个NP完全问题。当今SAT求解器的成功性能通常是由实际应用中出现的问题实例中的隐藏结构的存在来解释的。本项目将研究识别问题实例中隐藏结构的算法技术，以及利用识别出的隐藏结构有效解决问题实例的可能性。我们将根据威廉姆斯、戈麦斯和塞尔曼在2003年提出的小后门集来考虑隐藏结构。我们的研究有理论和实践目的。我们的理论目标是设计和分析后门集检测算法。特别地，我们将在参数化复杂性的框架中研究后门集检测（唐尼和Fellows 1999）。实践目标需要算法的实现和基准实例的实证研究。另一个目标是将后门集的研究扩展到与SAT相关或推广SAT的问题，包括计数问题和约束满足问题。

项目成果

Parameterized Proof Complexity

参数化证明复杂性

• DOI: 10.1007/s00037-010-0001-1
• 发表时间: 2011
• 期刊: computational complexity
• 影响因子: 1.4
• 作者: Dantchev S