Tighter Connections Between Formula-SAT and Shaving Logs

摘要: A noticeable fraction of Algorithms papers in the last few decades improve running time well-known algorithms for fundamental problems by logarithmic factors. For example, $O(n^2)$ dynamic programming solution to Longest Common Subsequence problem (LCS) was improved $O(n^2/\log^2 n)$ several ways and using a variety ingenious tricks. This line research, also known as "the art shaving log factors", lacks tool proving negative results. Specifically, how can we show that it is unlikely LCS be solved $O(n^2/\log^3 n)$? Perhaps only approach such results suggested recent paper Abboud, Hansen, Vassilevska W. Williams (STOC'16). The authors blame hardness logs on solving satisfiability Boolean formulas (Formula-SAT) faster than exhaustive search. They an $O(n^2/\log^{1000} algorithm would imply major advance circuit lower bounds. Whether this lead tighter barriers unclear. In paper, push its limit and, particular, prove barrier from complexity theory stands way five additional factors combinatorial problems. LCS, regular expression pattern matching, well Fr\'echet distance Computational Geometry, $O(n^2/\log^{7+\varepsilon} runtime new Formula-SAT algorithms. Our main result reduction SAT size $s$ over $n$ variables sequences length $N=2^{n/2} \cdot s^{1+o(1)}$. Our essentially efficient possible, greatly improves previously with s^c$, some $c \geq 100$.