{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:41:03Z","timestamp":1764402063162,"version":"3.46.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Due to the wide employment of automated reasoning\u00a0in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers\u2014and more recently SAT-based maximum satisfiability (MaxSAT) solvers\u2014trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first\u00a0time proof logging based on the\n                    <jats:sc>VeriPB<\/jats:sc>\n                    proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although\n                    <jats:sc>VeriPB<\/jats:sc>\n                    does not offer direct support for multi-objective problems, we detail how preorders in\n                    <jats:sc>VeriPB<\/jats:sc>\n                    can be\u00a0used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto optimality, without extending the\n                    <jats:sc>VeriPB<\/jats:sc>\n                    format or the proof checker. By implementing\n                    <jats:sc>VeriPB<\/jats:sc>\n                    proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_6","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:23:18Z","timestamp":1746174198000},"page":"108-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Certifying Pareto Optimality in Multi-objective Maximum Satisfiability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3532-696X","authenticated-orcid":false,"given":"Christoph","family":"Jabs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7660-8061","authenticated-orcid":false,"given":"Jeremias","family":"Berg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3460-4251","authenticated-orcid":false,"given":"Bart","family":"Bogaerts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2572-063X","authenticated-orcid":false,"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"6_CR1","unstructured":"VeriPB: Verifier for pseudo-Boolean proofs. https:\/\/gitlab.com\/MIAOresearch\/software\/VeriPB"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary. LIPIcs, vol.\u00a017, pp. 211\u2013221. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPIcs.ICLP.2012.211","DOI":"10.4230\/LIPIcs.ICLP.2012.211"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Bacchus, F., J\u00e4rvisalo, M., Martins, R.: Maximum satisfiabiliy. In: Biere et\u00a0al. [9], pp. 929\u2013991. https:\/\/doi.org\/10.3233\/FAIA201008","DOI":"10.3233\/FAIA201008"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective queries in markov decision processes. In: Hillston, J., Soudjani, S., Waga, M. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9-13, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14996, pp. 1\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-68416-6_1","DOI":"10.1007\/978-3-031-68416-6_1"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Principles and Practice of Constraint Programming \u2013 CP 2003, pp. 108\u2013122. Springer Berlin Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Paxian, T., Vandesande, D.: Certifying without loss of generality reasoning in solution-improving maximum satisfiability. In: Shaw [49], pp. 4:1\u20134:28. https:\/\/doi.org\/10.4230\/LIPICS.CP.2024.4","DOI":"10.4230\/LIPICS.CP.2024.4"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Vandesande, D.: Certified core-guided MaxSAT solving. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 1\u201322. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1","DOI":"10.1007\/978-3-031-38499-8_1"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023). https:\/\/doi.org\/10.1613\/jair.1.14296","DOI":"10.1613\/jair.1.14296"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Cabral, M., Janota, M., Manquinho, V.: SAT-based leximax optimisation algorithms. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2\u20135, 2022, Haifa, Israel. LIPIcs, vol.\u00a0236, pp. 29:1\u201329:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2022.29","DOI":"10.4230\/LIPICS.SAT.2022.29"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Cook, W.J., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discret. Appl. Math. 18(1), 25\u201338 (1987). https:\/\/doi.org\/10.1016\/0166-218X(87)90039-4","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Cortes, J.a., Lynce, I., Manquinho, V.: Slide &Drill, a New Approach for Multi-Objective Combinatorial Optimization. In: Shaw, P. (ed.) 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0307, pp. 8:1\u20138:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2024.8","DOI":"10.4230\/LIPIcs.CP.2024.8"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Cortes, J., Lynce, I., Manquinho, V.M.: 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\u201429th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22\u201327, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 55\u201373. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_7","DOI":"10.1007\/978-3-031-30820-8_7"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 220\u2013236. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 118\u2013135 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7","DOI":"10.1007\/978-3-662-54577-5_7"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Demirovic, E., McCreesh, C., McIlree, M.J., Nordstr\u00f6m, J., Oertel, A., Sidorov, K.: Pseudo-Boolean reasoning about states and transitions to certify dynamic programming and decision diagram algorithms. In: Shaw [49], pp. 9:1\u20139:21. https:\/\/doi.org\/10.4230\/LIPICS.CP.2024.9","DOI":"10.4230\/LIPICS.CP.2024.9"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Demirovic, E., Musliu, N., Winter, F.: Modeling and solving staff scheduling with partial weighted maxSAT. Ann. Oper. Res. 275(1), 79\u201399 (2019). https:\/\/doi.org\/10.1007\/S10479-017-2693-Y","DOI":"10.1007\/S10479-017-2693-Y"},{"key":"6_CR19","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.\u00a02919, pp. 502\u2013518. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput. 2(1-4), 1\u201326 (2006). https:\/\/doi.org\/10.3233\/sat190014","DOI":"10.3233\/sat190014"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Ehrgott, M.: Multicriteria Optimization (2. ed.). Springer (2005). https:\/\/doi.org\/10.1007\/3-540-27659-9","DOI":"10.1007\/3-540-27659-9"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Justifying all differences using pseudo-Boolean reasoning. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. pp. 1486\u20131494. AAAI Press (2020), https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/5507","DOI":"10.1609\/aaai.v34i02.5507"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Gocht, S., Martins, R., Nordstr\u00f6m, J., Oertel, A.: Certified CNF translations for pseudo-Boolean solving. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel. LIPIcs, vol.\u00a0236, pp. 16:1\u201316:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.16","DOI":"10.4230\/LIPIcs.SAT.2022.16"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Gocht, S., McBride, R., McCreesh, C., Nordstr\u00f6m, J., Prosser, P., Trimble, J.: Certifying solvers for clique and maximum common (connected) subgraph problems. In: Simonis, H. (ed.) Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12333, pp. 338\u2013357. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_20","DOI":"10.1007\/978-3-030-58475-7_20"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Subgraph isomorphism meets cutting planes: Solving with certified solutions. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020. pp. 1134\u20131140. ijcai.org (2020). https:\/\/doi.org\/10.24963\/ijcai.2020\/158, scheduled for July 2020, Yokohama, Japan, postponed due to the Corona pandemic","DOI":"10.24963\/ijcai.2020\/158"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: An auditable constraint programming solver. In: Solnon, C. (ed.) 28th International Conference on Principles and Practice of Constraint Programming, CP 2022, July 31 to August 8, 2022, Haifa, Israel. LIPIcs, vol.\u00a0235, pp. 25:1\u201325:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2022.25","DOI":"10.4230\/LIPIcs.CP.2022.25"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021. pp. 3768\u20133777. AAAI Press (2021), https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/16494","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany. pp. 10886\u201310891. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/DATE.2003.10008","DOI":"10.1109\/DATE.2003.10008"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Guerreiro, A.P., Cortes, J., Vanderpooten, D., Bazgan, C., Lynce, I., Manquinho, V., 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","DOI":"10.1016\/J.COR.2023.106153"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr., W.A.H., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 181\u2013188. IEEE (2013), https:\/\/ieeexplore.ieee.org\/document\/6679408\/","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Heule, M., Jr., W.A.H., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07898, pp. 345\u2013359. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_24","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Hoen, A., Oertel, A., Gleixner, A.M., Nordstr\u00f6m, J.: Certifying MIP-based presolve reductions for 0-1 integer linear programs. In: Dilkina, B. (ed.) Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14742, pp. 310\u2013328. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-60597-0_20","DOI":"10.1007\/978-3-031-60597-0_20"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Ihalainen, H., Oertel, A., Tan, Y.K., Berg, J., J\u00e4rvisalo, M., Myreen, M.O., Nordstr\u00f6m, J.: Certified MaxSAT preprocessing. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14739, pp. 396\u2013418. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_24","DOI":"10.1007\/978-3-031-63498-7_24"},{"key":"6_CR34","unstructured":"Jabs, C.: Scuttle: A multi-objective MaxSAT solver. https:\/\/bitbucket.org\/coreo-group\/scuttle"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Jabs, C., Berg, J., Bogaerts, B., J\u00e4rvisalo, M.: Certifying pareto optimality in multi-objective maximum satisfiability. CoRR abs\/2501.17493 (2025). https:\/\/doi.org\/10.48550\/arXiv.2501.17493, https:\/\/arxiv.org\/abs\/2501.17493","DOI":"10.48550\/arXiv.2501.17493"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Jabs, C., Berg, J., Ihalainen, H., J\u00e4rvisalo, M.: Preprocessing in SAT-based multi-objective combinatorial optimization. In: Yap, R.H.C. (ed.) 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada. LIPIcs, vol.\u00a0280, pp. 18:1\u201318:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CP.2023.18","DOI":"10.4230\/LIPICS.CP.2023.18"},{"key":"6_CR37","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 - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 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":"6_CR38","doi-asserted-by":"publisher","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 (Aug 2024). https:\/\/doi.org\/10.1613\/jair.1.15333","DOI":"10.1613\/jair.1.15333"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Jabs, C., Berg, J., Bogaerts, B., J\u00e4rvisalo, M.: Certifying pareto optimality in multi-objective maximum satisfiability\u2014TACAS 2025 artefact (Jan 2025). https:\/\/doi.org\/10.5281\/zenodo.14731485","DOI":"10.5281\/zenodo.14731485"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"Janota, M., Lynce, I., Manquinho, V., 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":"6_CR41","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07364, pp. 355\u2013370. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"Joshi, S., Martins, R., Manquinho, V.M.: 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.\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":"6_CR43","doi-asserted-by":"publisher","unstructured":"Karpinski, M., Piotr\u00f3w, M.: Encoding cardinality constraints using multiway merge selection networks. Constraints An Int. J. 24(3-4), 234\u2013251 (2019). https:\/\/doi.org\/10.1007\/S10601-019-09302-0","DOI":"10.1007\/S10601-019-09302-0"},{"key":"6_CR44","unstructured":"Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, July 6-7, 2009. CEUR Workshop Proceedings, vol.\u00a0556. CEUR-WS.org (2009), http:\/\/ceur-ws.org\/Vol-556\/paper06.pdf"},{"key":"6_CR45","doi-asserted-by":"publisher","unstructured":"Malioutov, D., Meel, K.S.: MLIC: A maxsat-based framework for learning interpretable classification rules. In: Hooker, J.N. (ed.) Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27\u201331, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11008, pp. 312\u2013327. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_21","DOI":"10.1007\/978-3-319-98334-9_21"},{"key":"6_CR46","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et\u00a0al. [9], pp. 133\u2013182. https:\/\/doi.org\/10.3233\/FAIA200987","DOI":"10.3233\/FAIA200987"},{"key":"6_CR47","doi-asserted-by":"publisher","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: Lecture Notes in Computer Science, pp. 531\u2013548. Springer International Publishing (aug 2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_39","DOI":"10.1007\/978-3-319-10428-7_39"},{"key":"6_CR48","doi-asserted-by":"publisher","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O\u2019Sullivan, B. (ed.) Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08656, pp. 564\u2013573. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_41","DOI":"10.1007\/978-3-319-10428-7_41"},{"key":"6_CR49","unstructured":"Shaw, P. (ed.): 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, LIPIcs, vol.\u00a0307. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"6_CR50","doi-asserted-by":"publisher","unstructured":"Soh, T., Banbara, M., Tamura, N., Le\u00a0Berre, D.: Solving multiobjective discrete optimization problems with propositional minimal model generation. In: Beck, J.C. (ed.) Principles and Practice of Constraint Programming\u201423rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 \u2013 September 1, 2017, Proceedings. Lecture Notes in Computer Science, 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":"6_CR51","doi-asserted-by":"publisher","unstructured":"Terra-Neves, M., Lynce, I., Manquinho, V.: Multi-objective optimization through pareto minimal correction subsets. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization (jul 2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/757","DOI":"10.24963\/ijcai.2018\/757"},{"key":"6_CR52","unstructured":"Vandesande, D.: Towards Certified MaxSAT Solving: Certified MaxSAT solving with SAT oracles and encodings of pseudo-Boolean constraints. Master\u2019s thesis, Vrije Universiteit Brussel (VUB) (2023), https:\/\/researchportal.vub.be\/nl\/studentTheses\/towards-certified-maxsat-solving"},{"key":"6_CR53","doi-asserted-by":"publisher","unstructured":"Vandesande, D., De Wulf, W., Bogaerts, B.: QMaxSATpb: A certified MaxSAT solver. In: Gottlob, G., Inclezan, D., Maratea, M. (eds.) Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13416, pp. 429\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-15707-3_33","DOI":"10.1007\/978-3-031-15707-3_33"}],"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-90653-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:32Z","timestamp":1764401792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}