Fixed-parameter algorithms and satisfiability

命题可满足性（SAT）是一个经典的计算问题，它为解决包括硬件和软件验证在内的各种重要问题提供了一个强大而通用的形式。在最坏的情况下，SAT很难解决；这是Cook在1972年的著名论文中第一个证明np完全的问题。今天的SAT解题器的成功表现通常可以解释为在实际应用中出现的问题实例中存在隐藏结构。该项目将研究识别问题实例中隐藏结构的算法技术，以及利用已识别的隐藏结构有效解决实例的可能性。我们将考虑Williams， Gomes, and Selman（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.