×

Hash-based preprocessing and inprocessing techniques in SAT solvers. (English) Zbl 07495567

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 82-97 (2021).
Summary: Modern satisfiability solvers are interwoven with important simplification techniques as preprocessors and inprocessors. Implementations of these techniques are hampered by expensive memory accesses which result in a large number of cache misses. This paper explores the application of hash functions in encoding clause structures and bitwise operations for detecting relations between clauses. The evaluation showed a significant increase in performance for subsumption and Blocked Clause Elimination on the Main track benchmark of the 2020 SAT competition.
For the entire collection see [Zbl 1482.68030].

MSC:

68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

MaxPre; MiniSat
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Bakhtiari, S., Safavi-Naini, R., Pieprzyk, J., et al.: Cryptographic hash functions: A survey. Technical Report, Citeseer (1995) · Zbl 1421.94037
[2] Balyo, T., Froleyks, N., Heule, M.J., Iser, M., Järvisalo, M., Suda, M.: Proceedings of sat competition 2020: Solver and benchmark descriptions (2020)
[3] Bayardo, R.J., Panda, B.: Fast algorithms for finding extremal sets. In: Proceedings of the 2011 SIAM International Conference on Data Mining, pp. 25-34. SIAM (2011)
[4] Eén, N.; Biere, A.; Bacchus, F.; Walsh, T., Effective preprocessing in SAT through variable and clause elimination, Theory and Applications of Satisfiability Testing, 61-75 (2005), Heidelberg: Springer, Heidelberg · Zbl 1128.68463
[5] Han, H.; Somenzi, F.; Kullmann, O., On-the-fly clause improvement, Theory and Applications of Satisfiability Testing, 209-222 (2009), Heidelberg: Springer, Heidelberg
[6] Järvisalo, M.; Biere, A.; Heule, M.; Esparza, J.; Majumdar, R., Blocked clause elimination, Tools and Algorithms for the Construction and Analysis of Systems, 129-144 (2010), Heidelberg: Springer, Heidelberg · Zbl 1306.68144
[7] Järvisalo, M.; Heule, MJH; Biere, A.; Gramlich, B.; Miller, D.; Sattler, U., Inprocessing rules, Automated Reasoning, 355-370 (2012), Heidelberg: Springer, Heidelberg · Zbl 1358.68256
[8] Jovanović, D.; Janičić, P.; Gramlich, B., Logical analysis of hash functions, Frontiers of Combining Systems, 200-215 (2005), Heidelberg: Springer, Heidelberg · Zbl 1171.94351
[9] Korhonen, T.; Berg, J.; Saikko, P.; Järvisalo, M.; Gaspers, S.; Walsh, T., MaxPre: an extended MaxSAT preprocessor, Theory and Applications of Satisfiability Testing - SAT 2017, 449-456 (2017), Cham: Springer, Cham · Zbl 06807242
[10] Legendre, F., Dequen, G., Krajecki, M.: Encoding hash functions as a sat problem. In: 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, vol. 1, pp. 916-921. IEEE (2012)
[11] de Mare, M.; Wright, RN; Ning, P.; Qing, S.; Li, N., Secure set membership using 3Sat, Information and Communications Security, 452-468 (2006), Heidelberg: Springer, Heidelberg
[12] Mironov, I.; Zhang, L.; Biere, A.; Gomes, CP, Applications of SAT solvers to cryptanalysis of hash functions, Theory and Applications of Satisfiability Testing - SAT 2006, 102-115 (2006), Heidelberg: Springer, Heidelberg · Zbl 1187.94028
[13] Nejati, S.; Liang, JH; Gebotys, C.; Czarnecki, K.; Ganesh, V.; Paskevich, A.; Wies, T., Adaptive restart and CEGAR-based solver for inverting cryptographic hash functions, Verified Software. Theories, Tools, and Experiments, 120-131 (2017), Cham: Springer, Cham
[14] Wang, J., Shen, H.T., Song, J., Ji, J.: Hashing for similarity search: A survey. arXiv preprint arXiv:1408.2927 (2014)
[15] Wang, J.; Zhang, T.; Sebe, N.; Shen, HT, A survey on learning to hash, IEEE Trans. Pattern Anal. Mach. intell., 40, 4, 769-790 (2017)
[16] Weaver, S., Heule, M.: Constructing minimal perfect hash functions using sat technology. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 1668-1675 (2020)
[17] Weaver, SA; Ray, KJ; Marek, VW; Mayer, AJ; Walker, AK, Satisfiability-based set membership filters, J. Satisfiability Boolean Model. Comput., 8, 3-4, 129-148 (2012) · Zbl 1322.68187
[18] Wotzlaw, A., van der Grinten, A., Speckenmeyer, E.: Effectiveness of pre-and inprocessing for cdcl-based sat solving. arXiv preprint arXiv:1310.4756 (2013)
[19] Zhang, L.; Bacchus, F.; Walsh, T., On subsumption removal and on-the-fly CNF simplification, Theory and Applications of Satisfiability Testing, 482-489 (2005), Heidelberg: Springer, Heidelberg · Zbl 1128.68488
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.