SAT的递归后门
Recursive Backdoors for SAT
摘要：
在命题逻辑的公式$ϕ$中，到一个易处理的公式类$\mathcal{C}$的强后门是$ϕ$的变量的集合$B$，使得$B$中的变量的每次赋值都导致来自$\mathcal{C}$的公式。小尺寸或具有良好结构的强后门，例如具有小的后门树宽度，导致命题可满足性问题SAT的有效解决方案。在本文中，我们提出了递归后门的新概念，这是由观察，为了解决SAT我们可以独立递归到部分分配的变量创建的组件的启发。递归后门的质量是通过其递归后门深度来衡量的。类似于后门树宽的概念，有界深度的递归后门包括具有某种树状结构的无限大小的后门。然而，这两个概念是不可比拟的，我们的结果产生新的可处理性结果SAT。
英文摘要：
A strong backdoor in a formula $ϕ$ of propositional logic to a tractable class $\mathcal{C}$ of formulas is a set $B$ of variables of $ϕ$ such that every assignment of the variables in $B$ results in a formula from $\mathcal{C}$. Strong backdoors of small size or with a good structure, e.g. with small backdoor treewidth, lead to efficient solutions for the propositional satisfiability problem SAT. In this paper we propose the new notion of recursive backdoors, which is inspired by the observation that in order to solve SAT we can independently recurse into the components that are created by partial assignments of variables. The quality of a recursive backdoor is measured by its recursive backdoor depth. Similar to the concept of backdoor treewidth, recursive backdoors of bounded depth include backdoors of unbounded size that have a certain treelike structure. However, the two concepts are incomparable and our results yield new tractability results for SAT.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
