{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:12:28Z","timestamp":1767237148293,"version":"3.37.3"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,1,12]],"date-time":"2019-01-12T00:00:00Z","timestamp":1547251200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,1,12]],"date-time":"2019-01-12T00:00:00Z","timestamp":1547251200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP16K00304"],"award-info":[{"award-number":["JP16K00304"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP17K00307"],"award-info":[{"award-number":["JP17K00307"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10601-018-9299-0","type":"journal-article","created":{"date-parts":[[2019,1,12]],"date-time":"2019-01-12T04:34:07Z","timestamp":1547267647000},"page":"133-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2480-6597","authenticated-orcid":false,"given":"Aolong","family":"Zha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miyuki","family":"Koshimura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Fujita","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,12]]},"reference":[{"key":"9299_CR1","unstructured":"Aavani, A., Mitchell, D.G., Ternovska, E. (2013). New encoding for translating pseudo-boolean constraints into SAT. In Proceedings of the 10th symposium on abstraction, reformulation, and approximation, SARA 2013, 11-12 July 2013, Leavenworth, Washington, USA. AAAI Press. \n                    http:\/\/www.aaai.org\/ocs\/index.php\/SARA\/SARA13\/paper\/view\/7212\n                    \n                  ."},{"issue":"1","key":"9299_CR2","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V. (2012). A new look at BDDs for Pseudo-Boolean constraints. Journal of Artificial Intelligence Research, 45(1), 443\u2013480. \n                    https:\/\/doi.org\/10.1613\/jair.3653\n                    \n                  .","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9299_CR3","doi-asserted-by":"publisher","unstructured":"Aggoun, A., & Vazacopoulos, A. (2004). Solving sports scheduling and timetabling problems with constraint programming. In Butenko, S., Gil-Lafuente, J. & Pardalos, P.M. (Eds.) Economics, management and optimization in sports (pp. 243\u2013264). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-24734-0_15\n                    \n                  .","DOI":"10.1007\/978-3-540-24734-0_15"},{"key":"9299_CR4","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 427\u2013440). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-02777-2_39\n                    \n                  .","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"9299_CR5","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In Proceedings of the 24th AAAI conference on artificial intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press. \n                    http:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI10\/paper\/view\/1774\n                    \n                  ."},{"key":"9299_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3Tegui","year":"2013","unstructured":"Ans\u00f3Tegui, C., Bonet, M. L., Levy, J. (2013). SAT-Based maxSAT algorithms. Artificial Intelligence, 196, 77\u2013105. \n                    https:\/\/doi.org\/10.1016\/j.artint.2013.01.002\n                    \n                  .","journal-title":"Artificial Intelligence"},{"issue":"2","key":"9299_CR7","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E. (2011). Cardinality networks: a theoretical and empirical study. Constraints, 16(2), 195\u2013221. \n                    https:\/\/doi.org\/10.1007\/s10601-010-9105-0\n                    \n                  .","journal-title":"Constraints"},{"key":"9299_CR8","doi-asserted-by":"publisher","unstructured":"Audemard, G., Lagniez, J., Simon, L. (2013). Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In J\u00e4rvisalo, M., & Gelder, A.V. (Eds.) Theory and applications of satisfiability testing - SAT 2013 - 16th international conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 7962, pp. 309\u2013317). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23\n                    \n                  .","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"9299_CR9","unstructured":"Audemard, G., & Simon, L. (2009). Predicting learnt clauses quality in modern SAT solvers. In IJCAI 2009, Proceedings of the 21st international joint conference on artificial intelligence, Pasadena, California, USA, July 11-17, 2009 (pp. 399\u2013404). Morgan Kaufmann Publishers Inc.\n                           \n                    http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf\n                    \n                  ."},{"key":"9299_CR10","doi-asserted-by":"publisher","unstructured":"Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In Rossi, F. (Ed.) Principles and practice of constraint programming - CP 2003, 9th international conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, Lecture Notes in Computer Science (Vol. 2833, pp. 108\u2013122). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8\n                    \n                  .","DOI":"10.1007\/978-3-540-45193-8_8"},{"issue":"1-4","key":"9299_CR11","first-page":"191","volume":"2","author":"O Bailleux","year":"2006","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O. (2006). A translation of Pseudo Boolean constraints to SAT. JSAT, 2(1-4), 191\u2013200. \n                    https:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/25\n                    \n                  .","journal-title":"JSAT"},{"key":"9299_CR12","doi-asserted-by":"publisher","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O. (2009). New encodings of Pseudo-Boolean constraints into CNF. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 181\u2013194). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-02777-2_19\n                    \n                  .","DOI":"10.1007\/978-3-642-02777-2_19"},{"issue":"2-3","key":"9299_CR13","first-page":"59","volume":"7","author":"DL Berre","year":"2010","unstructured":"Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2-3), 59\u20136. \n                    https:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/82\n                    \n                  .","journal-title":"JSAT"},{"key":"9299_CR14","doi-asserted-by":"publisher","unstructured":"Codish, M., Fekete, Y., Fuhs, C., Schneider-Kamp, P. (2011). Optimal base encodings for Pseudo-Boolean constraints. In Abdulla, P.A., & Leino, K.R.M. (Eds.) Tools and algorithms for the construction and analysis of systems - 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, Lecture Notes in Computer Science (Vol. 6605, pp. 189\u2013204). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-19835-9_16\n                    \n                  .","DOI":"10.1007\/978-3-642-19835-9_16"},{"key":"9299_CR15","doi-asserted-by":"publisher","unstructured":"Codish, M., & Zazon-Ivry, M. (2010). Pairwise cardinality networks. In Clarke, E.M., & Voronkov, A. (Eds.) Logic for programming, artificial intelligence, and reasoning - 16th international conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science (Vol. 6355, pp. 154\u2013172). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-17511-4_10\n                    \n                  .","DOI":"10.1007\/978-3-642-17511-4_10"},{"key":"9299_CR16","doi-asserted-by":"publisher","unstructured":"Cook, S.A. (1971). The complexity of theorem-proving procedures. In Proceedings of the 3rd annual ACM symposium on theory of computing, STOC \u201971 (pp. 151\u2013158). ACM. \n                    https:\/\/doi.org\/10.1145\/800157.805047\n                    \n                  .","DOI":"10.1145\/800157.805047"},{"key":"9299_CR17","doi-asserted-by":"publisher","unstructured":"Davies, J., & Bacchus, F. (2011). Solving MAXSAT by solving a sequence of simpler SAT instances. In Lee, J. (Ed.) Principles and practice of constraint programming - CP 2011 - 17th international conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, Lecture Notes in Computer Science (Vol. 6876, pp. 225\u2013239). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-23786-7_19\n                    \n                  .","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"9299_CR18","doi-asserted-by":"publisher","unstructured":"Davies, J., & Bacchus, F. (2013). Exploiting the power of mip solvers in maxsat. In J\u00e4rvisalo, M., & Gelder, A.V. (Eds.) Theory and applications of satisfiability testing - SAT 2013 - 16th international conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 7962, pp. 166\u2013181). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-39071-5_13\n                    \n                  .","DOI":"10.1007\/978-3-642-39071-5_13"},{"key":"9299_CR19","doi-asserted-by":"publisher","unstructured":"Davies, J., & Bacchus, F. (2013). Postponing optimization to speed up MAXSAT solving. In Schulte, C. (Ed.) Principles and practice of constraint programming - 19th international conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 8124, pp. 247\u2013262). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-40627-0_21\n                    \n                  .","DOI":"10.1007\/978-3-642-40627-0_21"},{"issue":"1-4","key":"9299_CR20","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2006). Translating Pseudo-Boolean constraints into SAT. JSAT, 2(1-4), 1\u201326. \n                    https:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/18\n                    \n                  .","journal-title":"JSAT"},{"key":"9299_CR21","doi-asserted-by":"publisher","unstructured":"Fei, L., Mize, L., Moon, C., Mullen, B., Singhal, S. (2010). Constraint analysis and debugging for multi-million instance SoC designs. In 11th international symposium on quality electronic design (ISQED), 22-24 March 2010, San Jose, CA, USA (pp. 422\u2013427): IEEE.\n                           \n                    https:\/\/doi.org\/10.1109\/ISQED.2010.5450540\n                    \n                  .","DOI":"10.1109\/ISQED.2010.5450540"},{"key":"9299_CR22","doi-asserted-by":"publisher","unstructured":"Fekete, Y., & Codish, M. (2014). Simplifying Pseudo-Boolean constraints in residual number systems. In Sinz, C., & Egly, U. (Eds.) Theory and applications of satisfiability testing - SAT 2014 - 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science (Vol. 8561, pp. 351\u2013366). Springer International Publishing. \n                    https:\/\/doi.org\/10.1007\/978-3-319-09284-3_26\n                    \n                  .","DOI":"10.1007\/978-3-319-09284-3_26"},{"key":"9299_CR23","doi-asserted-by":"publisher","unstructured":"Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In Biere, A., & Gomes, C.P. (Eds.) Theory and applications of satisfiability testing - SAT 2006, 9th international conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, Lecture Notes in Computer Science (Vol. 4121, pp. 252\u2013265). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/11814948_25\n                    \n                  .","DOI":"10.1007\/11814948_25"},{"key":"9299_CR24","unstructured":"Gent, I.P. (2002). Arc consistency in SAT. In Proceedings of the 15th Eureopean conference on artificial intelligence, ECAI\u20192002, Lyon, France, July 2002 (pp. 121\u2013125): IOS Press. \n                    https:\/\/ipg.host.cs.st-andrews.ac.uk\/papers\/ipgECAI.ps\n                    \n                  ."},{"issue":"4","key":"9299_CR25","first-page":"85","volume":"B4","author":"S Hayata","year":"2015","unstructured":"Hayata, S., & Hasegawa, R. (2015). Improvement in CNF encoding of cardinality constraints for weighted partial MaxSAT. SIG-FPAI, in Japanese, B4(4), 85\u201390. \n                    http:\/\/id.nii.ac.jp\/1004\/00000592\n                    \n                  .","journal-title":"SIG-FPAI, in Japanese"},{"key":"9299_CR26","unstructured":"Heras, F., Morgado, A., Marques-Silva, J. (2011). Core-guided binary search algorithms for maximum satisfiability. In Proceedings of the 25th AAAI conference on artificial intelligence, AAAI 2011, San Francisco, California, USA, August 7-11, 2011: AAAI Press. \n                    http:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI11\/paper\/view\/3713\n                    \n                  ."},{"issue":"1","key":"9299_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1080\/10511970701744992","volume":"18","author":"LJ Heyer","year":"2008","unstructured":"Heyer, L.J. (2008). A mathematical optimization problem in bioinformatics. PRIMUS, 18(1), 101\u2013118. \n                    https:\/\/doi.org\/10.1080\/10511970701744992\n                    \n                  .","journal-title":"PRIMUS"},{"key":"9299_CR28","doi-asserted-by":"publisher","unstructured":"H\u00f6lldobler, S., Manthey, N., Steinke, P. (2012). A compact encoding of pseudo-boolean constraints into SAT. In Glimm, B., & Kr\u00fcger, A. (Eds.) KI 2012: Advances in artificial intelligence - 35th annual German conference on AI, Saarbr\u00fccken, Germany, September 24-27, 2012. Proceedings, Lecture Notes in Computer Science (Vol. 7526, pp. 107\u2013118). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-33347-7_10\n                    \n                  .","DOI":"10.1007\/978-3-642-33347-7_10"},{"issue":"3","key":"9299_CR29","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1287\/opre.1060.0371","volume":"55","author":"JN Hooker","year":"2007","unstructured":"Hooker, J.N. (2007). Planning and scheduling by Logic-Based benders decomposition. Operations Research, 55(3), 588\u2013602. \n                    https:\/\/doi.org\/10.1287\/opre.1060.0371\n                    \n                  .","journal-title":"Operations Research"},{"key":"9299_CR30","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J. (2018). PySAT: a python toolkit for prototyping with SAT Oracles. In Beyersdorff, O., & Wintersteiger, C.M. (Eds.) Theory and applications of satisfiability testing - SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science (Vol. 10929, pp. 428\u2013437). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26\n                    \n                  .","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"9299_CR31","doi-asserted-by":"publisher","unstructured":"Joshi, S., Martins, R., Manquinho, V.M. (2015). Generalized totalizer encoding for pseudo-boolean constraints. In Pesant, G. (Ed.) Principles and practice of constraint programming - 21st international conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, Lecture Notes in Computer Science (Vol. 9255, pp. 200\u2013209). Springer International Publishing. \n                    https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15\n                    \n                  .","DOI":"10.1007\/978-3-319-23219-5_15"},{"key":"9299_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24777-7","volume-title":"Knapsack problems","author":"H Kellerer","year":"2004","unstructured":"Kellerer, H., Pferschy, U., Pisinger, D. (2004). Knapsack problems. Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-24777-7\n                    \n                  ."},{"issue":"1\/2","key":"9299_CR33","first-page":"95","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R. (2012). QMaxSAT: a partial Max-SAT solver. JSAT, 8(1\/2), 95\u2013100. \n                    https:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/98\n                    \n                  .","journal-title":"JSAT"},{"issue":"1","key":"9299_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2004.05.004","volume":"159","author":"J Larrosa","year":"2004","unstructured":"Larrosa, J., & Schiex, T. (2004). Solving weighted CSP by maintaining arc consistency. Artificial Intelligence, 159(1), 1\u201326. \n                    https:\/\/doi.org\/10.1016\/j.artint.2004.05.004\n                    \n                  .","journal-title":"Artificial Intelligence"},{"key":"9299_CR35","doi-asserted-by":"publisher","unstructured":"Li, C.M., & Many\u00e0, F. (2009). MaxSAT, hard and soft constraints. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications, (Vol. 185, pp. 613\u2013631). Amsterdam: IOS Press. \n                    https:\/\/doi.org\/10.3233\/978-1-58603-929-5-613\n                    \n                  .","DOI":"10.3233\/978-1-58603-929-5-613"},{"key":"9299_CR36","doi-asserted-by":"publisher","unstructured":"Manquinho, V.M., Silva, J.P.M., Planes, J. (2009). Algorithms for weighted boolean optimization. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 495\u2013508). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-02777-2_45\n                    \n                  .","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"9299_CR37","doi-asserted-by":"publisher","unstructured":"Manthey, N., Philipp, T., Steinke, P. (2014). A more compact translation of pseudo-boolean constraints into CNF such that generalized arc consistency is maintained. In Lutz, C., & Thielscher, M. (Eds.) KI 2014: advances in artificial intelligence - 37th annual German conference on AI, Stuttgart, Germany, September 22-26, 2014. Proceedings, Lecture Notes in Computer Science (Vol. 8736, pp. 123\u2013134). Springer International Publishing. \n                    https:\/\/doi.org\/10.1007\/978-3-319-11206-0_13\n                    \n                  .","DOI":"10.1007\/978-3-319-11206-0_13"},{"key":"9299_CR38","doi-asserted-by":"publisher","unstructured":"Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H. (2013). Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In 2013 IEEE 25th international conference on tools with artificial intelligence, Herndon, VA, USA, November 4-6, 2013 (pp. 9\u201317): IEEE Computer Society. \n                    https:\/\/doi.org\/10.1109\/ICTAI.2013.13\n                    \n                  .","DOI":"10.1109\/ICTAI.2013.13"},{"key":"9299_CR39","doi-asserted-by":"publisher","unstructured":"Paxian, T., Reimer, S., Becker, B. (2018). Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In Beyersdorff, O., & Wintersteiger, C.M. (Eds.) Theory and applications of satisfiability testing - SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science (Vol. 10929, pp. 37\u201353). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-94144-8_3\n                    \n                  .","DOI":"10.1007\/978-3-319-94144-8_3"},{"key":"9299_CR40","doi-asserted-by":"publisher","unstructured":"Roussel, O., & Manquinho, V.M. (2004). Pseudo-Boolean and cardinality constraints. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (Vol. 185, pp. 695\u2013733). Amsterdam: IOS Press. \n                    https:\/\/doi.org\/10.3233\/978-1-58603-929-5-695\n                    \n                  .","DOI":"10.3233\/978-1-58603-929-5-695"},{"key":"9299_CR41","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., & Lynce, I. (2007). Towards robust CNF encodings of cardinality constraints. In Bessi\u00e8re, C. (Ed.) Principles and practice of constraint programming - CP 2007, 13th international conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, Lecture Notes in Computer Science (Vol. 4741, pp. 483\u2013497). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-74970-7_35\n                    \n                  .","DOI":"10.1007\/978-3-540-74970-7_35"},{"key":"9299_CR42","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Lynce, I., Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (Vol. 185, pp. 131\u2013153). Amsterdam: IOS Press. \n                    https:\/\/doi.org\/10.3233\/978-1-58603-929-5-131\n                    \n                  .","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"9299_CR43","doi-asserted-by":"publisher","unstructured":"Sinz, C. (2005). Towards an optimal CNF encoding of Boolean cardinality constraints. In van Beek, P. (Ed.) Principles and practice of constraint programming - CP 2005, 11th international conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, Lecture Notes in Computer Science (Vol. 3709, pp. 827\u2013831). Berlin: Springer. \n                    https:\/\/doi.org\/10.1007\/11564751_73\n                    \n                  .","DOI":"10.1007\/11564751_73"},{"issue":"2","key":"9299_CR44","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63\u201369. \n                    https:\/\/doi.org\/10.1016\/S0020-0190(98)00144-6\n                    \n                  .","journal-title":"Information Processing Letters"},{"key":"9299_CR45","doi-asserted-by":"publisher","unstructured":"Wood, R.G., & Rutenbar, R.A. (1997). FPGA routing and routability estimation via Boolean satisfiability. In Proceedings of the 1997 ACM 5th international symposium on field-programmable gate arrays, FPGA \u201997 (pp. 119\u2013125). ACM. \n                    https:\/\/doi.org\/10.1145\/258305.258322\n                    \n                  .","DOI":"10.1145\/258305.258322"},{"key":"9299_CR46","doi-asserted-by":"publisher","unstructured":"Zha, A., Koshimura, M., Fujita, H. (2017). A hybrid encoding of pseudo-boolean constraints into CNF. In Conference on technologies and applications of artificial intelligence, TAAI 2017, Taipei, Taiwan, December 1-3, 2017 (pp. 9\u201312). IEEE Computer Society. \n                    https:\/\/doi.org\/10.1109\/TAAI.2017.15\n                    \n                  .","DOI":"10.1109\/TAAI.2017.15"},{"key":"9299_CR47","doi-asserted-by":"publisher","unstructured":"Zha, A., Nomoto, K., Ueda, S., Koshimura, M., Sakurai, Y., Yokoo, M. (2017). Coalition structure generation for partition function games utilizing a concise graphical representation. In An, B., Bazzan, A., Leite, J., Villata, S., van der Torre, L. (Eds.) PRIMA 2017: principles and practice of multi-agent systems - 20th international conference, Nice, France, October 30 - November 3, 2017, Proceedings, Lecture Notes in Computer Science (Vol. 10621, pp. 143\u2013159): Springer International Publishing. \n                    https:\/\/doi.org\/10.1007\/978-3-319-69131-2_9\n                    \n                  .","DOI":"10.1007\/978-3-319-69131-2_9"},{"key":"9299_CR48","doi-asserted-by":"publisher","unstructured":"Zha, A., Uemura, N., Koshimura, M., Fujita, H. (2017). Mixed radix weight totalizer encoding for Pseudo-Boolean constraints. In 2017 IEEE 29th international conference on tools with artificial intelligence, Boston, MA, USA, November 6-8, 2017 (pp. 868\u2013875). IEEE Computer Society. \n                    https:\/\/doi.org\/10.1109\/ICTAI.2017.00135\n                    \n                  .","DOI":"10.1109\/ICTAI.2017.00135"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-018-9299-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-018-9299-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-018-9299-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T14:58:28Z","timestamp":1589727508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-018-9299-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,12]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["9299"],"URL":"https:\/\/doi.org\/10.1007\/s10601-018-9299-0","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2019,1,12]]},"assertion":[{"value":"12 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}