Dynamic Boolean Formula Evaluation
We present a linear space data structure for Dynamic Evaluation of k-CNF Boolean Formulas which achieves O(m^{1-1/k}) query and variable update time where m is the number of clauses in the formula and clauses are of size at most a constant k. Our algorithm is additionally able to count the total number of satisfied clauses. We then show how this data structure can be parallelized in the PRAM model to achieve O(log m) span (i.e. parallel time) and still O(m^{1-1/k}) work. This parallel algorithm works in the stronger Binary Fork model.
We then give a series of lower bounds on the problem including an average-case result showing the lower bounds hold even when the updates to the variables are chosen at random. Specifically, a reduction from k-Clique shows that dynamically counting the number of satisfied clauses takes time at least n^{(2ω-3)/6 √{2k} -1 -o(√k)}, where 2 ≤ ω < 2.38 is the matrix multiplication constant. We show the Combinatorial k-Clique Hypothesis implies a lower bound of m^{(1-k^{-1/2})(1-o(1))} which suggests our algorithm is close to optimal without involving Matrix Multiplication or new techniques. We next give an average-case reduction to k-clique showing the prior lower bounds hold even when the updates are chosen at random. We use our conditional lower bound to show any Binary Fork algorithm solving these problems requires at least Ω(log m) span, which is tight against our algorithm in this model. Finally, we give an unconditional linear space lower bound for Dynamic k-CNF Boolean Formula Evaluation.
Data Structures
SAT
Dynamic Algorithms
Boolean Formulas
Fine-grained Complexity
Parallel Algorithms
Theory of computation~Design and analysis of algorithms
61:1-61:19
Regular Paper
Rathish
Das
Rathish Das
Cheriton School of Computer Science, University of Waterloo, Canada
Supported by the Canada Research Chairs Programme and NSERC Discovery Grants.
Andrea
Lincoln
Andrea Lincoln
University of California, Berkeley, CA, USA
Simons NTT Fellow, Berkeley, CA, USA
This work is supported partly by NSF 1652303, 1909046, and HDR TRIPODS 1934846 grants, and an Alfred P. Sloan Fellowship. This work was also supported by the Simons NTT research fellowship.
Jayson
Lynch
Jayson Lynch
Cheriton School of Computer Science, University of Waterloo, Canada
Supported by the Canada Research Chairs Programme and NSERC Discovery Grants.
J. Ian
Munro
J. Ian Munro
Cheriton School of Computer Science, University of Waterloo, Canada
Supported by the Canada Research Chairs Programme and NSERC Discovery Grants.
10.4230/LIPIcs.ISAAC.2021.61
Amir Abboud, Arturs Backurs, Karl Bringmann, and Marvin Künnemann. Fine-grained complexity of analyzing compressed data: Quantifying improvements over decompress-and-solve. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 192-203. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.26.
https://doi.org/10.1109/FOCS.2017.26
Amir Abboud, Arturs Backurs, and Virginia Vassilevska Williams. If the current clique algorithms are optimal, so is valiant’s parser. In Venkatesan Guruswami, editor, IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 98-117. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FOCS.2015.16.
https://doi.org/10.1109/FOCS.2015.16
Amir Abboud and Virginia Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. In 2014 IEEE 55th Annual Symposium on Foundations of Computer Science, pages 434-443. IEEE, 2014.
Umut A Acar, Guy E Blelloch, and Robert D Blumofe. The data locality of work stealing. In ACM symposium on Parallel algorithms and architectures, pages 1-12, 2000.
David Alberts and Monika Rauch Henzinger. Average case analysis of dynamic graph algorithms. In Kenneth L. Clarkson, editor, Proceedings of the Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, 22-24 January 1995. San Francisco, California, USA, pages 312-321. ACM/SIAM, 1995. URL: http://dl.acm.org/citation.cfm?id=313651.313712.
http://dl.acm.org/citation.cfm?id=313651.313712
Josh Alman and Virginia Vassilevska Williams. A refined laser method and faster matrix multiplication. CoRR, abs/2010.05846, 2020. URL: http://arxiv.org/abs/2010.05846.
http://arxiv.org/abs/2010.05846
Marshall Ball, Alon Rosen, Manuel Sabin, and Prashant Nalini Vasudevan. Average-case fine-grained hardness. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, pages 483-496, 2017.
Marshall Ball, Alon Rosen, Manuel Sabin, and Prashant Nalini Vasudevan. Proofs of work from worst-case assumptions. In Annual International Cryptology Conference, pages 789-819. Springer, 2018.
Naama Ben-David, Guy E Blelloch, Jeremy T Fineman, Phillip B Gibbons, Yan Gu, Charles McGuffey, and Julian Shun. Parallel algorithms for asymmetric read-write costs. In ACM Symposium on Parallelism in Algorithms and Architectures, pages 145-156, 2016.
Guy E Blelloch, Rezaul Alam Chowdhury, Phillip B Gibbons, Vijaya Ramachandran, Shimin Chen, and Michael Kozuch. Provably good multicore cache performance for divide-and-conquer algorithms. In SODA, volume 8, pages 501-510. Citeseer, 2008.
Guy E Blelloch, Jeremy T Fineman, Phillip B Gibbons, and Harsha Vardhan Simhadri. Scheduling irregular parallel computations on hierarchical caches. In ACM symposium on Parallelism in algorithms and architectures, pages 355-366, 2011.
Guy E Blelloch, Jeremy T Fineman, Yan Gu, and Yihan Sun. Optimal parallel algorithms in the binary-forking model. In ACM Symposium on Parallelism in Algorithms and Architectures, pages 89-102, 2020.
Guy E Blelloch, Jeremy T Fineman, Yan Gu, and Yihan Sun. Optimal parallel algorithms in the binary-forking model. In Proceedings of the 32nd ACM Symposium on Parallelism in Algorithms and Architectures, pages 89-102, 2020.
Enric Boix-Adserà, Matthew Brennan, and Guy Bresler. The average-case complexity of counting cliques in erdős-rényi hypergraphs. In 2019 IEEE 60th Annual Symposium on Foundations of Computer Science (FOCS), pages 1256-1280. IEEE, 2019.
Enric Boix-Adserà, Matthew Brennan, and Guy Bresler. The average-case complexity of counting cliques in erdős-rényi hypergraphs. In David Zuckerman, editor, 60th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2019, Baltimore, Maryland, USA, November 9-12, 2019, pages 1256-1280. IEEE Computer Society, 2019.
S Buss, S Cook, Arvind Gupta, and Vijaya Ramachandran. An optimal parallel algorithm for formula evaluation. SIAM Journal on Computing, 21(4):755-780, 1992.
Samuel R Buss. The boolean formula value problem is in alogtime. In Proceedings of the nineteenth annual ACM symposium on Theory of computing, pages 123-131, 1987.
Feng Chen and Grigore Roşu. Towards monitoring-oriented programming: A paradigm combining specification and implementation. Electronic Notes in Theoretical Computer Science, 89(2):108-127, 2003.
Richard Cole and Vijaya Ramachandran. Resource oblivious sorting on multicores. ACM Transactions on Parallel Computing (TOPC), 3(4):1-31, 2017.
Søren Dahlgaard. On the hardness of partially dynamic graph problems and connections to diameter. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.
Mina Dalirrooyfard, Andrea Lincoln, and Virginia Vassilevska Williams. New techniques for proving fine-grained average-case hardness. arXiv preprint, 2020. URL: http://arxiv.org/abs/2008.06591.
http://arxiv.org/abs/2008.06591
Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon M. Kleinberg, Christos H. Papadimitriou, Prabhakar Raghavan, and Uwe Schöning. A deterministic (2-2/(k+1))^n algorithm for k-SAT based on local search. Theor. Comput. Sci., 289(1):69-83, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00174-8.
https://doi.org/10.1016/S0304-3975(01)00174-8
Rathish Das, Shih-Yu Tsai, Sharmila Duppala, Jayson Lynch, Esther M Arkin, Rezaul Chowdhury, Joseph SB Mitchell, and Steven Skiena. Data races and the discrete resource-time tradeoff problem with resource reuse over paths. In ACM Symposium on Parallelism in Algorithms and Architectures, pages 359-368, 2019.
Akshay Degwekar, Vinod Vaikuntanathan, and Prashant Nalini Vasudevan. Fine-grained cryptography. In Annual International Cryptology Conference, pages 533-562. Springer, 2016.
Merrick Furst, James B Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical systems theory, 17(1):13-27, 1984.
Oded Goldreich. On counting dollartdollar-cliques mod 2. Electron. Colloquium Comput. Complex., 27:104, 2020. URL: https://eccc.weizmann.ac.il/report/2020/104.
https://eccc.weizmann.ac.il/report/2020/104
Oded Goldreich and Guy Rothblum. Counting t-cliques: Worst-case to average-case reductions and direct interactive proof systems. In 2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS), pages 77-88. IEEE, 2018.
Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai, and Thatchaphol Saranurak. Unifying and strengthening hardness for dynamic problems via the online matrix-vector multiplication conjecture. In Proceedings of the forty-seventh annual ACM symposium on Theory of computing, pages 21-30, 2015.
Monika Henzinger, Andrea Lincoln, Stefan Neumann, and Virginia Vassilevska Williams. Conditional hardness for sensitivity problems. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
Shuichi Hirahara and Nobutaka Shimizu. Nearly optimal average-case complexity of counting bicliques under seth. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 2346-2365. SIAM, 2021.
J. JaJa. An Introduction to Parallel Algorithms. Addison Wesley, 1997. URL: https://books.google.com/books?id=9BpYtwAACAAJ.
https://books.google.com/books?id=9BpYtwAACAAJ
Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, and Mahesh Viswanathan. Java-mac: a run-time assurance tool for java programs. Electronic Notes in Theoretical Computer Science, 55(2):218-235, 2001.
Ilan Kremer, Noam Nisan, and Dana Ron. On randomized one-round communication complexity. Computational Complexity, 8(1):21-49, 1999.
Rio LaVigne, Andrea Lincoln, and Virginia Vassilevska Williams. Public-key cryptography in the fine-grained setting. In Annual International Cryptology Conference, pages 605-635. Springer, 2019.
Andrea Lincoln and Adam Yedidia. Faster random k-cnf satisfiability. arXiv preprint, 2019. URL: http://arxiv.org/abs/1903.10618.
http://arxiv.org/abs/1903.10618
Mihai Patrascu. Towards polynomial lower bounds for dynamic problems. In Proceedings of the forty-second ACM symposium on Theory of computing, pages 603-610, 2010.
Liam Roditty and Uri Zwick. On dynamic shortest paths problems. In European Symposium on Algorithms, pages 580-591. Springer, 2004.
Henning Schnoor. The complexity of the boolean formula value problem. Technical report, Technical report, Theoretical Computer Science, University of Hannover, 2005.
Uwe Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18 October, 1999, New York, NY, USA, pages 410-414, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814612.
https://doi.org/10.1109/SFFCS.1999.814612
Rathish Das, Andrea Lincoln, Jayson Lynch, and J. Ian Munro
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode