Tighter Connections Between Formula-SAT and Shaving Logs
Tighter Connections Between Formula-SAT and Shaving Logs
复制标题
Formula-SAT 和剃须原木之间的联系更紧密
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
K. Bringmann
中科院分区：
文献类型：
--
作者：
Amir Abboud;K. Bringmann
在过去的几十年里，有相当一部分算法论文通过对数因子提高了解决基本问题的知名算法的运行时间。例如，最长公共子序列问题（LCS）的$O(n^2)$动态规划解决方案通过多种方式改进为$O(n^2/\log^2 n)$，并使用了各种巧妙的技巧。这类研究，也被称为“去除对数因素的艺术”，缺乏证明负面结果的工具。具体来说，我们如何证明LCS不可能及时解决$O(n^2/\log^3 n)$ ？
Abboud, Hansen, Vassilevska W. and Williams最近的一篇论文（STOC'16）可能提出了这种结果的唯一方法。作者将刨除原木的难度归咎于布尔公式（Formula-SAT）求解可满足性的难度，而不是穷尽搜索。他们表明，用于LCS的$O(n^2/\log^{1000} n)$算法将意味着电路下界的重大进步。目前尚不清楚这种做法是否会导致更严格的壁垒。
在本文中，我们将这种方法推向其极限，特别是证明了复杂性理论中一个众所周知的障碍，即在基本组合问题中去除五个额外的对数因子。对于LCS，正则表达式模式匹配，以及来自计算几何的fr<s:1>距离问题，我们表明$O(n^2/\log^{7+\varepsilon} n)$运行时将隐含新的Formula-SAT算法。
我们的主要结果是从对$n$变量的大小$s$公式的SAT减少到长度$N=2^{n/2} \cdot s^{1+o(1)}$序列的LCS。我们的还原本质上是尽可能高效的，并且它极大地改进了先前已知的使用$N=2^{n/2} \cdot s^c$的LCS还原，对于一些$c \geq 100$。
A noticeable fraction of Algorithms papers in the last few decades improve the running time of well-known algorithms for fundamental problems by logarithmic factors. For example, the $O(n^2)$ dynamic programming solution to the Longest Common Subsequence problem (LCS) was improved to $O(n^2/\log^2 n)$ in several ways and using a variety of ingenious tricks. This line of research, also known as "the art of shaving log factors", lacks a tool for proving negative results. Specifically, how can we show that it is unlikely that LCS can be solved in time $O(n^2/\log^3 n)$?
Perhaps the only approach for such results was suggested in a recent paper of Abboud, Hansen, Vassilevska W. and Williams (STOC'16). The authors blame the hardness of shaving logs on the hardness of solving satisfiability on Boolean formulas (Formula-SAT) faster than exhaustive search. They show that an $O(n^2/\log^{1000} n)$ algorithm for LCS would imply a major advance in circuit lower bounds. Whether this approach can lead to tighter barriers was unclear.
In this paper, we push this approach to its limit and, in particular, prove that a well-known barrier from complexity theory stands in the way for shaving five additional log factors for fundamental combinatorial problems. For LCS, regular expression pattern matching, as well as the Fr\'echet distance problem from Computational Geometry, we show that an $O(n^2/\log^{7+\varepsilon} n)$ runtime would imply new Formula-SAT algorithms.
Our main result is a reduction from SAT on formulas of size $s$ over $n$ variables to LCS on sequences of length $N=2^{n/2} \cdot s^{1+o(1)}$. Our reduction is essentially as efficient as possible, and it greatly improves the previously known reduction for LCS with $N=2^{n/2} \cdot s^c$, for some $c \geq 100$.