Fixed-parameter algorithms and satisfiability

命题可满足性(SAT)是一个经典的计算问题，它为解决包括硬件验证和软件验证在内的各种重要问题提供了一种强大而通用的形式。在最坏的情况下，SAT是很难解决的；这是库克在他著名的1972年的论文中证明的第一个NP-完全问题。今天的SAT解算器的成功性能通常由实际应用中出现的问题实例中的隐藏结构来解释。本项目将研究在问题实例中识别隐藏结构的算法技术，以及利用已识别的隐藏结构有效地解决实例的可能性。我们将考虑威廉姆斯、戈麦斯和塞尔曼2003年提出的关于小型后门集的隐藏结构。我们的研究具有理论和实践两方面的目标。我们的理论目标是设计和分析后门程序检测算法。特别是，我们将在参数化复杂性的框架内研究后门集合检测(Downey And Fellows1999)。实际目标要求实施基准实例的算法和实证研究。进一步的目标是将后门集的研究扩展到与SAT相关的问题或推广到SAT的问题，包括计数问题和约束满足问题。

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.