宽度参数化SAT：时间-空间权衡
摘要：SAT的宽度参数化，如树宽和路径宽度，使我们能够研究计算上更易处理和实际的SAT实例。我们提供了两个简单的算法。其中一个在时间空间 $(O^*(2^{2tw(phi)}), O^*(2^{tw(phi)}))$ 内同时运行，另一个在时间空间 $(O^*(3^{tw(phi)log{|phi|}}),|phi|^{O(1)})$ 内运行，其中 $tw(phi)$ 是包含 $|phi|$ 个子句和变量的公式 $phi$ 的树宽。这部分回答了Alekhnovitch和Razborov的问题，他们也给出了指数时间和空间的算法，并问空间能否变得更小。我们猜测，对于这个问题，运行时间为 $2^{tw(phi)mathbf{o(log{|phi|})}}$ 的任何算法必定将空间扩大到指数级的 $tw(phi)$。
我们介绍了一种新颖的方法来结合这两个简单的算法，允许我们在运行时间和空间之间在指数中交换因子。我们的技术产生了一系列由两个参数控制的算法。通过固定一个参数，我们获得了一个在时间空间 $(O^*(3^{1.441(1-epsilon)tw(phi)log{|phi|}}), O^*(2^{2epsilon tw(phi)}))$ 中运行的算法，其中 $0 作者：Shiteng Chen, Tiancheng Lou, Periklis Papakonstantinou and Bangsheng
Tang 论文ID：1108.2385 分类：Computational Complexity 分类简称：cs.CC 提交时间：2011-08-12