{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:26Z","timestamp":1771262186823,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_33","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"438-445","source":"Crossref","is-referenced-by-count":85,"title":["Open-WBO: A Modular MaxSAT Solver,"],"prefix":"10.1007","author":[{"given":"Ruben","family":"Martins","sequence":"first","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Ach\u00e1, R.A., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, 1\u201321 (2012)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-33558-7_9","volume-title":"Principles and Practice of Constraint Programming","author":"C. Ans\u00f3tegui","year":"2012","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gab\u00e0s, J., Levy, J.: Improving SAT-Based Weighted MaxSAT Solvers. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 86\u2013101. Springer, Heidelberg (2012)"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann [18], pp. 427\u2013440","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11527695_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"C. Ans\u00f3tegui","year":"2005","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F.: Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 1\u201315. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"33_CR5","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/AIC-2010-0462","volume":"23","author":"R. As\u00edn","year":"2010","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Communications\u00a023(2-3), 145\u2013157 (2010)","journal-title":"AI Communications"},{"issue":"2","key":"33_CR6","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\u00a016(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G. Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.M., Simon, L.: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 309\u2013317. Springer, Heidelberg (2013)"},{"key":"33_CR8","unstructured":"Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. In: Boutilier, C. (ed.) International Joint Conference on Artificial Intelligence, pp. 399\u2013404 (2009)"},{"key":"33_CR9","unstructured":"Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 42\u201343"},{"key":"33_CR10","unstructured":"Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M.: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Tech. rep., Department of Computer Science Series of Publications B, vol. B-2013-1, University of Helsinki, Helsinki (2013)"},{"key":"33_CR11","unstructured":"Chen, J.: Solvers with a Bit-Encoding Phase Selection Policy and a Decision-Depth-Sensitive Restart Policy. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 44\u201345"},{"key":"33_CR12","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z. Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On Solving the Partial MAX-SAT Problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"key":"33_CR14","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of All Different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a07526, pp. 107\u2013118. Springer, Heidelberg (2012)"},{"issue":"1\/2","key":"33_CR16","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/SAT190090","volume":"8","author":"M. Janota","year":"2012","unstructured":"Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: Tools for Package Upgradability Solving. Journal on Satisfiability, Boolean Modeling and Computation\u00a08(1\/2), 89\u201394 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"33_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\u00a08, 95\u2013100 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","year":"2009","unstructured":"Kullmann, O. (ed.): SAT 2009. LNCS, vol.\u00a05584. Springer, Heidelberg (2009)"},{"issue":"2-3","key":"33_CR19","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\u00a07(2-3), 59\u201366 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Rapicault, P.: Dependency Management for the Eclipse Ecosystem: Eclipse P2, Metadata and Resolution. In: International Workshop on Open Component Ecosystems, pp. 21\u201330. ACM (2009)","DOI":"10.1145\/1595800.1595805"},{"key":"33_CR21","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability, pp. 613\u2013631. IOS Press (2009)"},{"issue":"4","key":"33_CR22","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M. Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal Speedup of Las Vegas Algorithms. Information Processing Letters\u00a047(4), 173\u2013180 (1993)","journal-title":"Information Processing Letters"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Kullmann [18], pp. 495\u2013508","DOI":"10.1007\/978-3-642-02777-2_45"},{"issue":"3-4","key":"33_CR24","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10472-011-9233-2","volume":"62","author":"J. Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Argelich, J., Gra\u00e7a, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Annals of Mathematics and Artificial Intelligence\u00a062(3-4), 317\u2013343 (2011)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"33_CR25","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: On Partitioning for Maximum Satisfiability. In: Raedt, L.D., Bessi\u00e8re, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol.\u00a0242, pp. 913\u2013914. IOS Press (2012)"},{"issue":"4","key":"33_CR26","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A. Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints\u00a018(4), 478\u2013534 (2013)","journal-title":"Constraints"},{"key":"33_CR27","unstructured":"Nabeshima, H., Iwanuma, K., Inoue, K.: GLUEMINISAT2.2.7. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 46\u201347"},{"key":"33_CR28","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 (2013)","DOI":"10.1109\/ICTAI.2013.13"},{"key":"33_CR29","unstructured":"Oh, C.: gluH: Modified Version of glucose 2.1. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], p. 48"},{"key":"33_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A Lightweight Component Caching Scheme for Satisfiability Solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"33_CR31","unstructured":"Wieringa, S.: GlucoRed. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 40\u201341"},{"key":"33_CR32","unstructured":"Yasumoto, T., Okugawa, T.: SINNminisat. In: Proceedings of SAT Competition 2013 : Solver and Benchmark Descriptions [10], p. 85"},{"key":"33_CR33","unstructured":"Yasumoto, T., Okugawa, T.: ZENN. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], p. 95"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T22:01:25Z","timestamp":1598047285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}