{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:51:52Z","timestamp":1742979112151,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_7","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"82-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Hash-Based Preprocessing and Inprocessing Techniques in SAT Solvers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0525-4344","authenticated-orcid":false,"given":"Henrik","family":"Cao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bakhtiari, S., Safavi-Naini, R., Pieprzyk, J., et al.: Cryptographic hash functions: A survey. Technical Report, Citeseer (1995)","DOI":"10.1007\/BFb0032359"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Balyo, T., Froleyks, N., Heule, M.J., Iser, M., J\u00e4rvisalo, M., Suda, M.: Proceedings of sat competition 2020: Solver and benchmark descriptions (2020)","DOI":"10.1016\/j.artint.2021.103572"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bayardo, R.J., Panda, B.: Fast algorithms for finding extremal sets. In: Proceedings of the 2011 SIAM International Conference on Data Mining, pp. 25\u201334. SIAM (2011)","DOI":"10.1137\/1.9781611972818.3"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_5"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-02777-2_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"H Han","year":"2009","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_21"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11559306_11","volume-title":"Frontiers of Combining Systems","author":"D Jovanovi\u0107","year":"2005","unstructured":"Jovanovi\u0107, D., Jani\u010di\u0107, P.: Logical analysis of hash functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 200\u2013215. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_11"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-66263-3_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"T Korhonen","year":"2017","unstructured":"Korhonen, T., Berg, J., Saikko, P., J\u00e4rvisalo, M.: MaxPre: an extended MaxSAT preprocessor. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 449\u2013456. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_28"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013921. IEEE (2012)","DOI":"10.1109\/ICTAI.2012.128"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11935308_32","volume-title":"Information and Communications Security","author":"M de Mare","year":"2006","unstructured":"de Mare, M., Wright, R.N.: Secure set membership using 3Sat. In: Ning, P., Qing, S., Li, N. (eds.) ICICS 2006. LNCS, vol. 4307, pp. 452\u2013468. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11935308_32"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11814948_13","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I Mironov","year":"2006","unstructured":"Mironov, I., Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 102\u2013115. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_13"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-319-72308-2_8","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"S Nejati","year":"2017","unstructured":"Nejati, S., Liang, J.H., Gebotys, C., Czarnecki, K., Ganesh, V.: Adaptive restart and CEGAR-based solver for inverting cryptographic hash functions. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 120\u2013131. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_8"},{"key":"7_CR14","unstructured":"Wang, J., Shen, H.T., Song, J., Ji, J.: Hashing for similarity search: A survey. arXiv preprint arXiv:1408.2927 (2014)"},{"issue":"4","key":"7_CR15","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1109\/TPAMI.2017.2699960","volume":"40","author":"J Wang","year":"2017","unstructured":"Wang, J., Zhang, T., Sebe, N., Shen, H.T., et al.: A survey on learning to hash. IEEE Trans. Pattern Anal. Mach. intell. 40(4), 769\u2013790 (2017)","journal-title":"IEEE Trans. Pattern Anal. Mach. intell."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"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\u20131675 (2020)","DOI":"10.1609\/aaai.v34i02.5529"},{"issue":"3\u20134","key":"7_CR17","first-page":"129","volume":"8","author":"SA Weaver","year":"2012","unstructured":"Weaver, S.A., Ray, K.J., Marek, V.W., Mayer, A.J., Walker, A.K.: Satisfiability-based set membership filters. J. Satisfiability Boolean Model. Comput. 8(3\u20134), 129\u2013148 (2012)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"7_CR18","unstructured":"Wotzlaw, A., van der Grinten, A., Speckenmeyer, E.: Effectiveness of pre-and inprocessing for cdcl-based sat solving. arXiv preprint arXiv:1310.4756 (2013)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/11499107_42","volume-title":"Theory and Applications of Satisfiability Testing","author":"L Zhang","year":"2005","unstructured":"Zhang, L.: On subsumption removal and on-the-fly CNF simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 482\u2013489. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_42"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:38:08Z","timestamp":1672652288000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}