A Bloom Filter-based Algorithm for Fast Detection of Common Variables
Zhen Wang, Kang Liu, Chao Xu · 2023
Satisfiability problem has significant applications in many fields, such as software verification and Robot path planning. Researchers have proposed many reduction rules for the conjunctive normal form formula, some of which need to detect the common variables in the formula. Even though these reduction rules only take polynomial time, when the time complexity of the rules exceeds $O\left(n^{3}\right)$, recursive inprocessing detections with in each branch are time-consuming. Due to this, the Bloom Common Variable Detection Algorithm (CVDA-Bloom) is proposed, which is based on the Bloom filter concept and hash clause detection technique. The hash method is utilized as a filter to detect common variables, while the Bloom filter concept is used to reduce the false positive rate in the hash process. The experiments used 85 SAT instances from 7 series of the SAT2021 Competition. The results show that compared to the pure hash clause detection technique, the clause pass rate of the CVDA-Bloom algorithm decreases by $21.01 \%$ on average, and the false positive rate decreases by $66.57\%$ on average. Furthermore, disabling the Bloom hash clause detection technique will increase the time by $260.03\%$. When used with the actual reduction rules, the CVDA-Bloom algorithm effectively lowers the number of clauses that must be checked explicitly, which can lower the performance overhead and speed up the detection.