{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:36Z","timestamp":1771262196269,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\nIn 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 still scarce. Due to this shortage of efficient tools for MOCO, many real-world applications formulated as multi-objective are simplified to single-objective, using either a linear combination or a lexicographic ordering of the objective functions to optimize.<\/jats:p><jats:p>In this paper, we extend the state of the art of MOCO solvers with two novel unsatisfiability-based algorithms. The first is a core-guided MOCO solver. The second is a hitting set-based MOCO solver. Experimental results in several sets of benchmark instances show that our new unsatisfiability-based algorithms can outperform state-of-the-art SAT-based algorithms for MOCO.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_7","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"55-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization"],"prefix":"10.1007","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":[[2023,4,20]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","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.\u00a08124, pp. 117\u2013132. Springer (2013), https:\/\/doi.org\/10.1007\/978-3-642-40627-0_12","DOI":"10.1007\/978-3-642-40627-0_12"},{"key":"7_CR2","doi-asserted-by":"crossref","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.\u00a05584, pp. 427\u2013440. Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-02777-2_39","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"7_CR3","doi-asserted-by":"crossref","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.\u00a02833, pp. 108\u2013122. Springer (2003), https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"7_CR4","doi-asserted-by":"crossref","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.\u00a09892, pp. 86\u201395. Springer (2016), https:\/\/doi.org\/10.1007\/978-3-319-44953-1_6","DOI":"10.1007\/978-3-319-44953-1_6"},{"key":"7_CR5","doi-asserted-by":"crossref","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.\u00a06894, pp. 43\u201356. Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-24270-0_4","DOI":"10.1007\/978-3-642-24270-0_4"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Deb, K., Agrawal, S., Pratap, A., Meyarivan, T.: A Fast Elitist Non-dominated Sorting Genetic Algorithm for Multi-objective Optimisation: NSGA-II. In: International Conference on Parallel Problem Solving from Nature. pp. 849\u2013858. Springer (2000)","DOI":"10.1007\/3-540-45356-3_83"},{"key":"7_CR7","doi-asserted-by":"crossref","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 (2007), https:\/\/doi.org\/10.1109\/VLSID.2007.81","DOI":"10.1109\/VLSID.2007.81"},{"key":"7_CR8","unstructured":"Gavanelli, M.: An algorithm for multi-criteria optimization in csps. In: European Conference on Artificial Intelligence. pp. 136\u2013140. IOS Press (2002)"},{"key":"7_CR9","doi-asserted-by":"crossref","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","DOI":"10.1016\/j.cor.2021.105471"},{"key":"7_CR10","unstructured":"Jabs, C., Berg, J., Niskanen, A., J\u00e4rvisalo, M.: Maxsat-based bi-objective boolean optimization. In: International Conference on Theory and Applications of Satisfiability Testing. LIPIcs, vol.\u00a0236, pp. 12:1\u201312:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022), https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.12"},{"key":"7_CR11","doi-asserted-by":"crossref","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","DOI":"10.3233\/SAT190090"},{"key":"7_CR12","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.\u00a0210, pp. 31:1\u201331:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021), https:\/\/doi.org\/10.4230\/LIPIcs.CP.2021.31"},{"key":"7_CR13","doi-asserted-by":"crossref","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.\u00a09255, pp. 200\u2013209. Springer (2015), https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15","DOI":"10.1007\/978-3-319-23219-5_15"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Karpinski, M., Piotr\u00f3w, M.: Encoding cardinality constraints using multiway merge selection networks. Constraints 24(3-4), 234\u2013251 (2019), https:\/\/doi.org\/10.1007\/s10601-019-09302-0","DOI":"10.1007\/s10601-019-09302-0"},{"key":"7_CR15","doi-asserted-by":"crossref","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 (2020), https:\/\/doi.org\/10.1007\/978-3-030-51825-7_36","DOI":"10.1007\/978-3-030-51825-7_36"},{"key":"7_CR16","doi-asserted-by":"crossref","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.\u00a06015, pp. 69\u201383. Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-12002-2_6","DOI":"10.1007\/978-3-642-12002-2_6"},{"key":"7_CR17","doi-asserted-by":"crossref","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","DOI":"10.1016\/j.future.2017.08.027"},{"key":"7_CR18","unstructured":"Development Assurance Level Benchmark Set from the LION Challenge. https:\/\/www.lifl.fr\/LION9\/challenge.php"},{"key":"7_CR19","unstructured":"Benchmarks from the Mancoosi International Solver Competition 2011. http:\/\/data.mancoosi.org\/misc2011\/problems\/"},{"key":"7_CR20","unstructured":"Mancoosi international solver competition 2011. https:\/\/www.mancoosi.org\/misc-2011\/index.html"},{"key":"7_CR21","doi-asserted-by":"crossref","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.\u00a05584, pp. 495\u2013508. Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-02777-2_45","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"7_CR22","doi-asserted-by":"crossref","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","DOI":"10.1016\/j.eswa.2019.04.024"},{"key":"7_CR23","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR abs\/0712.1097 (2007), http:\/\/arxiv.org\/abs\/0712.1097"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Argelich, J., Gra\u00e7a, A., Lynce, I.: Boolean lexicographic optimization: Algorithms & applications. Ann. Math. Artif. Intell. 62, 317\u2013343 (07 2011). https:\/\/doi.org\/10.1007\/s10472-011-9233-2","DOI":"10.1007\/s10472-011-9233-2"},{"key":"7_CR25","unstructured":"packup package upgradeability solver webpage. http:\/\/sat.inesc-id.pt\/~mikolas\/sw\/packup\/"},{"key":"7_CR26","unstructured":"Rayside, D., Estler, H.C., Jackson, D.: The guided improvement algorithm for exact, general-purpose, many-objective combinatorial optimization. Tech. Rep. Technical Report MIT-CSAIL-TR-2009-033, MIT Massachusetts Institute of Technology (2009)"},{"key":"7_CR27","unstructured":"Roussel, O., Manquinho, V.M.: Pseudo-boolean and cardinality constraints. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 695\u2013733. IOS Press (2009), https:\/\/doi.org\/10.3233\/978-1-58603-929-5-695"},{"key":"7_CR28","doi-asserted-by":"crossref","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 (2017), https:\/\/doi.org\/10.1007\/978-3-319-66158-2_38","DOI":"10.1007\/978-3-319-66158-2_38"},{"key":"7_CR29","unstructured":"Tamura, N., Banbara, M.: Sugar: A CSP to SAT translator based on order encoding. Proceedings of the Second International CSP Solver Competition pp. 65\u201369 (2008)"},{"key":"7_CR30","doi-asserted-by":"crossref","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 (2017), https:\/\/doi.org\/10.1007\/978-3-319-66263-3_13","DOI":"10.1007\/978-3-319-66263-3_13"},{"key":"7_CR31","doi-asserted-by":"crossref","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","DOI":"10.1007\/s10489-020-01998-5"},{"key":"7_CR32","doi-asserted-by":"crossref","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","DOI":"10.1109\/TSE.2018.2874648"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Li, H.: MOEA\/D: A Multiobjective Evolutionary Algorithm Based on Decomposition. IEEE Transactions on Evolutionary Computation 11(6), 712\u2013731 (2007)","DOI":"10.1109\/TEVC.2007.892759"},{"key":"7_CR34","unstructured":"Zitzler, E.: Evolutionary Algorithms for Multiobjective Optimization: Methods and Applications. Ph.D. thesis, University of Zurich, Z\u00fcrich, Switzerland (1999)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:03:15Z","timestamp":1690974195000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}