Dynamic Boolean Formula Evaluation

Authors Rathish Das, Andrea Lincoln, Jayson Lynch, J. Ian Munro



PDF
Thumbnail PDF

File

LIPIcs.ISAAC.2021.61.pdf
  • Filesize: 0.71 MB
  • 19 pages

Document Identifiers

Author Details

Rathish Das
  • Cheriton School of Computer Science, University of Waterloo, Canada
Andrea Lincoln
  • University of California, Berkeley, CA, USA
  • Simons NTT Fellow, Berkeley, CA, USA
Jayson Lynch
  • Cheriton School of Computer Science, University of Waterloo, Canada
J. Ian Munro
  • Cheriton School of Computer Science, University of Waterloo, Canada

Cite As Get BibTex

Rathish Das, Andrea Lincoln, Jayson Lynch, and J. Ian Munro. Dynamic Boolean Formula Evaluation. In 32nd International Symposium on Algorithms and Computation (ISAAC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 212, pp. 61:1-61:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ISAAC.2021.61

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Data Structures
  • SAT
  • Dynamic Algorithms
  • Boolean Formulas
  • Fine-grained Complexity
  • Parallel Algorithms

Metrics

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

References

  1. 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.
  2. 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.
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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.
  6. 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.
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. 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. Google Scholar
  19. Richard Cole and Vijaya Ramachandran. Resource oblivious sorting on multicores. ACM Transactions on Parallel Computing (TOPC), 3(4):1-31, 2017. Google Scholar
  20. 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. Google Scholar
  21. 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.
  22. 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.
  23. 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. Google Scholar
  24. Akshay Degwekar, Vinod Vaikuntanathan, and Prashant Nalini Vasudevan. Fine-grained cryptography. In Annual International Cryptology Conference, pages 533-562. Springer, 2016. Google Scholar
  25. Merrick Furst, James B Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical systems theory, 17(1):13-27, 1984. Google Scholar
  26. Oded Goldreich. On counting dollartdollar-cliques mod 2. Electron. Colloquium Comput. Complex., 27:104, 2020. URL: https://eccc.weizmann.ac.il/report/2020/104.
  27. 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. Google Scholar
  28. 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. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. J. JaJa. An Introduction to Parallel Algorithms. Addison Wesley, 1997. URL: https://books.google.com/books?id=9BpYtwAACAAJ.
  32. 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. Google Scholar
  33. Ilan Kremer, Noam Nisan, and Dana Ron. On randomized one-round communication complexity. Computational Complexity, 8(1):21-49, 1999. Google Scholar
  34. 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. Google Scholar
  35. Andrea Lincoln and Adam Yedidia. Faster random k-cnf satisfiability. arXiv preprint, 2019. URL: http://arxiv.org/abs/1903.10618.
  36. 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. Google Scholar
  37. Liam Roditty and Uri Zwick. On dynamic shortest paths problems. In European Symposium on Algorithms, pages 580-591. Springer, 2004. Google Scholar
  38. Henning Schnoor. The complexity of the boolean formula value problem. Technical report, Technical report, Theoretical Computer Science, University of Hannover, 2005. Google Scholar
  39. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail