摘要翻译：
Knuth(1990)引入了一类嵌套公式，并证明了它们的可满足性可以在多项式时间内判定。我们证明了，以目标类嵌套公式的最小强后门集的大小为参数，检验任意CNF公式的可满足性是固定参数可处理的。因此，对于任意k>0的公式F,只要存在一个大小至多为k的变量集B，使得对于每一个真值赋值t到B,公式F[t]是嵌套的，就可以在多项式时间内解决可满足性问题；而且，多项式的次与k无关。我们的算法利用Robertson和Seymour（1986）的网格小定理，或者发现公式的关联图有界树宽--这种情况可以用一元二阶逻辑的模型检验来解决--或者在关联图中发现许多顶点不相交的阻塞。对于后一种情况，使用新的组合参数来查找小后门集。结合这两种情况导致一个近似算法产生一个强大的后门集，其大小由最优函数上界。通过对这组变量的所有赋值，利用Knuth算法，确定了输入公式的可满足性。
---
英文标题：
《Strong Backdoors to Nested Satisfiability》
---
作者：
Serge Gaspers and Stefan Szeider
---
最新提交年份：
2012
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Data Structures and Algorithms        数据结构与算法
分类描述：Covers data structures and analysis of algorithms. Roughly includes material in ACM Subject Classes E.1, E.2, F.2.1, and F.2.2.
涵盖数据结构和算法分析。大致包括ACM学科类E.1、E.2、F.2.1和F.2.2中的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Computational Complexity        计算复杂度
分类描述：Covers models of computation, complexity classes, structural complexity, complexity tradeoffs, upper and lower bounds. Roughly includes material in ACM Subject Classes F.1 (computation by abstract devices), F.2.3 (tradeoffs among complexity measures), and F.4.3 (formal languages), although some material in formal languages may be more appropriate for Logic in Computer Science. Some material in F.2.1 and F.2.2, may also be appropriate here, but is more likely to have Data Structures and Algorithms as the primary subject area.
涵盖计算模型，复杂度类别，结构复杂度，复杂度折衷，上限和下限。大致包括ACM学科类F.1（抽象设备的计算）、F.2.3（复杂性度量之间的权衡）和F.4.3（形式语言）中的材料，尽管形式语言中的一些材料可能更适合于计算机科学中的逻辑。在F.2.1和F.2.2中的一些材料可能也适用于这里，但更有可能以数据结构和算法作为主要主题领域。
--
一级分类：Mathematics        数学
二级分类：Combinatorics        组合学
分类描述：Discrete mathematics, graph theory, enumeration, combinatorial optimization, Ramsey theory, combinatorial game theory
离散数学，图论，计数，组合优化，拉姆齐理论，组合对策论
--

---
英文摘要：
  Knuth (1990) introduced the class of nested formulas and showed that their satisfiability can be decided in polynomial time. We show that, parameterized by the size of a smallest strong backdoor set to the target class of nested formulas, checking the satisfiability of any CNF formula is fixed-parameter tractable. Thus, for any k>0, the satisfiability problem can be solved in polynomial time for any formula F for which there exists a variable set B of size at most k such that for every truth assignment t to B, the formula F[t] is nested; moreover, the degree of the polynomial is independent of k.   Our algorithm uses the grid-minor theorem of Robertson and Seymour (1986) to either find that the incidence graph of the formula has bounded treewidth - a case that is solved using model checking for monadic second order logic - or to find many vertex-disjoint obstructions in the incidence graph. For the latter case, new combinatorial arguments are used to find a small backdoor set. Combining both cases leads to an approximation algorithm producing a strong backdoor set whose size is upper bounded by a function of the optimum. Going through all assignments to this set of variables and using Knuth's algorithm, the satisfiability of the input formula is decided.
---
PDF链接：
https://arxiv.org/pdf/1202.4331