Abstract
We present a linear space data structure for Dynamic Evaluation of kCNF Boolean Formulas which achieves O(m^{11/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^{11/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 averagecase result showing the lower bounds hold even when the updates to the variables are chosen at random. Specifically, a reduction from kClique 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 kClique Hypothesis implies a lower bound of m^{(1k^{1/2})(1o(1))} which suggests our algorithm is close to optimal without involving Matrix Multiplication or new techniques. We next give an averagecase reduction to kclique 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 kCNF 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:161:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772143},
ISSN = {18688969},
year = {2021},
volume = {212},
editor = {Ahn, HeeKap and Sadakane, Kunihiko},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15494},
URN = {urn:nbn:de:0030drops154945},
doi = {10.4230/LIPIcs.ISAAC.2021.61},
annote = {Keywords: Data Structures, SAT, Dynamic Algorithms, Boolean Formulas, Finegrained Complexity, Parallel Algorithms}
}
Keywords: 

Data Structures, SAT, Dynamic Algorithms, Boolean Formulas, Finegrained Complexity, Parallel Algorithms 
Collection: 

32nd International Symposium on Algorithms and Computation (ISAAC 2021) 
Issue Date: 

2021 
Date of publication: 

30.11.2021 