Document Open Access Logo

Tighter Connections Between Formula-SAT and Shaving Logs

Authors Amir Abboud, Karl Bringmann

Thumbnail PDF


  • Filesize: 0.49 MB
  • 18 pages

Document Identifiers

Author Details

Amir Abboud
  • IBM Almaden Research Center, San Jose, USA
Karl Bringmann
  • Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

Cite AsGet BibTex

Amir Abboud and Karl Bringmann. Tighter Connections Between Formula-SAT and Shaving Logs. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


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^3n)? 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échet distance problem from Computational Geometry, we show that an O(n^2/log^{7+epsilon}{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} * 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} * s^c, for some c >= 100.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Fine-Grained Complexity
  • Hardness in P
  • Formula-SAT
  • Longest Common Subsequence
  • Frechet Distance


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Amir Abboud, Arturs Backurs, Thomas Dueholm Hansen, Virginia Vassilevska Williams, and Or Zamir. Subtree isomorphism revisited. In Proc. of 27th SODA, pages 1256-1271, 2016. Google Scholar
  2. Amir Abboud, Arturs Backurs, and Virginia Vassilevska Williams. Tight Hardness Results for LCS and other Sequence Similarity Measures. In Proc. of 56th FOCS, pages 59-78, 2015. Google Scholar
  3. Amir Abboud, Thomas Dueholm Hansen, Virginia Vassilevska Williams, and Ryan Williams. Simulating branching programs with edit distance and friends: or: a polylog shaved is a lower bound made. In Proc. of the 48th STOC, pages 375-388, 2016. Google Scholar
  4. Amir Abboud and Virginia Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. In Proc. of 55th FOCS, pages 434-443, 2014. Google Scholar
  5. Amir Abboud, Virginia Vassilevska Williams, and Joshua R. Wang. Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs. In Proc. of 27th SODA, pages 377-391, 2016. Google Scholar
  6. Amir Abboud, Virginia Vassilevska Williams, and Oren Weimann. Consequences of faster sequence alignment. In Proc. of 41st ICALP, pages 39-51, 2014. Google Scholar
  7. Amir Abboud, Virginia Vassilevska Williams, and Huacheng Yu. Matching triangles and basing hardness on an extremely popular conjecture. In Proc. of 47th STOC, pages 41-50, 2015. Google Scholar
  8. Amir Abboud, Ryan Williams, and Huacheng Yu. More applications of the polynomial method to algorithm design. In Proc. of 26th SODA, pages 218-230, 2015. Google Scholar
  9. P. Agarwal, R. B. Avraham, H. Kaplan, and M. Sharir. Computing the discrete Fréchet distance in subquadratic time. In Proc. 24th ACM-SIAM Symposium on Discrete Algorithms (SODA'13), pages 156-167, 2013. Google Scholar
  10. Lloyd Allison and Trevor I Dix. A bit-string longest-common-subsequence algorithm. Information Processing Letters, 23(5):305-310, 1986. Google Scholar
  11. Helmut Alt and Maike Buchin. Can we compute the similarity between surfaces? Discrete &Computational Geometry, 43(1):78-99, 2010. Google Scholar
  12. Helmut Alt and Michael Godau. Computing the Fréchet distance between two polygonal curves. International Journal of Computational Geometry &Applications, 5(1-2):78-99, 1995. Google Scholar
  13. Helmut Alt, Christian Knauer, and Carola Wenk. Comparison of distance measures for planar curves. Algorithmica, 38(1):45-58, 2004. Google Scholar
  14. Stephen F Altschul, Thomas L Madden, Alejandro A Schäffer, Jinghui Zhang, Zheng Zhang, Webb Miller, and David J Lipman. Gapped blast and psi-blast: a new generation of protein database search programs. Nucleic acids research, 25(17):3389-3402, 1997. Google Scholar
  15. Alexander E Andreev. About one method of obtaining more than quadratic effective lower bounds of complexity of pi-schemes, 1987. Google Scholar
  16. V Arlazarov, E Dinic, I Faradzev, and M Kronrod. On economic construction of the transitive closure of a direct graph. In Sov. Math (Doklady), volume 11, pages 1209-1210, 1970. Google Scholar
  17. Boris Aronov, Sariel Har-Peled, Christian Knauer, Yusu Wang, and Carola Wenk. Fréchet distance for curves, revisited. In Proc. 14th Annual European Symposium on Algorithms (ESA'06), volume 4168 of LNCS, pages 52-63. Springer, 2006. Google Scholar
  18. Arturs Backurs and Piotr Indyk. Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false). In Proc. of 47th STOC, pages 51-58, 2015. Google Scholar
  19. Arturs Backurs and Piotr Indyk. Which regular expression patterns are hard to match? In FOCS, 2016. Google Scholar
  20. Nikhil Bansal and Ryan Williams. Regularity lemmas and combinatorial algorithms. In Proc. of 50th FOCS, pages 745-754, 2009. Google Scholar
  21. Ilya Baran, Erik D. Demaine, and Mihai Patrascu. Subquadratic algorithms for 3sum. Algorithmica, 50(4):584-596, 2008. URL:
  22. Paul Beame, Russell Impagliazzo, and Srikanth Srinivasan. Approximating ac^0 by small height decision trees and a deterministic algorithm for #ac^0sat. In Computational Complexity (CCC), 2012 IEEE 27th Annual Conference on, pages 117-125. IEEE, 2012. Google Scholar
  23. Philip Bille and Martin Farach-Colton. Fast and compact regular expression matching. Theoretical Computer Science, 409(3):486-496, 2008. URL:
  24. Philip Bille and Mikkel Thorup. Faster regular expression matching. In International Colloquium on Automata, Languages, and Programming, pages 171-182. Springer, 2009. Google Scholar
  25. Maria Luisa Bonet and Samuel R. Buss. Size-depth tradeoffs for boolean fomulae. Inf. Process. Lett., 49(3):151-155, 1994. URL:
  26. Sotiris Brakatsoulas, Dieter Pfoser, Randall Salas, and Carola Wenk. On map-matching vehicle tracking data. In Proc. 31st International Conference on Very Large Data Bases (VLDB'05), pages 853-864, 2005. Google Scholar
  27. Karl Bringmann. Why walking the dog takes time: Frechet distance has no strongly subquadratic algorithms unless seth fails. In Proc. of 55th FOCS, pages 661-670, 2014. Google Scholar
  28. Karl Bringmann, Allan Grønlund, and Kasper Green Larsen. A dichotomy for regular expression membership testing. CoRR, abs/1611.00918, 2016. URL:,
  29. Karl Bringmann and Marvin Künnemann. Quadratic Conditional Lower Bounds for String Problems and Dynamic Time Warping. In Proc. of 56th FOCS, pages 79-97, 2015. Google Scholar
  30. Kevin Buchin, Maike Buchin, Joachim Gudmundsson, Maarten Löffler, and Jun Luo. Detecting commuting patterns by clustering subtrajectories. International Journal of Computational Geometry &Applications, 21(3):253-282, 2011. Google Scholar
  31. Kevin Buchin, Maike Buchin, Wouter Meulemans, and Wolfgang Mulzer. Four soviets walk the dog - with an application to Alt’s conjecture. In Proc. 25th ACM-SIAM Symposium on Discrete Algorithms (SODA'14), pages 1399-1413, 2014. Google Scholar
  32. Kevin Buchin, Maike Buchin, and Yusu Wang. Exact algorithms for partial curve matching via the Fréchet distance. In Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA'09), pages 645-654, 2009. Google Scholar
  33. Massimo Cairo, Roberto Grossi, and Romeo Rizzi. New bounds for approximating extremal distances in undirected graphs. In Proceedings of the Twenty-Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2016, Arlington, VA, USA, January 10-12, 2016, pages 363-376, 2016. Google Scholar
  34. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. A duality between clause width and clause density for SAT. In Proc. of 21st CCC, pages 252-260, 2006. Google Scholar
  35. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. The complexity of satisfiability of small depth circuits. In Proc. of 4th IWPEC, pages 75-85, 2009. Google Scholar
  36. Erin Wolf Chambers, Éric Colin de Verdière, Jeff Erickson, Sylvain Lazard, Francis Lazarus, and Shripad Thite. Homotopic Fréchet distance between curves or, walking your dog in the woods in polynomial time. Computational Geometry, 43(3):295-311, 2010. Google Scholar
  37. Timothy M. Chan. The art of shaving logs. In Proc. of the 13th WADS, page 231, 2013. Google Scholar
  38. Timothy M. Chan. Speeding up the four russians algorithm by about one more logarithmic factor. In Proc. of 26th SODA, pages 212-217, 2015. Google Scholar
  39. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Model and objective separation with conditional lower bounds: Disjunction is harder than conjunction. CoRR, abs/1602.02670, 2016. URL:,
  40. Ruiwen Chen. Satisfiability algorithms and lower bounds for boolean formulas over finite bases. In International Symposium on Mathematical Foundations of Computer Science, pages 223-234. Springer, 2015. Google Scholar
  41. Ruiwen Chen and Valentine Kabanets. Correlation bounds and #sat algorithms for small linear-size circuits. In Computing and Combinatorics - 21st International Conference, COCOON 2015, Beijing, China, August 4-6, 2015, Proceedings, pages 211-222, 2015. Google Scholar
  42. Ruiwen Chen, Valentine Kabanets, Antonina Kolokolova, Ronen Shaltiel, and David Zuckerman. Mining circuit lower bound proofs for meta-algorithms. computational complexity, 24(2):333-392, 2015. Google Scholar
  43. Ruiwen Chen, Valentine Kabanets, and Nitin Saurabh. An improved deterministic#sat algorithm for small de morgan formulas. In International Symposium on Mathematical Foundations of Computer Science, pages 165-176. Springer, 2014. Google Scholar
  44. Ruiwen Chen and Rahul Santhanam. Satisfiability on mixed instances. In Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, Cambridge, MA, USA, January 14-16, 2016, pages 393-402, 2016. Google Scholar
  45. A. F. Cook and Carola Wenk. Geodesic Fréchet distance inside a simple polygon. ACM Transactions on Algorithms, 7(1):193-204, 2010. Google Scholar
  46. Thomas H.. Cormen, Charles Eric Leiserson, Ronald L Rivest, and Clifford Stein. Introduction to algorithms, volume 6. MIT press Cambridge, 2001. Google Scholar
  47. Maxime Crochemore, Costas S Iliopoulos, Yoan J Pinzon, and James F Reid. A fast and practical bit-vector algorithm for the longest common subsequence problem. Information Processing Letters, 80(6):279-285, 2001. Google Scholar
  48. Maxime Crochemore, Gad M Landau, and Michal Ziv-Ukelson. A subquadratic sequence alignment algorithm for unrestricted scoring matrices. SIAM journal on computing, 32(6):1654-1673, 2003. Google Scholar
  49. Evgeny Dantsin and Edward A. Hirsch. Worst-case upper bounds. In Handbook of Satisfiability, pages 403-424. IOS Press, 2009. URL:
  50. Anne Driemel and Sariel Har-Peled. Jaywalking your dog: computing the Fréchet distance with shortcuts. SIAM Journal on Computing, 42(5):1830-1866, 2013. Google Scholar
  51. Anne Driemel, Sariel Har-Peled, and Carola Wenk. Approximating the Fréchet distance for realistic curves in near linear time. Discrete &Computational Geometry, 48(1):94-127, 2012. Google Scholar
  52. Thomas Eiter and Heikki Mannila. Computing discrete Fréchet distance. Technical Report CD-TR 94/64, Christian Doppler Laboratory for Expert Systems, TU Vienna, Austria, 1994. Google Scholar
  53. Ari Freund. Improved subquadratic 3sum. Algorithmica, 77(2):440-458, 2017. URL:
  54. Paweł Gawrychowski. Faster algorithm for computing the edit distance between slp-compressed strings. In International Symposium on String Processing and Information Retrieval, pages 229-236. Springer, 2012. Google Scholar
  55. Michael Godau. A natural metric for curves - computing the distance for polygonal chains and approximation algorithms. In Proc. 8th Symposium on Theoretical Aspects of Computer Science (STACS'91), volume 480 of LNCS, pages 127-136. Springer, 1991. Google Scholar
  56. Omer Gold and Micha Sharir. Improved bounds for 3sum, k-sum, and linear degeneracy. CoRR, abs/1512.05279, 2015. URL:,
  57. Alexander Golovnev, Alexander S Kulikov, Alexander Smal, and Suguru Tamaki. Circuit size lower bounds and#sat upper bounds through a general framework. In Electronic Colloquium on Computational Complexity (ECCC), volume 23, page 22, 2016. Google Scholar
  58. Szymon Grabowski. New tabulation and sparse dynamic programming based techniques for sequence similarity problems. In Stringology, pages 202-211, 2014. URL:
  59. Allan Grønlund and Seth Pettie. Threesomes, degenerates, and love triangles. In 55th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2014, Philadelphia, PA, USA, October 18-21, 2014, pages 621-630, 2014. Google Scholar
  60. Johan Håstad. The shrinkage exponent of de morgan formulas is 2. SIAM J. Comput., 27(1):48-64, 1998. Google Scholar
  61. John Hopcroft, Wolfgang Paul, and Leslie Valiant. On time versus space. Journal of the ACM (JACM), 24(2):332-337, 1977. Google Scholar
  62. Heikki Hyyrö. Bit-parallel lcs-length computation revisited. In Proc. 15th Australasian Workshop on Combinatorial Algorithms (AWOCA 2004), pages 16-27. Citeseer, 2004. Google Scholar
  63. Russell Impagliazzo, Shachar Lovett, Ramamohan Paturi, and Stefan Schneider. 0-1 integer linear programming with a linear number of constraints. Electronic Colloquium on Computational Complexity (ECCC), 21:24, 2014. URL:
  64. Russell Impagliazzo, William Matthews, and Ramamohan Paturi. A satisfiability algorithm for ac 0. In Proceedings of the twenty-third annual ACM-SIAM symposium on Discrete Algorithms, pages 961-972. SIAM, 2012. Google Scholar
  65. Russell Impagliazzo and Noam Nisan. The effect of random restrictions on formula size. Random Structures &Algorithms, 4(2):121-133, 1993. Google Scholar
  66. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. Journal of Computer and System Sciences, 62(2):367-375, 2001. Google Scholar
  67. Russell Impagliazzo, Ramamohan Paturi, and Stefan Schneider. A satisfiability algorithm for sparse depth two threshold circuits. In 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, 26-29 October, 2013, Berkeley, CA, USA, pages 479-488, 2013. Google Scholar
  68. Piotr Indyk. Approximate nearest neighbor algorithms for Fréchet distance via product metrics. In Proc. 18th Annual Symposium on Computational Geometry (SoCG'02), pages 102-106, 2002. Google Scholar
  69. Valeriy M Khrapchenko. Method of determining lower bounds for the complexity of p-schemes. Mathematical Notes, 10(1):474-479, 1971. Google Scholar
  70. Ilan Komargodski, Ran Raz, and Avishay Tal. Improved average-case lower bounds for demorgan formula size. In Foundations of Computer Science (FOCS), 2013 IEEE 54th Annual Symposium on, pages 588-597. IEEE, 2013. Google Scholar
  71. Isaac TS Li, Warren Shum, and Kevin Truong. 160-fold acceleration of the smith-waterman algorithm using a field programmable gate array (fpga). BMC bioinformatics, 8(1):1, 2007. Google Scholar
  72. Yongchao Liu, Adrianto Wirawan, and Bertil Schmidt. Cudasw++ 3.0: accelerating smith-waterman protein database search by coupling cpu and gpu simd instructions. BMC bioinformatics, 14(1):1, 2013. Google Scholar
  73. Anil Maheshwari, Jörg-Rüdiger Sack, Kaveh Shahbaz, and Hamid Zarrabi-Zadeh. Fréchet distance with speed limits. Computational Geometry, 44(2):110-120, 2011. Google Scholar
  74. William J Masek and Michael S Paterson. A faster algorithm computing string edit distances. Journal of Computer and System sciences, 20(1):18-31, 1980. Google Scholar
  75. Daniel Moeller, Ramamohan Paturi, and Stefan Schneider. Subquadratic algorithms for succinct stable matching. In Computer Science - Theory and Applications - 11th International Computer Science Symposium in Russia, CSR 2016, St. Petersburg, Russia, June 9-13, 2016, Proceedings, pages 294-308, 2016. Google Scholar
  76. Mario E. Munich and Pietro Perona. Continuous dynamic time warping for translation-invariant curve alignment with applications to signature verification. In Proc. 7th IEEE International Conference on Computer Vision, volume 1, pages 108-115, 1999. Google Scholar
  77. Gene Myers. A four russians algorithm for regular expression pattern matching. Journal of the ACM (JACM), 39(2):432-448, 1992. Google Scholar
  78. Igor C Oliveira. Algorithms versus circuit lower bounds. CoRR, abs/1309.0249, 2013. URL:
  79. Michael S Paterson and Uri Zwick. Shrinkage of de morgan formulae under restriction. Random Structures &Algorithms, 4(2):135-150, 1993. Google Scholar
  80. Mihai Patrascu and Ryan Williams. On the possibility of faster SAT algorithms. In Proc. of 21st SODA, pages 1065-1075, 2010. Google Scholar
  81. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337-364, 2005. Google Scholar
  82. Liam Roditty and Virginia Vassilevska Williams. Fast approximation algorithms for the diameter and radius of sparse graphs. In Proc. of 45th STOC, pages 515-524, 2013. Google Scholar
  83. Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, and Junichi Teruyama. A satisfiability algorithm for depth-2 circuits with a symmetric gate at the top and and gates at the bottom. In Electronic Colloquium on Computational Complexity (ECCC), 2015. Google Scholar
  84. Rahul Santhanam. Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In Proc. of the 51th FOCS, pages 183-192, 2010. Google Scholar
  85. Rahul Santhanam et al. Ironic complicity: Satisfiability algorithms and circuit lower bounds. Bulletin of EATCS, 1(106), 2013. Google Scholar
  86. Kazuhisa Seto and Suguru Tamaki. A satisfiability algorithm and average-case hardness for formulas over the full binary basis. computational complexity, 22(2):245-274, 2013. Google Scholar
  87. Temple F Smith and Michael S Waterman. Identification of common molecular subsequences. Journal of molecular biology, 147(1):195-197, 1981. Google Scholar
  88. Philip M Spira. On time-hardware complexity tradeoffs for boolean functions. In Proceedings of the 4th Hawaii Symposium on System Sciences, pages 525-527, 1971. Google Scholar
  89. Bella Abramovna Subbotovskaya. Realizations of linear functions by formulas using+. Doklady Akademii Nauk SSSR, 136(3):553-555, 1961. Google Scholar
  90. Avishay Tal. Shrinkage of de morgan formulae by spectral techniques. In Foundations of Computer Science (FOCS), 2014 IEEE 55th Annual Symposium on, pages 551-560. IEEE, 2014. Google Scholar
  91. Avishay Tal. #sat algorithms from shrinkage. Electronic Colloquium on Computational Complexity (ECCC), 22:114, 2015. URL:
  92. Ken Thompson. Programming techniques: Regular expression search algorithm. Communications of the ACM, 11(6):419-422, 1968. Google Scholar
  93. Robert A Wagner and Michael J Fischer. The string-to-string correction problem. Journal of the ACM (JACM), 21(1):168-173, 1974. Google Scholar
  94. Ryan Williams. A new algorithm for optimal 2-constraint satisfaction and its implications. Theoretical Computer Science, 348(2):357-365, 2005. Google Scholar
  95. Ryan Williams. Improving exhaustive search implies superpolynomial lower bounds. SIAM Journal on Computing, 42(3):1218-1244, 2013. Google Scholar
  96. Ryan Williams. Algorithms for Circuits and Circuits for Algorithms: Connecting the Tractable and Intractable. In Proc. International Congress of Mathematicians, 2014. Google Scholar
  97. Ryan Williams. Faster all-pairs shortest paths via circuit complexity. In Proc. of 46th STOC, pages 664-673, 2014. Google Scholar
  98. Ryan Williams. Nonuniform ACC circuit lower bounds. J. ACM, 61(1):2:1-2:32, 2014. Google Scholar
  99. Huacheng Yu. An improved combinatorial algorithm for boolean matrix multiplication. In Proc. of 42nd ICALP, pages 1094-1105, 2015. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail