宽度参数化的SAT：时空权衡
Width-parameterized SAT: Time-Space Tradeoffs
摘要：
SAT的宽度参数化，如树宽度和路径宽度，使计算更容易处理和实用的SAT实例的研究。我们给出了两个简单的算法。一个在时间-空间$(O^*(2^{2tw(ϕ)}), O^*(2^{tw(ϕ)}))$中同时运行，另一个在时间-空间$(O^*(3^{tw(ϕ)\log{|ϕ|}}),|ϕ|^{O(1)})$中运行，其中$tw(ϕ)$是公式$ϕ$的树宽，其中有$|ϕ|$许多子句和变量。这部分回答了Alekhnovitch和Razborov的问题，他们也给出了算法在时间和空间上的指数，并询问是否可以使空间更小。我们推测，这个问题的每一个算法，运行在时间$2^{tw(ϕ)\mathbf{o(\log{|ϕ|})}}$必然炸毁的空间指数在$tw(ϕ)$。我们引入了一种新的方法来结合这两个简单的算法，使我们能够贸易\emph{constant}因素之间的指数运行时间和空间。我们的技术产生了由两个参数控制的一系列算法。通过固定一个参数，我们得到一个算法，运行在时间-空间$(O^*(3^{1.441(1-ε)tw(ϕ)\log{|ϕ|}}), O^*(2^{2εtw(ϕ)}))$，对每个$0<ε<1$。我们系统地研究了这种技术的局限性，并表明，这些算法的结果是最好的实现使用这种技术。我们还进一步研究了SAT的宽度参数化的计算复杂性。我们证明了非稀疏化的路径宽度$ω(\log|ϕ|)$的公式的下界，和分离的复杂性的路径宽度和树宽度参数化SAT模合理的复杂性假设。
英文摘要：
Width parameterizations of SAT, such as tree-width and path-width, enable the study of computationally more tractable and practical SAT instances. We give two simple algorithms. One that runs simultaneously in time-space $(O^*(2^{2tw(ϕ)}), O^*(2^{tw(ϕ)}))$ and another that runs in time-space $(O^*(3^{tw(ϕ)\log{|ϕ|}}),|ϕ|^{O(1)})$, where $tw(ϕ)$ is the tree-width of a formula $ϕ$ with $|ϕ|$ many clauses and variables. This partially answers the question of Alekhnovitch and Razborov, who also gave algorithms exponential both in time and space, and asked whether the space can be made smaller. We conjecture that every algorithm for this problem that runs in time $2^{tw(ϕ)\mathbf{o(\log{|ϕ|})}}$ necessarily blows up the space to exponential in $tw(ϕ)$. We introduce a novel way to combine the two simple algorithms that allows us to trade \emph{constant} factors in the exponents between running time and space. Our technique gives rise to a family of algorithms controlled by two parameters. By fixing one parameter we obtain an algorithm that runs in time-space $(O^*(3^{1.441(1-ε)tw(ϕ)\log{|ϕ|}}), O^*(2^{2εtw(ϕ)}))$, for every $0<ε<1$. We systematically study the limitations of this technique, and show that these algorithmic results are the best achievable using this technique. We also study further the computational complexity of width parameterizations of SAT. We prove non-sparsification lower bounds for formulas of path-width $ω(\log|ϕ|)$, and a separation between the complexity of path-width and tree-width parametrized SAT modulo plausible complexity assumptions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
