嵌套可满足性的强后门
Strong Backdoors to Nested Satisfiability
摘要：
Knuth（1990）引入了嵌套公式类，并证明了它们的可满足性可以在多项式时间内判定。我们表明，参数化的最小强后门集的大小的嵌套公式的目标类，检查可满足性的任何CNF公式是固定参数听话。因此，对于任何k>0，可满足性问题可以在多项式时间内解决，对于任何公式F，存在大小至多为k的变量集B，使得对于每个真值赋值t到B，公式F[t]是嵌套的;此外，多项式的次数与k无关。我们的算法使用Robertson和Seymour（1986）的网格子定理来发现公式的关联图具有有界树宽（这种情况使用一元二阶逻辑的模型检验来解决）或者在关联图中找到许多顶点不相交的障碍物。对于后一种情况，新的组合参数被用来找到一个小的后门集。结合这两种情况下，导致一个近似算法产生一个强大的后门集的大小是上界的最佳功能。通过对这组变量的所有赋值，并使用Knuth算法，确定输入公式的可满足性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
