{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T11:30:24Z","timestamp":1771241424349,"version":"3.50.1"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T00:00:00Z","timestamp":1771200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T00:00:00Z","timestamp":1771200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005765","name":"Universidade de Lisboa","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005765","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>In the last decade, numerous algorithms for single-objective Boolean optimization have been proposed that rely on the iterative usage of a highly effective Propositional Satisfiability (SAT) solver. But the use of SAT solvers in Multi-Objective Combinatorial Optimization (MOCO) algorithms is scarce. Due to the shortage of efficient tools for MOCO, many real-world applications formulated as multi-objective are cast as single-objective, using either a linear combination or by setting a preference order among the objectives. In this paper, we extend the state of the art of MOCO solvers with three novel unsatisfiability-based algorithms. The first two are core-guided MOCO solvers. The third is a hitting set MOCO solver. Experimental results in several sets of benchmark instances show that our new unsatisfiability-based algorithms can outperform and complement other SAT-based, state-of-the-art algorithms for MOCO.<\/jats:p>","DOI":"10.1007\/s10817-026-09749-w","type":"journal-article","created":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T10:57:30Z","timestamp":1771239450000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unsatisfiability-based Algorithms for Multi-Objective Combinatorial Optimization"],"prefix":"10.1007","volume":"70","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4833-8054","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Cortes","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4868-415X","authenticated-orcid":false,"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4205-2189","authenticated-orcid":false,"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,16]]},"reference":[{"key":"9749_CR1","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1016\/j.future.2017.08.027","volume":"105","author":"R Li","year":"2020","unstructured":"Li, R., Zheng, Q., Li, X., Yan, Z.: Multi-objective optimization for rebalancing virtual machine placement. Future Gener. Comput. Syst. 105, 824\u2013842 (2020). https:\/\/doi.org\/10.1016\/j.future.2017.08.027","journal-title":"Future Gener. Comput. Syst."},{"key":"9749_CR2","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.eswa.2019.04.024","volume":"130","author":"R Marques","year":"2019","unstructured":"Marques, R., Russo, L.M.S., Roma, N.: Flying tourist problem: Flight time and cost minimization in complex routes. Expert Syst. Appl. 130, 172\u2013187 (2019). https:\/\/doi.org\/10.1016\/j.eswa.2019.04.024","journal-title":"Expert Syst. Appl."},{"issue":"10","key":"9749_CR3","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1109\/TSE.2018.2874648","volume":"46","author":"Y Yuan","year":"2020","unstructured":"Yuan, Y., Banzhaf, W.: ARJA: automated repair of java programs via multi-objective genetic programming. IEEE Trans. Software Eng. 46(10), 1040\u20131067 (2020). https:\/\/doi.org\/10.1109\/TSE.2018.2874648","journal-title":"IEEE Trans. Software Eng."},{"key":"9749_CR4","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. Ann. Math. Artif. Intell. 62, 317\u2013343 (2011). https:\/\/doi.org\/10.1007\/s10472-011-9233-2","journal-title":"Ann. Math. Artif. Intell."},{"key":"9749_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/j.cor.2021.105471","volume":"136","author":"AP Guerreiro","year":"2021","unstructured":"Guerreiro, A.P., Manquinho, V.M., Figueira, J.R.: Exact hypervolume subset selection through incremental computations. Comput. Oper. Res. 136, 105471 (2021). https:\/\/doi.org\/10.1016\/j.cor.2021.105471","journal-title":"Comput. Oper. Res."},{"key":"9749_CR6","doi-asserted-by":"publisher","unstructured":"Deb, K., Agrawal, S., Pratap, A., Meyarivan, T.: A fast elitist non-dominated sorting genetic algorithm for multi-objective optimisation: NSGA-II. In: 6th International Conference Parallel Problem Solving from Nature. Lecture Notes in Computer Science, vol. 1917, pp. 849\u2013858. Springer, Paris, France (2000). https:\/\/doi.org\/10.1007\/3-540-45356-3_83","DOI":"10.1007\/3-540-45356-3_83"},{"issue":"6","key":"9749_CR7","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1109\/TEVC.2007.892759","volume":"11","author":"Q Zhang","year":"2007","unstructured":"Zhang, Q., Li, H.: MOEA\/D: A multiobjective evolutionary algorithm based on decomposition. IEEE Trans. Evol. Comput. 11(6), 712\u2013731 (2007). https:\/\/doi.org\/10.1109\/TEVC.2007.892759","journal-title":"IEEE Trans. Evol. Comput."},{"key":"9749_CR8","doi-asserted-by":"publisher","unstructured":"Gavanelli, M.: An algorithm for multi-criteria optimization in csps. In: European Conference on Artificial Intelligence, pp. 136\u2013140. IOS Press, Lyon, France (2002). https:\/\/doi.org\/10.5555\/3000905.3000935","DOI":"10.5555\/3000905.3000935"},{"key":"9749_CR9","doi-asserted-by":"publisher","unstructured":"Legriel, J., Guernic, C.L., Cotton, S., Maler, O.: Approximating the pareto front of multi-criteria optimization problems. In: Esparza, J., Majumdar, R. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS). Lecture Notes in Computer Science, vol. 6015, pp. 69\u201383. Springer, Paphos, Cyprus (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_6","DOI":"10.1007\/978-3-642-12002-2_6"},{"key":"9749_CR10","unstructured":"Rayside, D., Estler, H.-C., Jackson, D.: The guided improvement algorithm for exact, general-purpose, many-objective combinatorial optimization. Technical Report Technical Report MIT-CSAIL-TR-2009-033, MIT Massachusetts Institute of Technology (2009)"},{"key":"9749_CR11","doi-asserted-by":"publisher","unstructured":"Terra-Neves, M., Lynce, I., Manquinho, V.M.: Introducing pareto minimal correction subsets. In: International Conference on Theory and Applications of Satisfiability Testing. LNCS, vol. 10491, pp. 195\u2013211. Springer, Melbourne, Australia (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_13","DOI":"10.1007\/978-3-319-66263-3_13"},{"key":"9749_CR12","doi-asserted-by":"publisher","unstructured":"Soh, T., Banbara, M., Tamura, N., Berre, D.L.: Solving multiobjective discrete optimization problems with propositional minimal model generation. In: International Conference Principles and Practice of Constraint Programming. LNCS, vol. 10416, pp. 596\u2013614. Springer, Melbourne, Australia (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_38","DOI":"10.1007\/978-3-319-66158-2_38"},{"key":"9749_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/J.COR.2023.106153","volume":"153","author":"AP Guerreiro","year":"2023","unstructured":"Guerreiro, A.P., Cortes, J., Vanderpooten, D., Bazgan, C., Lynce, I., Manquinho, V.M., Figueira, J.R.: Exact and approximate determination of the pareto front using minimal correction subsets. Comput. Oper. Res. 153, 106153 (2023). https:\/\/doi.org\/10.1016\/J.COR.2023.106153","journal-title":"Comput. Oper. Res."},{"issue":"6","key":"9749_CR14","doi-asserted-by":"publisher","first-page":"3865","DOI":"10.1007\/s10489-020-01998-5","volume":"51","author":"N Tian","year":"2021","unstructured":"Tian, N., Ouyang, D., Wang, Y., Hou, Y., Zhang, L.: Core-guided method for constraint-based multi-objective combinatorial optimization. Appl. Intell. 51(6), 3865\u20133879 (2021). https:\/\/doi.org\/10.1007\/s10489-020-01998-5","journal-title":"Appl. Intell."},{"key":"9749_CR15","doi-asserted-by":"publisher","unstructured":"Janota, M., Morgado, A., Santos, J.F., Manquinho, V.M.: The seesaw algorithm: Function optimization using implicit hitting sets. In: International Conference on Principles and Practice of Constraint Programming. LIPIcs, vol. 210, pp. 31\u201313116. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Online (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2021.31","DOI":"10.4230\/LIPIcs.CP.2021.31"},{"key":"9749_CR16","doi-asserted-by":"publisher","first-page":"1223","DOI":"10.1613\/jair.1.15333","volume":"80","author":"C Jabs","year":"2024","unstructured":"Jabs, C., Berg, J., Niskanen, A., J\u00e4rvisalo, M.: From single-objective to bi-objective maximum satisfiability solving. Journal of Artificial Intelligence Research 80, 1223\u20131269 (2024). https:\/\/doi.org\/10.1613\/jair.1.15333","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9749_CR17","doi-asserted-by":"publisher","unstructured":"Jabs, C., Berg, J., J\u00e4rvisalo, M.: Core boosting in sat-based multi-objective optimization. In: Dilkina, B. (ed.) Integration of Constraint Programming, Artificial Intelligence, and Operations Research\u201421st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28\u201331, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14743, pp. 1\u201319. Springer, (2024). https:\/\/doi.org\/10.1007\/978-3-031-60599-4_1","DOI":"10.1007\/978-3-031-60599-4_1"},{"key":"9749_CR18","doi-asserted-by":"publisher","unstructured":"Cortes, J., Lynce, I., Manquinho, V.: New core-guided and hitting set algorithms for multi-objective combinatorial optimization. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 55\u201373. Springer, Paris, France (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_7","DOI":"10.1007\/978-3-031-30820-8_7"},{"key":"9749_CR19","volume-title":"Multicriteria Optimization","author":"M Ehrgott","year":"2005","unstructured":"Ehrgott, M.: Multicriteria Optimization. Springer, Berlin, Heidelberg (2005)"},{"key":"9749_CR20","doi-asserted-by":"publisher","unstructured":"Li, C.M., Many\u00e0, F.: Maxsat, hard and soft constraints. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 613\u2013631. IOS Press, Amsterdam, Netherlands (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-613","DOI":"10.3233\/978-1-58603-929-5-613"},{"key":"9749_CR21","doi-asserted-by":"publisher","unstructured":"Roussel, O., Manquinho, V.M.: Pseudo-boolean and cardinality constraints. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 695\u2013733. IOS Press, Amsterdam, Netherlands (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-695","DOI":"10.3233\/978-1-58603-929-5-695"},{"issue":"9","key":"9749_CR22","doi-asserted-by":"publisher","first-page":"2674","DOI":"10.1016\/J.COR.2005.10.003","volume":"34","author":"M Ehrgott","year":"2007","unstructured":"Ehrgott, M., Gandibleux, X.: Bound sets for biobjective combinatorial optimization problems. Comput. Oper. Res. 34(9), 2674\u20132694 (2007). https:\/\/doi.org\/10.1016\/J.COR.2005.10.003","journal-title":"Comput. Oper. Res."},{"issue":"3","key":"9749_CR23","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1016\/j.ejor.2017.01.032","volume":"260","author":"A Przybylski","year":"2017","unstructured":"Przybylski, A., Gandibleux, X.: Multi-objective branch and bound. Eur. J. Oper. Res. 260(3), 856\u2013872 (2017). https:\/\/doi.org\/10.1016\/j.ejor.2017.01.032","journal-title":"Eur. J. Oper. Res."},{"key":"9749_CR24","doi-asserted-by":"publisher","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 2833, pp. 108\u2013122. Springer, Kinsale, Ireland (2003). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"9749_CR25","doi-asserted-by":"publisher","unstructured":"Joshi, S., Martins, R., Manquinho, V.M.: Generalized totalizer encoding for pseudo-boolean constraints. In: International Conference Principles and Practice of Constraint Programming. LNCS, vol. 9255, pp. 200\u2013209. Springer, Cork, Ireland (2015). https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15","DOI":"10.1007\/978-3-319-23219-5_15"},{"issue":"3\u20134","key":"9749_CR26","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/s10601-019-09302-0","volume":"24","author":"M Karpinski","year":"2019","unstructured":"Karpinski, M., Piotr\u00f3w, M.: Encoding cardinality constraints using multiway merge selection networks. Constraints 24(3\u20134), 234\u2013251 (2019). https:\/\/doi.org\/10.1007\/s10601-019-09302-0","journal-title":"Constraints"},{"key":"9749_CR27","doi-asserted-by":"publisher","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) 9th International Conference on Theory and Applications of Satisfiability Testing - SAT 2006, Seattle, WA, USA, August 12-15, 2006. Lecture Notes in Computer Science, vol. 4121, pp. 252\u2013265. Springer, Seattle, WA, USA (2006). https:\/\/doi.org\/10.1007\/11814948_25","DOI":"10.1007\/11814948_25"},{"key":"9749_CR28","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Manquinho, V.M.: Towards more effective unsatisfiability-based maximum satisfiability algorithms. In: B\u00fcning, H.K., Zhao, X. (eds.) 11th International Conference on Theory and Applications of Satisfiability Testing, SAT 2008, Guangzhou, China, May 12-15, 2008. Lecture Notes in Computer Science, vol. 4996, pp. 225\u2013230. Springer, Guangzhou, China (2008). https:\/\/doi.org\/10.1007\/978-3-540-79719-7_21","DOI":"10.1007\/978-3-540-79719-7_21"},{"key":"9749_CR29","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Sciuto, D. (ed.) Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008, pp. 408\u2013413. ACM, Munich, Germany (2008). https:\/\/doi.org\/10.1109\/DATE.2008.4484715","DOI":"10.1109\/DATE.2008.4484715"},{"key":"9749_CR30","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: International Conference Theory and Applications of Satisfiability Testing. LNCS, vol. 5584, pp. 427\u2013440. Springer, Swansea, UK (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_39","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"9749_CR31","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR abs\/0712.1097 (2007)"},{"key":"9749_CR32","doi-asserted-by":"publisher","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Open-wbo: A modular maxsat solver,. In: Sinz, C., Egly, U. (eds.) 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Lecture Notes in Computer Science, vol. 8561, pp. 438\u2013445. Springer, Vienna, Austria (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"9749_CR33","doi-asserted-by":"publisher","unstructured":"Strichman, O.: Pruning techniques for the sat-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) 11th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001. Lecture Notes in Computer Science, vol. 2144, pp. 58\u201370. Springer, Livingston, Scotland, UK (2001). https:\/\/doi.org\/10.1007\/3-540-44798-9_4","DOI":"10.1007\/3-540-44798-9_4"},{"key":"9749_CR34","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: Strichman, O., Biere, A. (eds.) First International Workshop on Bounded Model Checking, BMC@CAV 2003, Boulder, Colorado, USA, July 13, 2003. Electronic Notes in Theoretical Computer Science, vol. 89, pp. 543\u2013560. Elsevier, Boulder, Colorado, USA (2003). https:\/\/doi.org\/10.1016\/S1571-0661(05)82542-3","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"9749_CR35","doi-asserted-by":"publisher","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) 15th International Conference on Theory and Applications of Satisfiability Testing - SAT 2012, Trento, Italy, June 17-20, 2012. Lecture Notes in Computer Science, vol. 7317, pp. 242\u2013255. Springer, Trento, Italy (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_19","DOI":"10.1007\/978-3-642-31612-8_19"},{"key":"9749_CR36","doi-asserted-by":"publisher","unstructured":"Audemard, G., Lagniez, J., Simon, L.: Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction. In: J\u00e4rvisalo, M., Gelder, A.V. (eds.) 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, July 8-12, 2013. Lecture Notes in Computer Science, vol. 7962, pp. 309\u2013317. Springer, Helsinki, Finland (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"9749_CR37","doi-asserted-by":"publisher","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J.H. (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. Springer, Perugia, Italy (2011). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_19","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"9749_CR38","doi-asserted-by":"publisher","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) 19th International Conference on Principles and Practice of Constraint Programming, CP 2013, Uppsala, Sweden, Setpember 16-20, 2013. Lecture Notes in Computer Science, vol. 8124, pp. 247\u2013262. Springer, Uppsala, Sweden (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_21","DOI":"10.1007\/978-3-642-40627-0_21"},{"key":"9749_CR39","doi-asserted-by":"publisher","unstructured":"Saikko, P., Berg, J., J\u00e4rvisalo, M.: LMHS: A SAT-IP hybrid maxsat solver. In: Creignou, N., Berre, D.L. (eds.) 19th International Conference on Theory and Applications of Satisfiability Testing - SAT 2016, Bordeaux, France, July 5-8, 2016. Lecture Notes in Computer Science, vol. 9710, pp. 539\u2013546. Springer, Bordeaux, France (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_34","DOI":"10.1007\/978-3-319-40970-2_34"},{"key":"9749_CR40","doi-asserted-by":"publisher","unstructured":"Berg, J., Bacchus, F., Poole, A.: Abstract cores in implicit hitting set maxsat solving. In: Pulina, L., Seidl, M. (eds.) 23rd International Conference on Theory and Applications of Satisfiability Testing - SAT 2020, Alghero, Italy, July 3-10, 2020. Lecture Notes in Computer Science, vol. 12178, pp. 277\u2013294. Springer, Alghero, Italy (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_20","DOI":"10.1007\/978-3-030-51825-7_20"},{"key":"9749_CR41","doi-asserted-by":"publisher","unstructured":"Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: International Conference on VLSI Design, pp. 37\u201342. IEEE Computer Society, Bangalore, India (2007). https:\/\/doi.org\/10.1109\/VLSID.2007.81","DOI":"10.1109\/VLSID.2007.81"},{"key":"9749_CR42","doi-asserted-by":"publisher","unstructured":"Manquinho, V.M., Silva, J.P.M., Planes, J.: Algorithms for weighted boolean optimization. In: International Conference on Theory and Applications of Satisfiability Testing. LNCS, vol. 5584, pp. 495\u2013508. Springer, Swansea, UK (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_45","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"9749_CR43","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gab\u00e0s, J., Levy, J.: Improving WPM2 for (weighted) partial maxsat. In: International Conference Principles and Practice of Constraint Programming. LNCS, vol. 8124, pp. 117\u2013132. Springer, Uppsala, Sweden (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_12","DOI":"10.1007\/978-3-642-40627-0_12"},{"key":"9749_CR44","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On Computing Minimal Correction Subsets. In: International Joint Conference on Artificial Intelligence, pp. 615\u2013622 (2013)"},{"key":"9749_CR45","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6695, pp. 159\u2013173. Springer, Ann Arbor, MI, USA (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_14","DOI":"10.1007\/978-3-642-21581-0_14"},{"issue":"2","key":"9749_CR46","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1287\/OPRE.1120.1139","volume":"61","author":"E Moreno-Centeno","year":"2013","unstructured":"Moreno-Centeno, E., Karp, R.M.: The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Oper. Res. 61(2), 453\u2013468 (2013). https:\/\/doi.org\/10.1287\/OPRE.1120.1139","journal-title":"Oper. Res."},{"key":"9749_CR47","unstructured":"Tamura, N., Banbara, M.: Sugar: A CSP to SAT translator based on order encoding. Proceedings of the Second International CSP Solver Competition, 65\u201369 (2008)"},{"key":"9749_CR48","doi-asserted-by":"publisher","unstructured":"Karpinski, M., Piotr\u00f3w, M.: Incremental encoding of pseudo-boolean goal functions based on comparator networks. In: International Conference on Theory and Applications of Satisfiability Testing. LNCS, vol. 12178, pp. 519\u2013535. Springer, Alghero, Italy (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_36","DOI":"10.1007\/978-3-030-51825-7_36"},{"issue":"1","key":"9749_CR49","doi-asserted-by":"publisher","first-page":"1840001","DOI":"10.1142\/S0218213018400018","volume":"27","author":"G Audemard","year":"2018","unstructured":"Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1840001\u20131184000125 (2018). https:\/\/doi.org\/10.1142\/S0218213018400018","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9749_CR50","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers. Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer, Santa Margherita Ligure, Italy (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9749_CR51","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Parrain, A.: The Sat4j Library, Release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7(2\u20133), 59\u20136 (2010)","DOI":"10.3233\/SAT190075"},{"key":"9749_CR52","doi-asserted-by":"publisher","unstructured":"Bieber, P., Delmas, R., Seguin, C.: Dalculus - theory and tool for development assurance level allocation. In: International Conference on Computer Safety, Reliability, and Security. LNCS, vol. 6894, pp. 43\u201356. Springer, Naples, Italy (2011). https:\/\/doi.org\/10.1007\/978-3-642-24270-0_4","DOI":"10.1007\/978-3-642-24270-0_4"},{"key":"9749_CR53","doi-asserted-by":"publisher","unstructured":"Bergman, D., Cir\u00e9, A.A.: Multiobjective optimization by decision diagrams. In: International Conference on Principles and Practice of Constraint Programming (CP). LNCS, vol. 9892, pp. 86\u201395. Springer, Toulouse, France (2016). https:\/\/doi.org\/10.1007\/978-3-319-44953-1_6","DOI":"10.1007\/978-3-319-44953-1_6"},{"issue":"1\/2","key":"9749_CR54","doi-asserted-by":"publisher","first-page":"89","DOI":"10.3233\/sat190090","volume":"8","author":"M Janota","year":"2012","unstructured":"Janota, M., Lynce, I., Manquinho, V.M., Marques-Silva, J.: Packup: Tools for package upgradability solving. J. Satisf. Boolean Model. Comput. 8(1\/2), 89\u201394 (2012). https:\/\/doi.org\/10.3233\/sat190090","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9749_CR55","unstructured":"Development Assurance Level Benchmark Set from the LION Challenge. https:\/\/www.cristal.univ-lille.fr\/LION9\/challenge.html"},{"key":"9749_CR56","unstructured":"Benchmarks from the Mancoosi International Solver Competition 2011. http:\/\/data.mancoosi.org\/misc2011\/problems\/"},{"key":"9749_CR57","unstructured":"Mancoosi International Solver Competition 2011. https:\/\/www.mancoosi.org\/misc-2011\/index.html"},{"key":"9749_CR58","unstructured":"packup package upgradeability solver webpage. https:\/\/sat.inesc-id.pt\/~mikolas\/sw\/packup\/"},{"key":"9749_CR59","unstructured":"Zitzler, E.: Evolutionary Algorithms for Multiobjective Optimization: Methods and Applications. PhD thesis, University of Zurich, Z\u00fcrich, Switzerland (1999)"},{"issue":"4","key":"9749_CR60","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1109\/TEVC.2013.2281535","volume":"18","author":"K Deb","year":"2014","unstructured":"Deb, K., Jain, H.: An evolutionary many-objective optimization algorithm using reference-point-based nondominated sorting approach, part I: solving problems with box constraints. IEEE Trans. Evol. Comput. 18(4), 577\u2013601 (2014). https:\/\/doi.org\/10.1109\/TEVC.2013.2281535","journal-title":"IEEE Trans. Evol. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09749-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-026-09749-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09749-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T10:57:32Z","timestamp":1771239452000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-026-09749-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,16]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["9749"],"URL":"https:\/\/doi.org\/10.1007\/s10817-026-09749-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,16]]},"assertion":[{"value":"19 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 January 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"3"}}