{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,9]],"date-time":"2025-11-09T07:48:47Z","timestamp":1762674527806,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,17]],"date-time":"2020-09-17T00:00:00Z","timestamp":1600300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["NRF-2017R1A2B4012559"],"award-info":[{"award-number":["NRF-2017R1A2B4012559"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,17]]},"DOI":"10.1145\/3426020.3426170","type":"proceedings-article","created":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T22:52:57Z","timestamp":1636066377000},"page":"470-475","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Empirical Study on SAT-Encodings of the At-Most-One Constraint"],"prefix":"10.1145","author":[{"given":"Van-Hau","family":"Nguyen","sequence":"first","affiliation":[{"name":"Hung Yen University of Technology and Education, Vietnam"}]},{"given":"Van-Quyet","family":"Nguyen","sequence":"additional","affiliation":[{"name":"Hung Yen University of Technology and Education, Vietnam"}]},{"given":"Kyungbaek","family":"Kim","sequence":"additional","affiliation":[{"name":"Chonnam National University, S. Korea"}]},{"given":"Pedro","family":"Barahona","sequence":"additional","affiliation":[{"name":"New University of Lisbon, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2021,11,4]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Importance of Variables Semantic in CNF Encoding of Cardinality Constraints. In SARA 2009","author":"Alban Grastien Anbulagan","year":"2009","unstructured":"Anbulagan and Alban Grastien . 2009 . Importance of Variables Semantic in CNF Encoding of Cardinality Constraints. In SARA 2009 , Lake Arrowhead, California, USA , 8-10 August 2009, Vadim Bulitko and J. Christopher Beck (Eds.). AAAI. Anbulagan and Alban Grastien. 2009. Importance of Variables Semantic in CNF Encoding of Cardinality Constraints. In SARA 2009, Lake Arrowhead, California, USA, 8-10 August 2009, Vadim Bulitko and J. Christopher Beck (Eds.). AAAI."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2010.17"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-010-9105-0"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_19"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07046-9_18"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_30"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of SAT Competition","author":"Biere Armin","year":"2013","unstructured":"Armin Biere . 2013 . Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013 . In Proceedings of SAT Competition 2013, Anton Belov Adrian Balint, Marjin Heule, and Matti J\u00e4rvisalo (Eds.). 51\u201352. Armin Biere. 2013. Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In Proceedings of SAT Competition 2013, Anton Belov Adrian Balint, Marjin Heule, and Matti J\u00e4rvisalo (Eds.). 51\u201352."},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation.","author":"Chen Jing-Chao","year":"2010","unstructured":"Jing-Chao Chen . 2010 . A new SAT Encoding of the At-Most-One Constraint . In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation. Jing-Chao Chen. 2010. A new SAT Encoding of the At-Most-One Constraint. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1623755.1623800"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190014"},{"volume-title":"Some Slow. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation.","author":"Alan","key":"e_1_3_2_1_14_1","unstructured":"Alan M. Frisch and Paul A. Giannoros. 2010. SAT Encodings of the At-Most-k Constraint. Some Old, Some New, Some Fast , Some Slow. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation. Alan M. Frisch and Paul A. Giannoros. 2010. SAT Encodings of the At-Most-k Constraint. Some Old, Some New, Some Fast, Some Slow. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9011-0"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04238-6_50"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3000905.3000932"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_13"},{"key":"e_1_3_2_1_19_1","unstructured":"Brahim Hnich Ian Miguel Ian P. Gent and Toby Walsh. [n. d.]. CSPLib is a Library of Test Problems for Constraint Solvers. http:\/\/www.csplib.org\/. ([n. d.]). [Online; accessed 24-April-2020].  Brahim Hnich Ian Miguel Ian P. Gent and Toby Walsh. [n. d.]. CSPLib is a Library of Test Problems for Constraint Solvers. http:\/\/www.csplib.org\/. ([n. d.]). [Online; accessed 24-April-2020]."},{"volume-title":"Proc. INFOCOM-5. 208\u2013212","author":"H\u00f6lldobler S.","key":"e_1_3_2_1_20_1","unstructured":"S. H\u00f6lldobler , N. Manthey , VH. Nguyen , and P. Steinke . 2012. Solving Hidokus Using SAT Solvers . In Proc. INFOCOM-5. 208\u2013212 . ISSN 2219-293X. S. H\u00f6lldobler, N. Manthey, VH. Nguyen, and P. Steinke. 2012. Solving Hidokus Using SAT Solvers. In Proc. INFOCOM-5. 208\u2013212. ISSN 2219-293X."},{"key":"e_1_3_2_1_21_1","volume-title":"Julian Stecklina, and Peter Steinke.","author":"H\u00f6lldobler Steffen","year":"2011","unstructured":"Steffen H\u00f6lldobler , Norbert Manthey , Van Hau Nguyen , Julian Stecklina, and Peter Steinke. 2011 . Modern Parallel SAT-Solvers. Technical Report. TU Dresden, Knowledge Representation and Reasoning . Steffen H\u00f6lldobler, Norbert Manthey, Van Hau Nguyen, Julian Stecklina, and Peter Steinke. 2011. Modern Parallel SAT-Solvers. Technical Report. TU Dresden, Knowledge Representation and Reasoning."},{"key":"e_1_3_2_1_23_1","first-page":"258","volume-title":"SAT-Variable Complexity of Hard Combinatorial Problems. In In Proceedings of the World Computer Congress of the IFIP","author":"Iwama Kazuo","year":"1994","unstructured":"Kazuo Iwama and Shuichi Miyazaki . 1994 . SAT-Variable Complexity of Hard Combinatorial Problems. In In Proceedings of the World Computer Congress of the IFIP , pages 253\u2013 258 (Volume 1). Elsevier Science B.V. 253\u2013258. Kazuo Iwama and Shuichi Miyazaki. 1994. SAT-Variable Complexity of Hard Combinatorial Problems. In In Proceedings of the World Computer Congress of the IFIP, pages 253\u2013258 (Volume 1). Elsevier Science B.V. 253\u2013258."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.10.004"},{"key":"e_1_3_2_1_25_1","volume-title":"the Fourth Workshop on Constraint in Formal Verification(CFV).","author":"Klieber Will","year":"2007","unstructured":"Will Klieber and Gihwon Kwon . 2007 . Efficient CNF Encoding for Selecting 1 from N Objects . In the Fourth Workshop on Constraint in Formal Verification(CFV). Will Klieber and Gihwon Kwon. 2007. Efficient CNF Encoding for Selecting 1 from N Objects. In the Fourth Workshop on Constraint in Formal Verification(CFV)."},{"volume-title":"The SAT Solver RISS3G at SC 2013","author":"Manthey Norbert","key":"e_1_3_2_1_26_1","unstructured":"Norbert Manthey . 2013. The SAT Solver RISS3G at SC 2013 (Department of Computer Science Series of Publications B), A. Balint, A. Belov, M. J.H. Heule, and M. J\u00e4rvisalo (Eds.), Vol. B-2013- 1 . University of Helsinki , Helsinki, Finland, 72\u201373. Norbert Manthey. 2013. The SAT Solver RISS3G at SC 2013 (Department of Computer Science Series of Publications B), A. Balint, A. Belov, M. J.H. Heule, and M. J\u00e4rvisalo (Eds.), Vol. B-2013-1. University of Helsinki, Helsinki, Finland, 72\u201373."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2011.54"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_29_1","volume-title":"Algebraic Fault Attack on SHA Hash Functions Using Programmatic SAT Solvers. In CP2018","author":"Nejati Saeed","year":"2018","unstructured":"Saeed Nejati , Jan Hor\u00e1\u010dek , Catherine Gebotys , and Vijay Ganesh . 2018 . Algebraic Fault Attack on SHA Hash Functions Using Programmatic SAT Solvers. In CP2018 , John Hooker (Ed.). Springer, Cham, 737\u2013754. Saeed Nejati, Jan Hor\u00e1\u010dek, Catherine Gebotys, and Vijay Ganesh. 2018. Algebraic Fault Attack on SHA Hash Functions Using Programmatic SAT Solvers. In CP2018, John Hooker (Ed.). Springer, Cham, 737\u2013754."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3155133.3155167"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676585.2676605"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2833258.2833293"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(02)00410-9"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_38"},{"volume-title":"Finding Large Cliques using SAT Local Search","author":"Prestwich Steve David","key":"e_1_3_2_1_35_1","unstructured":"Steve David Prestwich . 2007. Finding Large Cliques using SAT Local Search , B. OSullivan F. Benhamou, N. Jussien (Ed.), Vol. Trends in Constraint Programming. ISTE, 273\u2013 278 . Steve David Prestwich. 2007. Finding Large Cliques using SAT Local Search, B. OSullivan F. Benhamou, N. Jussien (Ed.), Vol. Trends in Constraint Programming. ISTE, 273\u2013278."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1771668.1771706"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9061-0"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726638"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00144-6"}],"event":{"name":"SMA 2020: The 9th International Conference on Smart Media and Applications","acronym":"SMA 2020","location":"Jeju Republic of Korea"},"container-title":["The 9th International Conference on Smart Media and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3426020.3426170","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3426020.3426170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:33Z","timestamp":1750195893000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3426020.3426170"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,17]]},"references-count":39,"alternative-id":["10.1145\/3426020.3426170","10.1145\/3426020"],"URL":"https:\/\/doi.org\/10.1145\/3426020.3426170","relation":{},"subject":[],"published":{"date-parts":[[2020,9,17]]},"assertion":[{"value":"2021-11-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}