{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:35Z","timestamp":1771262195799,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319232188","type":"print"},{"value":"9783319232195","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-23219-5_15","type":"book-chapter","created":{"date-parts":[[2015,8,12]],"date-time":"2015-08-12T10:17:33Z","timestamp":1439374653000},"page":"200-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Generalized Totalizer Encoding for Pseudo-Boolean Constraints"],"prefix":"10.1007","author":[{"given":"Saurabh","family":"Joshi","sequence":"first","affiliation":[]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,13]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","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.: A New Look at BDDs for Pseudo-Boolean Constraints. Journal of Artificial Intelligence Research 45, 443\u2013480 (2012)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Generic ILP versus specialized 0\u20131 ILP: an update. In: International Conference on Computer-Aided Design, pp. 450\u2013457. IEEE Press (2002)","DOI":"10.1145\/774572.774638"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P.: Solving linux upgradeability problems using boolean optimization. In: Workshop on Logics for Component Configuration, pp. 11\u201322 (2010)","DOI":"10.4204\/EPTCS.29.2"},{"issue":"2","key":"15_CR4","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.: Cardinality Networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"issue":"1\u20134","key":"15_CR6","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/SAT190021","volume":"2","author":"O Bailleux","year":"2006","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A Translation of Pseudo Boolean Constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1\u20134), 191\u2013200 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-02777-2_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"O Bailleux","year":"2009","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181\u2013194. Springer, Heidelberg (2009)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Barth, P.: Logic-based 0\u20131 Constraint Programming. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-1-4613-1315-1"},{"key":"15_CR9","unstructured":"B\u00fcttner, M., Rintanen, J.: Satisfiability planning with constraints on the number of actions. In: International Conference on Automated Planning and Scheduling, pp. 292\u2013299. AAAI Press (2005)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"1\u20134","key":"15_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1\u20134), 1\u201326 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"15_CR12","unstructured":"Gent, I.P.: Arc consistency in SAT. In: European Conference on Artificial Intelligence, pp. 121\u2013125. IOS Press (2002)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-28067-2_3","volume-title":"Algebraic and Numeric Biology","author":"A Gra\u00e7a","year":"2012","unstructured":"Gra\u00e7a, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Efficient and accurate haplotype inference by combining parsimony and pedigree information. In: Horimoto, K., Nakatsui, M., Popov, N. (eds.) ANB 2010. LNCS, vol. 6479, pp. 38\u201356. Springer, Heidelberg (2012)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-33347-7_10","volume-title":"KI 2012: Advances in Artificial Intelligence","author":"S H\u00f6lldobler","year":"2012","unstructured":"H\u00f6lldobler, S., Manthey, N., Steinke, P.: A compact encoding of pseudo-boolean constraints into SAT. In: Glimm, B., Kr\u00fcger, A. (eds.) KI 2012. LNCS, vol. 7526, pp. 107\u2013118. Springer, Heidelberg (2012)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Janota, M., Marques-Silva, J.: Towards efficient optimization in package management systems. In: International Conference on Software Engineering, pp. 745\u2013755. ACM (2014)","DOI":"10.1145\/2568225.2568306"},{"issue":"1\/2","key":"15_CR16","first-page":"89","volume":"8","author":"M Janota","year":"2012","unstructured":"Janota, M., Lynce, I., Manquinho, V.M., Marques-Silva, J.: PackUp: Tools for Package Upgradability Solving. JSAT 8(1\/2), 89\u201394 (2012)","journal-title":"JSAT"},{"key":"15_CR17","doi-asserted-by":"crossref","first-page":"95","DOI":"10.3233\/SAT190091","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8, 95\u2013100 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"2\u20133","key":"15_CR18","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7(2\u20133), 59\u201364 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"V Manquinho","year":"2009","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 495\u2013508. Springer, Heidelberg (2009)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-319-11206-0_13","volume-title":"KI 2014: Advances in Artificial Intelligence","author":"N Manthey","year":"2014","unstructured":"Manthey, N., Philipp, T., Steinke, P.: 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. LNCS, vol. 8736, pp. 123\u2013134. Springer, Heidelberg (2014)"},{"key":"15_CR21","unstructured":"Manthey, N., Steinke, P.: npSolver - A SAT based solver for optimization problems. In: Pragmatics of SAT (2012)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Integer programming models for optimization problems in test generation. In: Asia and South Pacific Design Automation, pp. 481\u2013487. IEEE Press (1998)","DOI":"10.1109\/ASPDAC.1998.669530"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Heidelberg (2014)"},{"issue":"3","key":"15_CR24","doi-asserted-by":"crossref","first-page":"229","DOI":"10.3233\/AIC-140592","volume":"27","author":"M Miranda","year":"2014","unstructured":"Miranda, M., Lynce, I., Manquinho, V.: Inferring phylogenetic trees using pseudo-Boolean optimization. AI Communications 27(3), 229\u2013243 (2014)","journal-title":"AI Communications"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In: International Conference on Tools with Artificial Intelligence, pp. 9\u201317. IEEE Press (2013)","DOI":"10.1109\/ICTAI.2013.13"},{"key":"15_CR26","unstructured":"Prestwich, S., Quirke, C.: Boolean and pseudo-boolean models for scheduling. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2003)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-34654-5_37","volume-title":"Advances in Artificial Intelligence \u2013 IBERAMIA 2012","author":"BC Ribas","year":"2012","unstructured":"Ribas, B.C., Suguimoto, R.M., Monta\u00f1o, R.A.N.R., Silva, F., de Bona, L., Castilho, M.A.: On modelling virtual machine consolidation to pseudo-boolean constraints. In: Pav\u00f3n, J., Duque-M\u00e9ndez, N.D., Fuentes-Fern\u00e1ndez, R. (eds.) IBERAMIA 2012. LNCS, vol. 7637, pp. 361\u2013370. Springer, Heidelberg (2012)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"15_CR29","unstructured":"Steinke, P., Manthey, N.: PBLib-A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF. Tech. rep., Technische Universit\u00e4t Dresden (2014). http:\/\/tools.computational-logic.org\/content\/pblib.php"},{"issue":"2","key":"15_CR30","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J Warners","year":"1998","unstructured":"Warners, J.: A Linear-Time Transformation of Linear Inequalities into Conjunctive Normal Form. Information Processing Letters 68(2), 63\u201369 (1998)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23219-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T23:47:47Z","timestamp":1748562467000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23219-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319232188","9783319232195"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"13 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}