{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,28]],"date-time":"2025-06-28T14:10:03Z","timestamp":1751119803068,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T00:00:00Z","timestamp":1512604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,12,7]]},"DOI":"10.1145\/3155133.3155167","type":"proceedings-article","created":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T13:26:53Z","timestamp":1512998813000},"page":"84-91","source":"Crossref","is-referenced-by-count":3,"title":["SAT Encodings of Finite-CSP Domains"],"prefix":"10.1145","author":[{"given":"Van-Hau","family":"Nguyen","sequence":"first","affiliation":[{"name":"Hung Yen University of Technology and Education, Vietnam"}]}],"member":"320","published-online":{"date-parts":[[2017,12,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_17"},{"volume-title":"AAAI\/IAAI","author":"Bacchus Fahiem","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","unstructured":"Olivier Bailleux. 2010. On the CNF Encoding of Cardinality Constraints and Beyond. CoRR abs\/1012.3853 (2010). Olivier Bailleux. 2010. On the CNF Encoding of Cardinality Constraints and Beyond. CoRR abs\/1012.3853 (2010)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_8"},{"volume-title":"Efficient SAT-Encoding of Linear CSP Constraints. In 13rd International Symposium on AI and Mathematics, ISAIM","year":"2014","author":"Barahona Pedro","key":"e_1_3_2_1_6_1"},{"volume-title":"CPAIOR (Lecture Notes in Computer Science)","author":"Barahona Pedro","key":"e_1_3_2_1_7_1"},{"volume-title":"Proceedings of SAT Competition","year":"2013","author":"Biere Armin","key":"e_1_3_2_1_8_1"},{"volume":"2","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence","author":"James","key":"e_1_3_2_1_9_1"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_11_1","unstructured":"Johan de Kleer. 1989. A Comparison of ATMS and CSP Techniques. In IJCAI. 290--296. Johan de Kleer. 1989. A Comparison of ATMS and CSP Techniques. In IJCAI. 290--296."},{"key":"e_1_3_2_1_12_1","unstructured":"Michael D. Ernst Todd D. Millstein and Daniel S. Weld. 1997. Automatic SAT-Compilation of Planning Problems. In IJCAI-97. Morgan Kaufmann 1169--1176. Michael D. Ernst Todd D. Millstein and Daniel S. Weld. 1997. Automatic SAT-Compilation of Planning Problems. In IJCAI-97. Morgan Kaufmann 1169--1176."},{"volume-title":"Some Slow. In Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation.","author":"Alan","key":"e_1_3_2_1_13_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Alan M. Frisch Timothy J. Peugniez Anthony J. Doggett and Peter W. Nightingale. 2005. Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. J. Autom. Reason. 35 (October 2005) 143--179. Issue 1--3. 10.1007\/s10817-005-9011-0 Alan M. Frisch Timothy J. Peugniez Anthony J. Doggett and Peter W. Nightingale. 2005. Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. J. Autom. Reason. 35 (October 2005) 143--179. Issue 1--3. 10.1007\/s10817-005-9011-0","DOI":"10.1007\/s10817-005-9011-0"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04238-6_50"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Allen Van Gelder. 2008. Another Look at Graph Coloring via Propositional Satisfiability. Discrete Appl. Math. 156 (January 2008) 230--243. Issue 2. 10.1016\/j.dam.2006.07.016 Allen Van Gelder. 2008. Another Look at Graph Coloring via Propositional Satisfiability. Discrete Appl. Math. 156 (January 2008) 230--243. Issue 2. 10.1016\/j.dam.2006.07.016","DOI":"10.1016\/j.dam.2006.07.016"},{"volume-title":"Proceedings 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, Alan M. Frisch and Ian Miguel (Eds.). Springer, 95--110","year":"2004","author":"Gent Ian","key":"e_1_3_2_1_17_1"},{"volume-title":"Proceedings of the 15th Eureopean Conference on Artificial Intelligence, ECAI'2002","year":"2002","author":"Gent Ian P.","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/3171837.3171974"},{"key":"e_1_3_2_1_20_1","unstructured":"Holger H. Hoos. 1999. SAT-Encodings Search Space Structure and Local Search Performance. In IJCAI Thomas Dean (Ed.). Morgan Kaufmann 296--303. Holger H. Hoos. 1999. SAT-Encodings Search Space Structure and Local Search Performance. In IJCAI Thomas Dean (Ed.). Morgan Kaufmann 296--303."},{"key":"e_1_3_2_1_21_1","first-page":"253","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"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387915.2387924"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90009-O"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Henry Kautz and Bart Selman. 2007. The State of SAT. Discrete Appl. Math. 155 (June 2007) 1514--1524. 10.1016\/j.dam.2006.10.004 Henry Kautz and Bart Selman. 2007. The State of SAT. Discrete Appl. Math. 155 (June 2007) 1514--1524. 10.1016\/j.dam.2006.10.004","DOI":"10.1016\/j.dam.2006.10.004"},{"key":"e_1_3_2_1_25_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--73. 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--73."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068412000130"},{"key":"e_1_3_2_1_27_1","unstructured":"Van-Hau Nguyen. 2015. SAT Encodings of Finite CSPs. In Dresden University of Technology. 181. Van-Hau Nguyen. 2015. SAT Encodings of Finite CSPs. In Dresden University of Technology. 181."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2833258.2833293"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676585.2676605"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Van-Hau Nguyen Miroslav N. Velev and Pedro Barahona. 2013. Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. In ICTAI. IEEE 1028--1035. 10.1109\/ICTAI.2013.154 Van-Hau Nguyen Miroslav N. Velev and Pedro Barahona. 2013. Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. In ICTAI. IEEE 1028--1035. 10.1109\/ICTAI.2013.154","DOI":"10.1109\/ICTAI.2013.154"},{"volume-title":"SAT (Lecture Notes in Computer Science)","author":"Petke Justyna","key":"e_1_3_2_1_31_1"},{"key":"e_1_3_2_1_32_1","unstructured":"Francesca Rossi Peter van Beek and Toby Walsh. 2006. Handbook of Constraint Programming (Foundations of Artificial Intelligence). Elsevier Science Inc. New York NY USA. Francesca Rossi Peter van Beek and Toby Walsh. 2006. Handbook of Constraint Programming (Foundations of Artificial Intelligence). Elsevier Science Inc. New York NY USA."},{"key":"e_1_3_2_1_33_1","unstructured":"Bart Selman Hector J. Levesque and David G. Mitchell. 1992. A New Method for Solving Hard Satisfiability Problems. In AAAI William R. Swartout (Ed.). AAAI Press \/ The MIT Press 440--446. Bart Selman Hector J. Levesque and David G. Mitchell. 1992. A New Method for Solving Hard Satisfiability Problems. In AAAI William R. Swartout (Ed.). AAAI Press \/ The MIT Press 440--446."},{"volume-title":"13th International Conference, CP 2007. 483--497","year":"2007","author":"Silva Jo\u00e3o Marques","key":"e_1_3_2_1_34_1"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_3_2_1_36_1","unstructured":"\u00c9ric Taillard. {n. d.}. http:\/\/mistic.heig-vd.ch\/taillard\/problemes.dir\/ordonnancement.dir\/ordonnancement.html. ({n. d.}). \u00c9ric Taillard. {n. d.}. http:\/\/mistic.heig-vd.ch\/taillard\/problemes.dir\/ordonnancement.dir\/ordonnancement.html. ({n. d.})."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9061-0"},{"volume-title":"SAT (Lecture Notes in Computer Science)","author":"Tanjo Tomoya","key":"e_1_3_2_1_38_1"},{"key":"e_1_3_2_1_39_1","unstructured":"Michael Trick. {n. d.}. DIMACS Graph-Coloring Problems. http:\/\/mat.gsia.cmu.edu\/COLOR\/instances.html. ({n. d.}). {Online; accessed 24-April-2014}. Michael Trick. {n. d.}. DIMACS Graph-Coloring Problems. http:\/\/mat.gsia.cmu.edu\/COLOR\/instances.html. ({n. d.}). {Online; accessed 24-April-2014}."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Miroslav N. Velev. 2007. Exploiting Hierarchy and Structure to Efficiently Solve Graph Coloring as SAT. In ICCAD Georges G. E. Gielen (Ed.). IEEE 135--142. Miroslav N. Velev. 2007. Exploiting Hierarchy and Structure to Efficiently Solve Graph Coloring as SAT. In ICCAD Georges G. E. Gielen (Ed.). IEEE 135--142.","DOI":"10.1109\/ICCAD.2007.4397256"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726638"}],"event":{"name":"SoICT 2017: The Eighth International Symposium on Information and Communication Technology","sponsor":["SOICT School of Information and Communication Technology - HUST","NAFOSTED The National Foundation for Science and Technology Development"],"location":"Nha Trang City Viet Nam","acronym":"SoICT 2017"},"container-title":["Proceedings of the Eighth International Symposium on Information and Communication Technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3155133.3155167","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3155133.3155167","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,28]],"date-time":"2025-06-28T13:35:12Z","timestamp":1751117712000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3155133.3155167"}},"subtitle":["A Survey"],"short-title":[],"issued":{"date-parts":[[2017,12,7]]},"references-count":41,"alternative-id":["10.1145\/3155133.3155167","10.1145\/3155133"],"URL":"https:\/\/doi.org\/10.1145\/3155133.3155167","relation":{},"subject":[],"published":{"date-parts":[[2017,12,7]]}}}