Fixed-parameter algorithms and satisfiability

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