{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T17:18:07Z","timestamp":1770484687328,"version":"3.49.0"},"publisher-location":"New York, New York, USA","reference-count":62,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1145\/2676585.2676605","type":"proceedings-article","created":{"date-parts":[[2015,1,16]],"date-time":"2015-01-16T19:18:59Z","timestamp":1421435939000},"page":"65-74","source":"Crossref","is-referenced-by-count":5,"title":["Solving the all-interval series problem"],"prefix":"10.1145","author":[{"given":"Van-Hau","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mai Thai","family":"Son","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"key-10.1145\/2676585.2676605-1","unstructured":"MiniZinc Challenge 2013 Results. https:\/\/www.minizinc.org\/challenge2013\/results2013.html."},{"key":"key-10.1145\/2676585.2676605-2","unstructured":"The International SAT Competitions. http:\/\/www.satcompetition.org\/."},{"key":"key-10.1145\/2676585.2676605-3","doi-asserted-by":"crossref","unstructured":"F. A. Aloul. Symmetry in Boolean Satisfiability.Symmetry, 2(2): 1121--1134, 2010.","DOI":"10.3390\/sym2021121"},{"key":"key-10.1145\/2676585.2676605-4","unstructured":"F. A. Aloul, K. A. Sakallah, and I. L. Markov. Efficient Symmetry Breaking for Boolean Satisfiability. InIJCAI, pages 271--276, 2003."},{"key":"key-10.1145\/2676585.2676605-5","doi-asserted-by":"crossref","unstructured":"T. Alsinet, R. Béjar, A. Cabiscol, C. Fernández, and F. Manyà. Minimal and Redundant SAT Encodings for the All-Interval-Series Problem. InTopics in Artificial Intelligence, 5th Catalonian Conference on AI (CCIA), volume 2504 ofLecture Notes in Computer Science, pages 139--144, 2002.","DOI":"10.1007\/3-540-36079-4_12"},{"key":"key-10.1145\/2676585.2676605-6","doi-asserted-by":"crossref","unstructured":"M. Ankerst, M. M. Breunig, H.-P. Kriegel, and J. Sander. OPTICS: Ordering Points To Identify the Clustering Structure. InSIGMOD, pages 49--60, 1999.","DOI":"10.1145\/304181.304187"},{"key":"key-10.1145\/2676585.2676605-7","doi-asserted-by":"crossref","unstructured":"C. Ansótegui and F. Manyà. Mapping problems with finite-domain variables to problems with boolean variables. InSAT (Selected Papers), volume 3542 ofLecture Notes in Computer Science, pages 1--15. Springer, 2004.","DOI":"10.1007\/11527695_1"},{"key":"key-10.1145\/2676585.2676605-8","unstructured":"F. Azevedo and V.-H. Nguyen. Extra Constraints for the Social Golfers Problem. In13th International Conference on Logic for Programming Artificial Intelligence and Reasoning- LPAR 2006, Short Papers Proceedings, 2006."},{"key":"key-10.1145\/2676585.2676605-9","unstructured":"F. Azevedo and V.-H. Nguyen. Symmetry Breaking and Extra Constraints for the Social Golfers Problem. InInternational Symmetry Conference (ISC 2007), Short Papers Proceedings, 2007."},{"key":"key-10.1145\/2676585.2676605-10","doi-asserted-by":"crossref","unstructured":"O. Bailleux and Y. Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. In F. Rossi, editor,CP, volume 2833 ofLecture Notes in Computer Science, pages 108--122. Springer, 2003.","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"key-10.1145\/2676585.2676605-11","unstructured":"P. Barahona, S. Hölldobler, and V. H. Nguyen. Translating the At-Most-One Constraint into SAT. InProc. Doctor Program. Uppsala University, Sweden, September 16--20, 2013."},{"key":"key-10.1145\/2676585.2676605-12","unstructured":"P. Barahona, S. Hölldobler, and V.-H. Nguyen. Efficient SAT-Encoding of Linear CSP Constraints. InISAIM, 2014."},{"key":"key-10.1145\/2676585.2676605-13","doi-asserted-by":"crossref","unstructured":"P. Barahona, S. Hölldobler, and V.-H. Nguyen. Representative Encodings to Translate Finite CSPs into SAT. In H. Simonis, editor,CPAIOR, volume 8451 ofLecture Notes in Computer Science, pages 251--267. Springer, 2014.","DOI":"10.1007\/978-3-319-07046-9_18"},{"key":"key-10.1145\/2676585.2676605-14","doi-asserted-by":"crossref","unstructured":"C. Bessiere, editor.Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, volume 4741 of Lecture Notes in Computer Science. Springer, 2007.","DOI":"10.1007\/978-3-540-74970-7"},{"key":"key-10.1145\/2676585.2676605-15","unstructured":"A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors.Handbook of Satisfiability, volume 185 ofFrontiers in Artificial Intelligence and Applications. IOS Press, 2009."},{"key":"key-10.1145\/2676585.2676605-16","doi-asserted-by":"crossref","unstructured":"C. Böhm, J. Feng, X. He, S. T. Mai, C. Plant, and J. Shao. A Novel Similarity Measure for Fiber Clustering using Longest Common Subsequence. InKDD Workshops, pages 1--9, 2011.","DOI":"10.1145\/2023582.2023584"},{"key":"key-10.1145\/2676585.2676605-17","unstructured":"J. M. Crawford and A. B. Baker. Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems. In B. Hayes-Roth and R. E. Korf, editors,Proceedings of the 12th National Conference on Artificial Intelligence, Volume 2, pages 1092--1097. AAAI Press \/ The MIT Press, 1994."},{"key":"key-10.1145\/2676585.2676605-18","unstructured":"J. M. Crawford, M. L. Ginsberg, E. M. Luks, and A. Roy. Symmetry-Breaking Predicates for Search Problems. InKR, pages 148--159, 1996."},{"key":"key-10.1145\/2676585.2676605-19","unstructured":"J. de Kleer. A Comparison of ATMS and CSP Techniques. InIJCAI, pages 290--296, 1989."},{"key":"key-10.1145\/2676585.2676605-20","unstructured":"M. Ester, H. Kriegel, J. Sander, and X. Xu. A Density-Based Algorithm for Discovering Clusters in Large Spatial Databases with Noise. InKDD, pages 226--231, 1996."},{"key":"key-10.1145\/2676585.2676605-21","doi-asserted-by":"crossref","unstructured":"T. Feydy and P. J. Stuckey. Lazy clause generation reengineered. In I. P. Gent, editor,CP, volume 5732 ofLecture Notes in Computer Science, pages 352--366. Springer, 2009.","DOI":"10.1007\/978-3-642-04244-7_29"},{"key":"key-10.1145\/2676585.2676605-22","unstructured":"A. M. Frisch and P. A. Giannoros. SAT Encodings of the At-Most-k Constraint. Some Old, Some New, Some Fast, Some Slow. InProc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, 2010."},{"key":"key-10.1145\/2676585.2676605-23","doi-asserted-by":"crossref","unstructured":"M. Gavanelli. The Log-Support Encoding of CSP into SAT. In Bessiere [14], pages 815--822.","DOI":"10.1007\/978-3-540-74970-7_59"},{"key":"key-10.1145\/2676585.2676605-24","doi-asserted-by":"crossref","unstructured":"M. Gebser, B. Kaufmann, and T. Schaub. The Conflict-Driven Answer Set Solver clasp: Progress Report. In E. Erdem, F. Lin, and T. Schaub, editors,LPNMR, volume 5753 ofLecture Notes in Computer Science, pages 509--514. Springer, 2009.","DOI":"10.1007\/978-3-642-04238-6_50"},{"key":"key-10.1145\/2676585.2676605-25","unstructured":"I. P. Gent. Arc Consistency in SAT. In F. van Harmelen, editor,Proceedings of the 15th Eureopean Conference on Artificial Intelligence, ECAI'2002, pages 121--125. IOS Press, 2002."},{"key":"key-10.1145\/2676585.2676605-26","doi-asserted-by":"crossref","unstructured":"I. P. Gent, T. Kelsey, S. A. Linton, I. Mcdonald, I. Miguel, and B. M. Smith. Conditional Symmetry Breaking. InPrinciples and Practice of Constraint Programming - CP 2005, LNCS 3709, pages 256--270. Springer, 2005.","DOI":"10.1007\/11564751_21"},{"key":"key-10.1145\/2676585.2676605-27","unstructured":"I. P. Gent, I. McDonald, and B. M. Smith. Conditional Symmetry in the All-Interval Series Problem. InProceedings of the Third International Workshop on Symmetry in Constraint Satisfaction Problems, pages 55--65, 2003."},{"key":"key-10.1145\/2676585.2676605-28","doi-asserted-by":"crossref","unstructured":"I. P. Gent, K. E. Petrie, and J.-F. Puget. Symmetry in Constraint Programming. InHandbook of Constraint Programming, volume 2, chapter 10, pages 329--376. Elsevier, 2006.","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"key-10.1145\/2676585.2676605-29","doi-asserted-by":"crossref","unstructured":"I. P. Gent and T. Walsh. CSPLib: A Benchmark Library for Constraints. InCP, pages 480--481, 1999.","DOI":"10.1007\/978-3-540-48085-3_36"},{"key":"key-10.1145\/2676585.2676605-30","doi-asserted-by":"crossref","unstructured":"S. Gilpin and I. Davidson. Incorporating SAT Solvers into Hierarchical Clustering Algorithms: An Efficient and Flexible Approach. InKDD, pages 1136--1144, 2011.","DOI":"10.1145\/2020408.2020585"},{"key":"key-10.1145\/2676585.2676605-31","unstructured":"B. Hnich, B. M. Smith, and T. Walsh. Dual Modelling of Permutation and Injection Problems.CoRR, abs\/1107.0038, 2011."},{"key":"key-10.1145\/2676585.2676605-32","unstructured":"S. Hölldobler, N. Manthey, V. Nguyen, and P. Steinke. Solving Hidokus Using SAT Solvers. InProc. INFOCOM-5, pages 208--212, 2012. ISSN 2219-293X."},{"key":"key-10.1145\/2676585.2676605-33","unstructured":"S. Hölldobler and V.-H. Nguyen. An Efficient Encoding of the At-Most-One Constraint. Technical report, KRR Group 2013-04, Technische Universität Dresden, 01062 Dresden, Germany, 2013."},{"key":"key-10.1145\/2676585.2676605-34","unstructured":"S. Hölldobler and V.-H. Nguyen. On SAT-Encodings of the At-Most-One Constraint. InProc. Twelfth International Workshop on Constraint Modelling and Reformulation, Uppsala, Sweden, September 16-20, pages 1--17, 2013."},{"key":"key-10.1145\/2676585.2676605-35","unstructured":"H. H. Hoos.Stochastic local search - methods, models, applications. PhD thesis, 1998."},{"key":"key-10.1145\/2676585.2676605-36","unstructured":"H. H. Hoos. SAT-Encodings, Search Space Structure, and Local Search Performance. In T. Dean, editor,6th IJCAI, 2 Volumes, 1450 pages, pages 296--303. Morgan Kaufmann, 1999."},{"key":"key-10.1145\/2676585.2676605-37","unstructured":"K. Iwama and S. Miyazaki. Sat-variable complexity of hard combinatorial problems. InProceedings of the World Computer Congress of the IFIP, pages 253--258. Elsevier Science B.V., pages 253--258, 1994."},{"key":"key-10.1145\/2676585.2676605-38","doi-asserted-by":"crossref","unstructured":"P. Jeavons and J. Petke. Local Consistency and SAT-Solvers.J. Artif. Intell. Res. (JAIR), 43: 329--351, 2012.","DOI":"10.1613\/jair.3531"},{"key":"key-10.1145\/2676585.2676605-39","doi-asserted-by":"crossref","unstructured":"S. Kasif. On the Parallel Complexity of Discrete Relaxation in Constraint Satisfaction Networks.Artificial Intelligence, 45(3): 275--286, 1990.","DOI":"10.1016\/0004-3702(90)90009-O"},{"key":"key-10.1145\/2676585.2676605-40","doi-asserted-by":"crossref","unstructured":"H.-P. Kriegel, P. Kröger, J. Sander, and A. Zimek. Density-based clustering.Data Mining and Knowledge Discovery, 1(3): 231--240, 2011.","DOI":"10.1002\/widm.30"},{"key":"key-10.1145\/2676585.2676605-41","doi-asserted-by":"crossref","unstructured":"S. T. Mai. Density-based clustering: A comprehensive survey. Technical report, University of Munich, 2013.","DOI":"10.1109\/ICDM.2013.39"},{"key":"key-10.1145\/2676585.2676605-42","unstructured":"S. T. Mai.Density-based Algorithms for Active and Anytime Clustering. PhD thesis, University of Munich, 2014."},{"key":"key-10.1145\/2676585.2676605-43","doi-asserted-by":"crossref","unstructured":"S. T. Mai, S. Goebl, and C. Plant. A similarity model and segmentation algorithm for white matter fiber tracts. InICDM, pages 1014--1019, 2012.","DOI":"10.1109\/ICDM.2012.95"},{"key":"key-10.1145\/2676585.2676605-44","doi-asserted-by":"crossref","unstructured":"S. T. Mai, X. He, J. Feng, and C. Böhm. Efficient anytime density-based clustering. InSDM, pages 112--120, 2013.","DOI":"10.1137\/1.9781611972832.13"},{"key":"key-10.1145\/2676585.2676605-45","unstructured":"S. T. Mai, X. He, J. Feng, C. Plant, and C. Böhm. Anytime Density-based Clustering of Complex Data.Knowledge and Information System (KAIS), (to appear)."},{"key":"key-10.1145\/2676585.2676605-46","doi-asserted-by":"crossref","unstructured":"S. T. Mai, X. He, N. Hubig, C. Plant, and C. Böhm. Active density-based clustering. InICDM, pages 508--517, 2013.","DOI":"10.1109\/ICDM.2013.39"},{"key":"key-10.1145\/2676585.2676605-47","unstructured":"K. Marriott and P. J. Stuckey. A MiniZinc Tutorial. http:\/\/www.minizinc.org\/."},{"key":"key-10.1145\/2676585.2676605-48","doi-asserted-by":"crossref","unstructured":"A. Metodi and M. Codish. Compiling Finite Domain Constraints to SAT with BEE.Theory and Practice of Logic Programming, 12(4-5): 465--483, 2012.","DOI":"10.1017\/S1471068412000130"},{"key":"key-10.1145\/2676585.2676605-49","doi-asserted-by":"crossref","unstructured":"V.-H. Nguyen, M. N. Velev, and P. Barahona. Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. InICTAI, pages 1028--1035. IEEE, 2013.","DOI":"10.1109\/ICTAI.2013.154"},{"key":"key-10.1145\/2676585.2676605-50","doi-asserted-by":"crossref","unstructured":"O. Ohrimenko, P. Stuckey, and M. Codish. Propagation via Lazy Clause Generation.Constraints, 14(3): 357--391, 2009.","DOI":"10.1007\/s10601-008-9064-x"},{"key":"key-10.1145\/2676585.2676605-51","unstructured":"S. D. Prestwich. CNF Encodings. In Biere et al. [15], pages 75--97."},{"key":"key-10.1145\/2676585.2676605-52","unstructured":"J.-C. Régin. A Filtering Algorithm for Constraints of Difference in CSPs. In B. Hayes-Roth and R. E. Korf, editors,AAAI, pages 362--367. AAAI Press \/ The MIT Press, 1994."},{"key":"key-10.1145\/2676585.2676605-53","unstructured":"J.-C. Régin and J.-F. Puget. Solving the All Interval Problem. http:\/\/www.cs.st-andrews.ac.uk\/~ianm\/CSPLib\/prob\/prob007\/puget.pdf."},{"key":"key-10.1145\/2676585.2676605-54","unstructured":"K. A. Sakallah. Symmetry and Satisfiability. In Biere et al. [15], pages 289--338."},{"key":"key-10.1145\/2676585.2676605-55","unstructured":"B. Selman, H. J. Levesque, and D. G. Mitchell. A New Method for Solving Hard Satisfiability Problems. In W. R. Swartout, editor,AAAI, pages 440--446. AAAI Press \/ The MIT Press, 1992."},{"key":"key-10.1145\/2676585.2676605-56","unstructured":"J. M. Silva and I. Lynce. Towards Robust CNF Encodings of Cardinality Constraints. In Bessiere [14], pages 483--497."},{"key":"key-10.1145\/2676585.2676605-57","unstructured":"H. Simonis and N. Beldiceanu. A Note on CSPLIB pro007. http:\/\/www.cs.st-andrews.ac.uk\/~ianm\/CSPLib\/prob\/prob007\/helmut.pdf."},{"key":"key-10.1145\/2676585.2676605-58","doi-asserted-by":"crossref","unstructured":"N. Tamura, A. Taga, S. Kitagawa, and M. Banbara. Compiling Finite Linear CSP into SAT.Constraints, 14(2): 254--272, 2009.","DOI":"10.1007\/s10601-008-9061-0"},{"key":"key-10.1145\/2676585.2676605-59","unstructured":"W. J. van Hoeve. The alldifferent Constraint: A Survey.CoRR, cs.PL\/0105015, 2001."},{"key":"key-10.1145\/2676585.2676605-60","doi-asserted-by":"crossref","unstructured":"W.-J. van Hoeve and I. Katriel. Global constraints. In F. Rossi, P. van Beek, and T. Walsh, editors,Handbook of Constraint Programming. Elsevier, 2006.","DOI":"10.1016\/S1574-6526(06)80010-6"},{"key":"key-10.1145\/2676585.2676605-61","doi-asserted-by":"crossref","unstructured":"M. N. Velev. Exploiting Hierarchy and Structure to Efficiently Solve Graph Coloring as SAT. In G. G. E. Gielen, editor,ICCAD, pages 135--142. IEEE, 2007.","DOI":"10.1109\/ICCAD.2007.4397256"},{"key":"key-10.1145\/2676585.2676605-62","doi-asserted-by":"crossref","unstructured":"T. Walsh. SAT v CSP. InPrinciples and Practice of Constraint Programming - CP2000, volume 1894 ofLecture Notes in Computer Science, pages 441--456. Springer, 2000.","DOI":"10.1007\/3-540-45349-0_32"}],"event":{"name":"the Fifth Symposium","location":"Hanoi, Viet Nam","acronym":"SoICT '14","number":"5","start":{"date-parts":[[2014,12,4]]},"end":{"date-parts":[[2014,12,5]]}},"container-title":["Proceedings of the Fifth Symposium on Information and Communication Technology - SoICT '14"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676585.2676605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=2676605&ftid=1529161&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:30Z","timestamp":1750277670000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=2676585.2676605"}},"subtitle":["SAT vs CP"],"proceedings-subject":"Information and Communication Technology","short-title":[],"issued":{"date-parts":[[2014]]},"references-count":62,"URL":"https:\/\/doi.org\/10.1145\/2676585.2676605","relation":{},"subject":[],"published":{"date-parts":[[2014]]}}}