{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:41:57Z","timestamp":1742942517156,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572456"},{"type":"electronic","value":"9783031572463"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present , a powerful local search SAT solver that effectively solves hard combinatorial problems. Its unique approach of transferring clause weights in local minima enhances its efficiency in solving problem instances. Since it is implemented on top of , benefits from practical techniques such as restart strategies and thread parallelization. Our implementation includes a parallel version that shares data structures across threads, leading to a significant reduction in memory usage. Our experiments demonstrate that outperforms similar solvers on a vast set of SAT competition benchmarks. Notably, with the parallel configuration of , we improve lower bounds for several van der Waerden numbers.<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_3","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"34-42","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["TaSSAT: Transfer and Share SAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8429-2108","authenticated-orcid":false,"given":"Md Solimul","family":"Chowdhury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3588-4873","authenticated-orcid":false,"given":"Cayden R.","family":"Codel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"3_CR1","unstructured":"SAT Competition 2022. https:\/\/satcompetition.github.io\/2022\/downloads.html, 2022."},{"key":"3_CR2","unstructured":"Cesare\u00a0Tinelli Aaron\u00a0Stump, Geoff\u00a0Sutcliffe. StarExec. https:\/\/www.starexec.org\/starexec\/public\/about.jsp, 2013."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Tanbir Ahmed, Oliver Kullmann, and Hunter\u00a0S. Snevily. On the van der Waerden numbers w(2; 3, t). Discrete Applied Mathematics, 174:27\u201351, 2014.","DOI":"10.1016\/j.dam.2014.05.007"},{"key":"3_CR4","unstructured":"Adrian Balint. Engineering stochastic local search for the satisfiability problem. PhD thesis, University of Ulm, 2014."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Adrian Balint, Armin Biere, Andreas Fr\u00f6hlich, and Uwe Sch\u00f6ning. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In Proceedings of SAT-2014, pages 302\u2013316, 2014.","DOI":"10.1007\/978-3-319-09284-3_23"},{"key":"3_CR6","unstructured":"Armin Biere. YalSAT: Yet Another Local Search Solver. http:\/\/fmv.jku.at\/yalsat\/, 2010."},{"key":"3_CR7","unstructured":"Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. CADICAL, KISSAT, PARACOOBA, PLINGELING and TREENGELING entering the SAT Competition. In Proceedings of SAT Competition, pages 50\u201353, 2020."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Shawn\u00a0T. Brown, Paola Buitrago, Edward Hanna, Sergiu Sanielevici, Robin Scibek, and Nicholas\u00a0A. Nystrom. Bridges-2: A platform for rapidly-evolving and data intensive research. In Association for Computing Machinery, New York, NY, USA, pages 1\u20134, 2021.","DOI":"10.1145\/3437359.3465593"},{"key":"3_CR9","unstructured":"Md\u00a0Solimul Chowdhury, Cayden Codel, and Marijn Heule. Artifact for TaSSAT: A stochastic local search solver for SAT."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Md\u00a0Solimul Chowdhury, Cayden\u00a0R. Codel, and Marijn\u00a0J.H. Heule. A linear weight transfer rule for local search. In NASA Formal Methods, 2023.","DOI":"10.1007\/978-3-031-33170-1_27"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Stephen\u00a0A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151\u2013158, 1971.","DOI":"10.1145\/800157.805047"},{"key":"3_CR12","unstructured":"Marijn J.\u00a0H. Heule. Solving edge-matching problems with satisfiability solvers. In SAT 2009 competitive events booklet, pages 69\u201382, 2009."},{"key":"3_CR13","unstructured":"Marijn J.\u00a0H. Heule, Anthony Karahalios, and Willem-Jan van Hoeve. From cliques to colorings and back again. In Proceedings of CP-2022, pages 26:1\u201326:10, 2022."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Marijn J.\u00a0H. Heule, Manuel Kauers, and Martina Seidl. New ways to multiply 3x3-matrices. J. Symb. Comput., 104:899\u2013916, 2019.","DOI":"10.1016\/j.jsc.2020.10.003"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Marijn J.\u00a0H. Heule and Oliver Kullmann. The science of brute force. Commun. ACM, 60(8):70\u201379, 2017.","DOI":"10.1145\/3107239"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Abdelraouf Ishtaiwi, John Thornton, Abdul Sattar, and Duc\u00a0Nghia Pham. Neighbourhood clause weight redistribution in local search for SAT. In Proceedings of CP-2005, Lecture Notes in Computer Science, pages 772\u2013776, 2005.","DOI":"10.1007\/11564751_62"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Proceedings of SAT-2009, pages 244\u2013257, 2009.","DOI":"10.1007\/978-3-642-02777-2_24"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T16:14:37Z","timestamp":1731687277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}