{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:38:23Z","timestamp":1769740703339,"version":"3.49.0"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving -hard optimization problems. However, ensuring correctness of MaxSAT solvers has remained a considerable concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper.<\/jats:p>\n          <jats:p>In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the <jats:sc>VeriPB<\/jats:sc> and <jats:sc>CakePB<\/jats:sc> tools, we provide formally verified end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_24","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"396-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Certified MaxSAT Preprocessing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4608-7549","authenticated-orcid":false,"given":"Hannes","family":"Ihalainen","sequence":"first","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-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"additional","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-2572-063X","authenticated-orcid":false,"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","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"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C., Schweitzer, P.: An introduction to certifying algorithms. IT - Information Technology Methoden und innovative Anwendungen der Informatik und Informationstechnik 53(6), 287\u2013293 (2011)","DOI":"10.1524\/itit.2011.0655"},{"key":"24_CR2","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gab\u00e0s, J., Levy, J.: Improving SAT-based weighted MaxSAT solvers. In: Milano, M. (eds.) Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP\u00a02012). LNCS, vol.\u00a07514, pp. 86\u2013101. Springer, Cham (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_9","DOI":"10.1007\/978-3-642-33558-7_9"},{"key":"24_CR3","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.) Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02020). LNCS, vol. 12178, pp. 277\u2013294. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_20","DOI":"10.1007\/978-3-030-51825-7_20"},{"key":"24_CR4","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.) Proceedings of the 29th International Conference on Automated Deduction (CADE-29). LNCS, vol. 14132, pp. 1\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1","DOI":"10.1007\/978-3-031-38499-8_1"},{"key":"24_CR5","doi-asserted-by":"publisher","unstructured":"Berg, J., J\u00e4rvisalo, M.: Unifying reasoning and core-guided search for maximum satisfiability. In: Calimeri, F., Leone, N., Manna, M. (eds.) Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA\u00a02019). LNCS, vol. 11468, pp. 287\u2013303. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-19570-0_19","DOI":"10.1007\/978-3-030-19570-0_19"},{"key":"24_CR6","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Subsumed label elimination for maximum satisfiability. In: Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI\u00a02016). FAIA, vol.\u00a0285, pp. 630\u2013638. IOS Press (2016)"},{"key":"24_CR7","unstructured":"Biere, A.: Tracecheck (2006). http:\/\/fmv.jku.at\/tracecheck\/"},{"key":"24_CR8","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.\u00a0336. IOS Press, February 2021","DOI":"10.3233\/FAIA336"},{"key":"24_CR9","doi-asserted-by":"crossref","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). Preliminary version in AAAI\u00a02022","DOI":"10.1613\/jair.1.14296"},{"key":"24_CR10","unstructured":"Bogaerts, B., McCreesh, C., Myreen, M.O., Nordstr\u00f6m, J., Oertel, A., Tan, Y.K.: Documentation of VeriPB and CakePB for the SAT competition 2023, March 2023. Available at https:\/\/satcompetition.github.io\/2023\/checkers.html"},{"issue":"8\u20139","key":"24_CR11","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":"24_CR12","doi-asserted-by":"crossref","unstructured":"Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern. Part B (Cybern.) 34(1), 52\u201359 (2004)","DOI":"10.1109\/TSMCB.2002.805807"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02010). LNCS, vol.\u00a06175, pp. 44\u201357. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"24_CR14","unstructured":"Buss, S.R., Nordstr\u00f6m, J.: Proof complexity and SAT solving. In: Biere et\u00a0al. [8], Chap.\u00a07, pp. 233\u2013350"},{"issue":"1","key":"24_CR15","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."},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt\u00a0Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (eds.) Proceedings of the 26th International Conference on Automated Deduction (CADE-26). LNCS, vol. 10395, pp. 220\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Marques-Silva, J.P., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u00a02017). LNCS, vol. 10205, pp. 118\u2013135. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7","DOI":"10.1007\/978-3-662-54577-5_7"},{"key":"24_CR18","doi-asserted-by":"publisher","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (eds.) Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP\u00a02011). LNCS, vol.\u00a06876, pp. 225\u2013239. Springer, Cham (2011). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_19","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"24_CR19","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":"24_CR20","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02005). LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Cham (2005). https:\/\/doi.org\/10.1007\/11499107_5","DOI":"10.1007\/11499107_5"},{"issue":"1\u20134","key":"24_CR21","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. Satisfiability Boolean Model. Comput. 2(1\u20134), 1\u201326 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"24_CR22","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\u00a02020), pp. 1486\u20131494, February 2020","DOI":"10.1609\/aaai.v34i02.5507"},{"key":"24_CR23","doi-asserted-by":"publisher","unstructured":"Filmus, Y., Mahajan, M., Sood, G., Vinyals, M.: MaxSAT resolution and subcube sums. In: Pulina, L., Seidl, M. (eds.) Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02020). LNCS, vol. 12178, pp. 295\u2013311. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_21","DOI":"10.1007\/978-3-030-51825-7_21"},{"key":"24_CR24","unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania (1995)"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Gimpel, J.F.: A reduction technique for prime implicant tables. In: Proceedings of the 5th Annual Symposium on Switching Circuit Theory and Logical Design, (SWCT\u00a01964), pp. 183\u2013191. IEEE Computer Society (1964)","DOI":"10.1109\/SWCT.1964.4"},{"key":"24_CR26","unstructured":"Gocht, S.: Certifying correctness for combinatorial algorithms by using pseudo-Boolean reasoning, Ph.D. thesis, Lund University, June 2022. https:\/\/portal.research.lu.se\/en\/publications\/certifying-correctness-for-combinatorial-algorithms-by-using-pseu"},{"key":"24_CR27","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\u00a02022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0236, pp. 16:1\u201316:25, August 2022"},{"key":"24_CR28","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. (eds.) Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP\u00a02020). LNCS, vol. 12333, pp. 338\u2013357. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_20","DOI":"10.1007\/978-3-030-58475-7_20"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Gocht, S., McCreesh, C., Myreen, M.O., Nordstr\u00f6m, J., Oertel, A., Tan, Y.K.: End-to-end verification for subgraph solving. In: Proceedings of the 368h AAAI Conference on Artificial Intelligence (AAAI\u00a02024), pp. 8038\u20138047, February 2024","DOI":"10.1609\/aaai.v38i8.28642"},{"key":"24_CR30","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\u00a02020), pp. 1134\u20131140, July 2020","DOI":"10.24963\/ijcai.2020\/158"},{"key":"24_CR31","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\u00a02022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0235, pp. 25:1\u201325:18, August 2022"},{"key":"24_CR32","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\u00a02021), pp. 3768\u20133777, February 2021","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"24_CR33","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\u00a02003), pp. 886\u2013891, March 2003","DOI":"10.1109\/DATE.2003.1253718"},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Yang, H. (eds.) Proceedings of the 26th European Symposium on Programming (ESOP\u00a02017). LNCS, vol. 10201, pp. 584\u2013610. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_22","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt\u00a0Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u00a02013), pp. 181\u2013188, October 2013","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"24_CR36","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Hunt\u00a0Jr., W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (eds.) Proceedings of the 24th International Conference on Automated Deduction (CADE-24). LNCS, vol.\u00a07898, pp. 345\u2013359. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_24","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Hoen, A., Oertel, A., Gleixner, A., Nordstr\u00f6m, J.: Certifying MIP-based presolve reductions for $$0$$\u2013$$1$$ integer linear programs. In: Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR\u00a02024), May 2024, to appear","DOI":"10.1007\/978-3-031-60597-0_20"},{"issue":"1","key":"24_CR38","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.: RC2: an efficient MaxSAT solver. J. Satisfiability Boolean Model. Comput. 11(1), 53\u201364 (2019)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"24_CR39","doi-asserted-by":"publisher","unstructured":"Ihalainen, H., Berg, J., J\u00e4rvisalo, M.: Clause redundancy and preprocessing in maximum satisfiability. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR\u00a02022). LNCS, vol. 13385, pp. 75\u201394. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_6","DOI":"10.1007\/978-3-031-10769-6_6"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"Ihalainen, H., et al.: Certified MaxSAT preprocessing (2024). https:\/\/arxiv.org\/abs\/2404.17316. Full-length version","DOI":"10.1007\/978-3-031-63498-7_24"},{"key":"24_CR41","doi-asserted-by":"publisher","unstructured":"Ihalainen, H., et al.: Experimental Repository for \u201cCertified MaxSAT Preprocessing\u201d, February 2024. https:\/\/doi.org\/10.5281\/zenodo.10630852","DOI":"10.5281\/zenodo.10630852"},{"key":"24_CR42","unstructured":"Jabs, C., Berg, J., Ihalainen, H., J\u00e4rvisalo, M.: Preprocessing in SAT-based multi-objective combinatorial optimization. In: Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming (CP\u00a02023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0280, pp. 18:1\u201318:20 (2023)"},{"key":"24_CR43","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u00a02010). LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"24_CR44","doi-asserted-by":"publisher","unstructured":"Korhonen, T., Berg, J., Saikko, P., J\u00e4rvisalo, M.: MaxPre: an extended MaxSAT preprocessor. In: Gaspers, S., Walsh, T. (eds.) Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02017). LNCS, vol. 10491, pp. 449\u2013456. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_28","DOI":"10.1007\/978-3-319-66263-3_28"},{"issue":"1","key":"24_CR45","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":"24_CR46","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S1571-0653(04)00314-2","volume":"9","author":"D Le Berre","year":"2001","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. Electron. Notes Discrete Math. 9, 59\u201380 (2001)","journal-title":"Electron. Notes Discrete Math."},{"key":"24_CR47","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisfiability Boolean Model. Comput. 7, 59\u201364 (2010)","DOI":"10.3233\/SAT190075"},{"key":"24_CR48","unstructured":"Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on Innovative Applications of Artificial Intelligence, pp. 291\u2013296. AAAI Press\/The MIT Press (2000)"},{"key":"24_CR49","doi-asserted-by":"publisher","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) 8th International Haifa Verification Conference (HVC\u00a02012), Revised Selected Papers. LNCS, vol.\u00a07857, pp. 102\u2013117. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_14","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"24_CR50","unstructured":"MaxPre 2: MaxSAT preprocessor. https:\/\/bitbucket.org\/coreo-group\/maxpre2"},{"key":"24_CR51","unstructured":"MaxSAT evaluations: Evaluating the state of the art in maximum satisfiability solver technology. https:\/\/maxsat-evaluations.github.io\/"},{"key":"24_CR52","unstructured":"MaxSAT evaluation 2023, July 2023. https:\/\/maxsat-evaluations.github.io\/2023"},{"issue":"2","key":"24_CR53","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":"24_CR54","unstructured":"McIlree, M., McCreesh, C.: Proof logging for smart extensional constraints. In: Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming (CP\u00a02023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0280, pp. 26:1\u201326:17, August 2023"},{"key":"24_CR55","doi-asserted-by":"crossref","unstructured":"McIlree, M., McCreesh, C., Nordstr\u00f6m, J.: Proof logging for the circuit constraint. In: Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR\u00a02024), May 2024, to appear","DOI":"10.1007\/978-3-031-60599-4_3"},{"key":"24_CR56","doi-asserted-by":"publisher","unstructured":"Morgado, A., Heras, F., Marques-Silva, J.: Improvements to core-guided binary search for MaxSAT. In: Cimatti, A., Sebastiani, R. (eds.) Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02012). LNCS, vol.\u00a07317, pp. 284\u2013297. Springer, Cham (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_22","DOI":"10.1007\/978-3-642-31612-8_22"},{"key":"24_CR57","doi-asserted-by":"publisher","unstructured":"Morgado, A., Ignatiev, A., Bonet, M.L., Marques-Silva, J.P., Buss, S.R.: DRMaxSAT with MaxHS: first contact. In: Janota, M., Lynce, I. (eds.) Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02019). LNCS, vol. 11628, pp. 239\u2013249. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_17","DOI":"10.1007\/978-3-030-24258-9_17"},{"key":"24_CR58","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\u00a02011), pp. 924\u2013926 (2011)","DOI":"10.1109\/ICTAI.2011.157"},{"issue":"2\u20133","key":"24_CR59","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1017\/S0956796813000282","volume":"24","author":"MO Myreen","year":"2014","unstructured":"Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2\u20133), 284\u2013315 (2014)","journal-title":"J. Funct. Program."},{"key":"24_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"R Ostrowski","year":"2002","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185\u2013199. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46135-3_13"},{"key":"24_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/978-3-030-67067-2_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Paxian","year":"2021","unstructured":"Paxian, T., Raiola, P., Becker, B.: On preprocessing for weighted MaxSAT. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 556\u2013577. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_25"},{"key":"24_CR62","doi-asserted-by":"publisher","unstructured":"Paxian, T., Reimer, S., Becker, B.: Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In: Beyersdorff, O., Wintersteiger, C. (eds.) Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02018). LNCS, vol. 10929, pp. 37\u201353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_3","DOI":"10.1007\/978-3-319-94144-8_3"},{"key":"24_CR63","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\u00a02020), pp. 137\u2013144, November 2020","DOI":"10.1109\/ICTAI50040.2020.00032"},{"key":"24_CR64","doi-asserted-by":"publisher","unstructured":"Py, M., Cherif, M.S., Habet, D.: A proof builder for Max-SAT. In: Li, CM., Many\u00e1, F. (eds.) Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02021). LNCS, vol. 12831, pp. 488\u2013498. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_33","DOI":"10.1007\/978-3-030-80223-3_33"},{"key":"24_CR65","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":"24_CR66","unstructured":"The International SAT Competitions web page. http:\/\/www.satcompetition.org"},{"key":"24_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"24_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276\u2013291. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11527695_22"},{"key":"24_CR69","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: Verified propagation redundancy and compositional UNSAT checking in CakeML. Int. J. Softw. Tools Technol. Transf. 25, 167\u2013184 (2023). Preliminary version in TACAS\u00a02021","DOI":"10.1007\/s10009-022-00690-y"},{"key":"24_CR70","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A.C.J., Owens, S., Norrish, M.: The verified CakeML compiler backend. J. Funct. Program. 29, e2:1\u2013e2:57 (2019)","DOI":"10.1017\/S0956796818000229"},{"issue":"1","key":"24_CR71","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A Van Gelder","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239\u2013253 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"24_CR72","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.) Proceedings of the 16th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR\u00a02022). LNCS, vol. 13416, pp. 429\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15707-3_33","DOI":"10.1007\/978-3-031-15707-3_33"},{"key":"24_CR73","unstructured":"VeriPB: Verifier for pseudo-Boolean proofs. https:\/\/gitlab.com\/MIAOresearch\/software\/VeriPB"},{"key":"24_CR74","doi-asserted-by":"publisher","unstructured":"Wetzler, N., Heule, M.J.H., Hunt\u00a0Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02014). LNCS, vol.\u00a08561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"24_CR75","unstructured":"Zabih, R., McAllester, D.A.: A rearrangement search strategy for determining propositional satisfiability. In: Proceedings of the 7th National Conference on Artificial Intelligence (AAAI\u00a01988), pp. 155\u2013160. AAAI Press\/The MIT Press (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:29Z","timestamp":1747592249000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}