{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:48:21Z","timestamp":1743140901106,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031249495"},{"type":"electronic","value":"9783031249501"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-24950-1_12","type":"book-chapter","created":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T14:03:19Z","timestamp":1673877799000},"page":"252-266","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["CosySEL: Improving SAT Solving Using Local Symmetries"],"prefix":"10.1007","author":[{"given":"Sabrine","family":"Saouli","sequence":"first","affiliation":[]},{"given":"Souheib","family":"Baarir","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Dutheillet","sequence":"additional","affiliation":[]},{"given":"Jo","family":"Devriendt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,1,17]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult sat instances in the presence of symmetry. In: Proceedings 2002 Design Automation Conference (IEEE Cat. No. 02CH37324) pp. 731\u2013736. IEEE (2002)","DOI":"10.1109\/DAC.2002.1012719"},{"issue":"5","key":"12_CR2","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"FA Aloul","year":"2006","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Comput. 55(5), 549\u2013558 (2006)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"12_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2898435","volume":"17","author":"A Atserias","year":"2016","unstructured":"Atserias, A., Lauria, M., Nordstr\u00f6m, J.: Narrow proofs may be maximally long. ACM Trans. Comput. Logic (TOCL) 17(3), 1\u201330 (2016)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1017\/jsl.2014.56","volume":"80","author":"A Atserias","year":"2015","unstructured":"Atserias, A., M\u00fcller, M., Oliva, S.: Lower bounds for DNF-refutations of a relativized weak pigeonhole principle. J. Symbolic Logic 80(2), 450\u2013476 (2015)","journal-title":"J. Symbolic Logic"},{"key":"12_CR5","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 399\u2013404 (2009)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Benhamou, B., Nabhani, T., Ostrowski, R., Sa\u00efdi, M.R.: Enhancing clause learning by symmetry in sat solvers. In: 2010 22nd IEEE International Conference on Tools with Artificial Intelligence, vol. 1, pp. 329\u2013335. IEEE (2010)","DOI":"10.1109\/ICTAI.2010.55"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"12_CR8","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)"},{"key":"12_CR9","first-page":"15","volume":"2021","author":"MS Cherif","year":"2021","unstructured":"Cherif, M.S., Habet, D., Terrioux, C.: Kissat MAB: combining VSIDS and CHB through multi-armed bandit. SAT Competition 2021, 15 (2021)","journal-title":"SAT Competition"},{"issue":"1996","key":"12_CR10","first-page":"148","volume":"96","author":"J Crawford","year":"1996","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. KR 96(1996), 148\u2013159 (1996)","journal-title":"KR"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-66263-3_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"J Devriendt","year":"2017","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M.: Symmetric explanation learning: effective dynamic symmetry handling for SAT. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 83\u2013100. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_6"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Devriendt, J., Bogaerts, B., De Cat, B., Denecker, M., Mears, C.: Symmetry propagation: Improved dynamic symmetry breaking in SAT. In: 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, vol. 1, pp. 49\u201356. IEEE (2012)","DOI":"10.1109\/ICTAI.2012.16"},{"key":"12_CR14","first-page":"67","volume":"2016","author":"J Elffers","year":"2016","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Documentation of some combinatorial benchmarks. Proc. SAT Competition 2016, 67\u201369 (2016)","journal-title":"Proc. SAT Competition"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/3-540-61511-3_115","volume-title":"Automated Deduction \u2014 Cade-13","author":"F Giunchiglia","year":"1996","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures\u2014the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 583\u2013597. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_115"},{"issue":"1","key":"12_CR16","first-page":"89","volume":"33","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Le Berre, D., Roussel, O., Simon, L.: The international sat solver competitions. AI Mag. 33(1), 89\u201392 (2012)","journal-title":"AI Mag."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R. (eds.) Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics, pp. 135\u2013149. SIAM (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-14186-7_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"H Katebi","year":"2010","unstructured":"Katebi, H., Sakallah, K.A., Markov, I.L.: Symmetry and satisfiability: an update. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 113\u2013127. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_11"},{"key":"12_CR19","unstructured":"Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: ECAI, vol. 92, pp. 359\u2013363 (1992)"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1023\/B:AMAI.0000018578.92398.10","volume":"41","author":"EM Luks","year":"2004","unstructured":"Luks, E.M., Roy, A.: The complexity of symmetry-breaking formulas. Ann. Math. Artif. Intell. 41(1), 19\u201345 (2004)","journal-title":"Ann. Math. Artif. Intell."},{"key":"12_CR21","first-page":"67","volume":"2018","author":"N Manthey","year":"2018","unstructured":"Manthey, N., Heusser, J.: Satcoin-bitcoin mining via SAT. SAT Competition 2018, 67 (2018)","journal-title":"SAT Competition"},{"issue":"1","key":"12_CR22","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1006326723002","volume":"24","author":"F Massacci","year":"2000","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a sat problem. J. Autom. Reasoning 24(1), 165\u2013203 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-89960-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Metin","year":"2018","unstructured":"Metin, H., Baarir, S., Colange, M., Kordon, F.: CDCLSym: introducing effective symmetry breaking in SAT solving. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 99\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_6"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-030-20652-9_21","volume-title":"NASA Formal Methods","author":"H Metin","year":"2019","unstructured":"Metin, H., Baarir, S., Kordon, F.: Composing symmetry propagation and effective symmetry breaking for SAT solving. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 316\u2013332. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_21"},{"issue":"4","key":"12_CR25","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-008-9060-1","volume":"14","author":"A Sabharwal","year":"2009","unstructured":"Sabharwal, A.: Symchaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints 14(4), 478\u2013505 (2009)","journal-title":"Constraints"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/10722167_36","volume-title":"Computer Aided Verification","author":"O Shtrichman","year":"2000","unstructured":"Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480\u2013494. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_36"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58\u201370. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44798-9_4"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/11513988_12","volume-title":"Computer Aided Verification","author":"D Tang","year":"2005","unstructured":"Tang, D., Malik, S., Gupta, A., Ip, C.N.: Symmetry reduction in SAT-based model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 125\u2013138. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_12"},{"issue":"03","key":"12_CR29","doi-asserted-by":"publisher","first-page":"1950011","DOI":"10.1142\/S0218213019500118","volume":"28","author":"RK Tchinda","year":"2019","unstructured":"Tchinda, R.K., Tayou Djamegni, C.: Enhancing static symmetry breaking with dynamic symmetry handling in CDCL SAT solvers. Int. J. Artif. Intell. Tools 28(03), 1950011 (2019)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"12_CR30","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of reasoning, pp. 466\u2013483. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Wang, C., Jin, H., Hachtel, G.D., Somenzi, F.: Refining the SAT decision ordering for bounded model checking. In: Proceedings of the 41st Annual Design Automation Conference, pp. 535\u2013538 (2004)","DOI":"10.1145\/996566.996713"},{"key":"12_CR32","unstructured":"Zhang, X., Cai, S., Chen, Z.: Improving cdcl via local search. SAT Competition 2021, 42 (2021)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-24950-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T14:04:00Z","timestamp":1715695440000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-24950-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031249495","9783031249501"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-24950-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 January 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Boston, MA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2023","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":"vmcai2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/vmcai-2023.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"34","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":"17","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":"0","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":"50% - 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":"4","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)"}}]}}