License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ISAAC.2021.61
URN: urn:nbn:de:0030-drops-154945
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15494/
Go to the corresponding LIPIcs Volume Portal

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

Dynamic Boolean Formula Evaluation

pdf-format:
LIPIcs-ISAAC-2021-61.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{das_et_al:LIPIcs.ISAAC.2021.61,
  author =	{Das, Rathish and Lincoln, Andrea and Lynch, Jayson and Munro, J. Ian},
  title =	{{Dynamic Boolean Formula Evaluation}},
  booktitle =	{32nd International Symposium on Algorithms and Computation (ISAAC 2021)},
  pages =	{61:1--61:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-214-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{212},
  editor =	{Ahn, Hee-Kap and Sadakane, Kunihiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15494},
  URN =		{urn:nbn:de:0030-drops-154945},
  doi =		{10.4230/LIPIcs.ISAAC.2021.61},
  annote =	{Keywords: Data Structures, SAT, Dynamic Algorithms, Boolean Formulas, Fine-grained Complexity, Parallel Algorithms}
}

Keywords: Data Structures, SAT, Dynamic Algorithms, Boolean Formulas, Fine-grained Complexity, Parallel Algorithms
Collection: 32nd International Symposium on Algorithms and Computation (ISAAC 2021)
Issue Date: 2021
Date of publication: 30.11.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI