{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T23:51:05Z","timestamp":1769730665583,"version":"3.49.0"},"publisher-location":"Cham","reference-count":76,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031384981","type":"print"},{"value":"9783031384998","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,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"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>In the last couple of decades, developments in SAT-based optimization have led to highly efficient maximum satisfiability (MaxSAT) solvers, but in contrast to the SAT solvers on which MaxSAT solving rests, there has been little parallel development of techniques to prove the correctness of MaxSAT results. We show how pseudo-Boolean proof logging can be used to certify state-of-the-art core-guided MaxSAT solving, including advanced techniques like structure sharing, weight-aware core extraction and hardening. Our experimental evaluation demonstrates that this approach is viable in practice. We are hopeful that this is the first step towards general proof logging techniques for MaxSAT solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_1","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Certified Core-Guided MaxSAT Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7660-8061","authenticated-orcid":false,"given":"Jeremias","family":"Berg","sequence":"first","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-0002-2700-4285","authenticated-orcid":false,"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9783-6768","authenticated-orcid":false,"given":"Andy","family":"Oertel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8150-3202","authenticated-orcid":false,"given":"Dieter","family":"Vandesande","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-38189-8_18","volume-title":"Facets of Combinatorial Optimization","author":"T Achterberg","year":"2013","unstructured":"Achterberg, T., Wunderling, R.: Mixed integer programming: analyzing 12 years of progress. In: J\u00fcnger, M., Reinelt, G. (eds.) Facets of Combinatorial Optimization, pp. 449\u2013481. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38189-8_18"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-319-98334-9_46","volume-title":"Principles and Practice of Constraint Programming","author":"\u00d6 Akg\u00fcn","year":"2018","unstructured":"Akg\u00fcn, \u00d6., Gent, I.P., Jefferson, C., Miguel, I., Nightingale, P.: Metamorphic testing of constraint solvers. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 727\u2013736. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_46"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C., Schweitzer, P.: An introduction to certifying algorithms. IT - Inf. Technol. Methoden Innov. Anwendungen Inform. Informationstechnik 53(6), 287\u2013293 (2011)","DOI":"10.1524\/itit.2011.0655"},{"key":"1_CR4","unstructured":"Alviano, M., Dodaro, C., Ricca, F.: A MaxSAT algorithm using cardinality constraints of bounded size. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 2677\u20132683. AAAI Press (2015)"},{"key":"1_CR5","unstructured":"Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012). Leibniz International Proceedings in Informatics (LIPIcs), vol. 17, pp. 211\u2013221 (2012)"},{"key":"1_CR6","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, pp. 86\u2013101. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_9"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.artint.2017.05.003","volume":"250","author":"C Ans\u00f3tegui","year":"2017","unstructured":"Ans\u00f3tegui, C., Gab\u00e0s, J.: WPM3: an (in)complete algorithm for weighted partial MaxSAT. Artif. Intell. 250, 37\u201357 (2017)","journal-title":"Artif. Intell."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bacchus, F., J\u00e4rvisalo, M., Martins, R.: Maximum satisfiabiliy. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 2nd edn., vol. 336, pp. 929\u2013991. IOS Press (2021)","DOI":"10.3233\/FAIA201008"},{"key":"1_CR9","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). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8"},{"key":"1_CR10","unstructured":"Barth, P.: A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Technical report MPI-I-95-2-003, Max-Planck-Institut f\u00fcr Informatik (1995)"},{"key":"1_CR11","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203\u2013208 (1997)"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Vandesande, D.: Experimental repository for \u201cCertified core-guided MaxSAT solving\u201d (2023). https:\/\/doi.org\/10.5281\/zenodo.7709687","DOI":"10.5281\/zenodo.7709687"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-319-66158-2_42","volume-title":"Principles and Practice of Constraint Programming","author":"J Berg","year":"2017","unstructured":"Berg, J., J\u00e4rvisalo, M.: Weight-aware core extraction in SAT-based MaxSAT solving. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 652\u2013670. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_42"},{"key":"1_CR14","unstructured":"Biere, A.: Tracecheck (2006). http:\/\/fmv.jku.at\/tracecheck\/"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 2nd edn., vol. 336. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"issue":"1","key":"1_CR16","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10479-006-0091-y","volume":"149","author":"R Bixby","year":"2007","unstructured":"Bixby, R., Rothberg, E.: Progress in computational mixed integer programming\u2013a look back from the other side of the tipping point. Ann. Oper. Res. 149(1), 37\u201341 (2007)","journal-title":"Ann. Oper. Res."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified symmetry and dominance breaking for combinatorial optimisation. In: Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI 2022), pp. 3698\u20133707 (2022)","DOI":"10.1609\/aaai.v36i4.20283"},{"key":"1_CR18","unstructured":"Bogaerts, B., McCreesh, C., Nordstr\u00f6m, J.: Solving with provably correct results: beyond satisfiability, and towards constraint programming (2022). Tutorial at the 28th International Conference on Principles and Practice of Constraint Programming. Slides available at http:\/\/www.jakobnordstrom.se\/presentations\/"},{"issue":"8\u20139","key":"1_CR19","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","volume":"171","author":"ML Bonet","year":"2007","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for max-SAT. Artif. Intell. 171(8\u20139), 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Buss, S.R., Nordstr\u00f6m, J.: Proof complexity and SAT solving. In: Biere et al. [15], chap. 7, pp. 233\u2013350 (2021)","DOI":"10.3233\/FAIA200990"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-11269-0_6","volume-title":"Parameterized and Exact Computation","author":"C Calabro","year":"2009","unstructured":"Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 75\u201385. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-11269-0_6"},{"key":"1_CR22","unstructured":"Certifying version of the CGSS core-guided MaxSAT solver with structure sharing. https:\/\/gitlab.com\/MIAOresearch\/software\/certified-cgss"},{"key":"1_CR23","unstructured":"CGSS, a core guided Max-SAT-algorithm using structure sharing technique for enhanced cardinality constraints, built on RC2 and PySAT. https:\/\/bitbucket.org\/coreo-group\/cgss\/"},{"issue":"1","key":"1_CR24","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discret. Appl. Math. 18(1), 25\u201338 (1987)","journal-title":"Discret. Appl. Math."},{"issue":"3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/s12532-013-0055-6","volume":"5","author":"W Cook","year":"2013","unstructured":"Cook, W., Koch, T., Steffy, D.E., Wolter, K.: A hybrid branch-and-bound approach for exact rational mixed-integer programming. Math. Program. Comput. 5(3), 305\u2013344 (2013)","journal-title":"Math. Program. Comput."},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-662-54577-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-39071-5_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166\u2013181. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_13"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-40627-0_21","volume-title":"Principles and Practice of Constraint Programming","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247\u2013262. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_21"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Devriendt, J., Gocht, S., Demirovi\u0107, E., Nordstr\u00f6m, J., Stuckey, P.: Cutting to the core of pseudo-Boolean optimization: combining core-guided search with cutting planes reasoning. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), pp. 3750\u20133758 (2021)","DOI":"10.1609\/aaai.v35i5.16492"},{"issue":"1\u20134","key":"1_CR31","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. J. Satisfiab. Boolean Model. Comput. 2(1\u20134), 1\u201326 (2006)","journal-title":"J. Satisfiab. Boolean Model. Comput."},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-030-73879-2_12","volume-title":"Integer Programming and Combinatorial Optimization","author":"L Eifler","year":"2021","unstructured":"Eifler, L., Gleixner, A.: A computational status update for exact rational mixed integer programming. In: Singh, M., Williamson, D.P. (eds.) IPCO 2021. LNCS, vol. 12707, pp. 163\u2013177. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-73879-2_12"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Justifying all differences using pseudo-Boolean reasoning. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), pp. 1486\u20131494 (2020)","DOI":"10.1609\/aaai.v34i02.5507"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-030-51825-7_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"Y Filmus","year":"2020","unstructured":"Filmus, Y., Mahajan, M., Sood, G., Vinyals, M.: MaxSAT resolution and subcube sums. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 295\u2013311. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_21"},{"key":"1_CR35","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. 4121, pp. 252\u2013265. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_25"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-030-58942-4_14","volume-title":"Integration of Constraint Programming, Artificial Intelligence, and Operations Research","author":"G Gange","year":"2020","unstructured":"Gange, G., Berg, J., Demirovi\u0107, E., Stuckey, P.J.: Core-guided and core-boosted search for CP. In: Hebrard, E., Musliu, N. (eds.) CPAIOR 2020. LNCS, vol. 12296, pp. 205\u2013221. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58942-4_14"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-030-30048-7_33","volume-title":"Principles and Practice of Constraint Programming","author":"X Gillard","year":"2019","unstructured":"Gillard, X., Schaus, P., Deville, Y.: SolverCheck: declarative testing of constraints. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 565\u2013582. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_33"},{"key":"1_CR38","unstructured":"Gocht, S., Martins, R., Nordstr\u00f6m, J., Oertel, A.: Certified CNF translations for pseudo-Boolean solving. In: Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp. 16:1\u201316:25 (2022)"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-030-58475-7_20","volume-title":"Principles and Practice of Constraint Programming","author":"S Gocht","year":"2020","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.) CP 2020. LNCS, vol. 12333, pp. 338\u2013357. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_20"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Subgraph isomorphism meets cutting planes: solving with certified solutions. In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI 2020), pp. 1134\u20131140 (2020)","DOI":"10.24963\/ijcai.2020\/158"},{"key":"1_CR41","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: An auditable constraint programming solver. In: Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 235, pp. 25:1\u201325:18 (2022)"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), pp. 3768\u20133777 (2021)","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2003), pp. 886\u2013891 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), pp. 181\u2013188 (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345\u2013359. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_24"},{"issue":"1","key":"1_CR46","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/SAT190116","volume":"11","author":"A Ignatiev","year":"2019","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.P.: RC2: an efficient MaxSAT solver. J. Satisfiab. Boolean Model. Comput. 11(1), 53\u201364 (2019)","journal-title":"J. Satisfiab. Boolean Model. Comput."},{"key":"1_CR47","unstructured":"Ihalainen, H., Berg, J., J\u00e4rvisalo, M.: Refined core relaxation for core-guided MaxSAT solving. In: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 210, pp. 28:1\u201328:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-031-10769-6_6","volume-title":"Automated Reasoning","author":"H Ihalainen","year":"2022","unstructured":"Ihalainen, H., Berg, J., J\u00e4rvisalo, M.: Clause redundancy and preprocessing in maximum satisfiability. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 75\u201394. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_6"},{"issue":"2","key":"1_CR49","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1006\/jcss.2000.1727","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of $$k$$-SAT. J. Comput. Syst. Sci. 62(2), 367\u2013375 (2001). Preliminary version in CCC 1999","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Karpinski, M., Piotr\u00f3w, M.: Competitive sorter-based encoding of PB-constraints into SAT. In: Proceedings of Pragmatics of SAT. EPiC Series in Computing, vol. 59, pp. 65\u201378. EasyChair (2018)","DOI":"10.29007\/hh3v"},{"issue":"3\u20134","key":"1_CR51","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)","journal-title":"Constraints"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Kraiczy, S., McCreesh, C.: Solving graph homomorphism and subgraph isomorphism problems faster through clique neighbourhood constraints. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI 2021), pp. 1396\u20131402 (2021)","DOI":"10.24963\/ijcai.2021\/193"},{"issue":"1","key":"1_CR53","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10817-010-9176-z","volume":"46","author":"J Larrosa","year":"2011","unstructured":"Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: A framework for certified Boolean branch-and-bound optimization. J. Autom. Reason. 46(1), 81\u2013102 (2011)","journal-title":"J. Autom. Reason."},{"key":"1_CR54","doi-asserted-by":"publisher","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. J. Satisfiab. Boolean Model. Comput. 7, 59\u201364 (2010)","journal-title":"J. Satisfiab. Boolean Model. Comput."},{"key":"1_CR55","unstructured":"Leivo, M., Berg, J., J\u00e4rvisalo, M.: Preprocessing in incomplete MaxSAT solving. In: Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 347\u2013354. IOS Press (2020)"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, hard and soft constraints. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 903\u2013927. IOS Press (2021)","DOI":"10.3233\/FAIA201007"},{"issue":"2","key":"1_CR57","doi-asserted-by":"publisher","first-page":"131","DOI":"10.3233\/AIC-210178","volume":"35","author":"C Li","year":"2022","unstructured":"Li, C., Xu, Z., Coll, J., Many\u00e0, F., Habet, D., He, K.: Boosting branch-and-bound MaxSAT solvers with clause learning. AI Commun. 35(2), 131\u2013151 (2022)","journal-title":"AI Commun."},{"issue":"3\u20134","key":"1_CR58","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(3\u20134), 317\u2013343 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"5","key":"1_CR59","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999). Preliminary version in ICCAD 1996","journal-title":"IEEE Trans. Comput."},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_39"},{"key":"1_CR61","unstructured":"MaxSAT evaluation 2022 (2022). https:\/\/maxsat-evaluations.github.io\/2022"},{"issue":"2","key":"1_CR62","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"1_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-10428-7_41","volume-title":"Principles and Practice of Constraint Programming","author":"A Morgado","year":"2014","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564\u2013573. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_41"},{"key":"1_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-030-24258-9_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"A Morgado","year":"2019","unstructured":"Morgado, A., Ignatiev, A., Bonet, M.L., Marques-Silva, J., Buss, S.: DRMaxSAT with MaxHS: first contact. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 239\u2013249. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_17"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Morgado, A., Marques-Silva, J.: On validating Boolean optimizers. In: Proceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence, (ICTAI 2011), pp. 924\u2013926 (2011)","DOI":"10.1109\/ICTAI.2011.157"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI 2014), pp. 2717\u20132723. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"1_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-94144-8_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"T Paxian","year":"2018","unstructured":"Paxian, T., Reimer, S., Becker, B.: Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 37\u201353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_3"},{"key":"1_CR69","doi-asserted-by":"crossref","unstructured":"Py, M., Cherif, M.S., Habet, D.: Towards bridging the gap between SAT and Max-SAT refutations. In: Proceedings of the 32nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2020), pp. 137\u2013144 (2020)","DOI":"10.1109\/ICTAI50040.2020.00032"},{"key":"1_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-80223-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"M Py","year":"2021","unstructured":"Py, M., Cherif, M.S., Habet, D.: A proof builder for Max-SAT. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 488\u2013498. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_33"},{"key":"1_CR71","doi-asserted-by":"publisher","first-page":"1373","DOI":"10.1613\/jair.1.13811","volume":"75","author":"M Py","year":"2022","unstructured":"Py, M., Cherif, M.S., Habet, D.: Proofs and certificates for Max-SAT. J. Artif. Intell. Res. 75, 1373\u20131400 (2022)","journal-title":"J. Artif. Intell. Res."},{"key":"1_CR72","volume-title":"Handbook of Constraint Programming, Foundations of Artificial Intelligence","year":"2006","unstructured":"Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol. 2. Elsevier, Amsterdam (2006)"},{"key":"1_CR73","unstructured":"Smirnov, P., Berg, J., J\u00e4rvisalo, M.: Improvements to the implicit hitting set approach to pseudo-Boolean optimization. In: Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp. 13:1\u201313:18 (2022)"},{"key":"1_CR74","unstructured":"Smirnov, P., Berg, J., J\u00e4rvisalo, M.: Pseudo-Boolean optimization by implicit hitting sets. In: Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 210, pp. 51:1\u201351:20 (2021)"},{"key":"1_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-031-15707-3_33","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"D Vandesande","year":"2022","unstructured":"Vandesande, D., De Wulf, W., Bogaerts, B.: QMaxSATpb: a certified MaxSAT solver. In: Gottlob, G., Inclezan, D., Maratea, M. (eds.) LPNMR 2022. LNCS, vol. 13416, pp. 429\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15707-3_33"},{"key":"1_CR76","unstructured":"VeriPB: Verifier for pseudo-Boolean proofs. https:\/\/gitlab.com\/MIAOresearch\/software\/VeriPB"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T10:36:10Z","timestamp":1730025370000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":76,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1","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":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 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":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"77","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":"28","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":"5","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":"36% - 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":"6","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)"}}]}}