Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Certified MaxSAT Preprocessing

Ihalainen, Hannes ; Oertel, Andy LU orcid ; Tan, Yong Kiam ; Berg, Jeremias ; Järvisalo, Matti ; Myreen, Magnus O. and Nordström, Jakob LU (2024) 12th International Joint Conference, IJCAR 2024 In Lecture Notes in Computer Science 14739. p.396-418
Abstract
Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-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... (More)
Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-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.

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 VeriPB and CakePB 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. (Less)
Please use this url to cite or link to this publication:
author
; ; ; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Automated Reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I
series title
Lecture Notes in Computer Science
editor
Benzmüller, Christoph ; Heule, Marijn J.H. and Schmidt, Renate A.
volume
14739
edition
1
pages
396 - 418
publisher
Springer
conference name
12th International Joint Conference, IJCAR 2024
conference location
Nancy, France
conference dates
2024-07-03 - 2024-09-06
external identifiers
  • scopus:85200234682
ISSN
1611-3349
0302-9743
ISBN
978-3-031-63498-7
978-3-031-63497-0
DOI
10.1007/978-3-031-63498-7_24
language
English
LU publication?
yes
id
a4dcd6dd-6acb-44ae-bbf2-697f3de70895
date added to LUP
2024-09-09 10:36:07
date last changed
2024-10-08 08:54:37
@inproceedings{a4dcd6dd-6acb-44ae-bbf2-697f3de70895,
  abstract     = {{Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-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.<br/><br/>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 VeriPB and CakePB 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.}},
  author       = {{Ihalainen, Hannes and Oertel, Andy and Tan, Yong Kiam and Berg, Jeremias and Järvisalo, Matti and Myreen, Magnus O. and Nordström, Jakob}},
  booktitle    = {{Automated Reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I}},
  editor       = {{Benzmüller, Christoph and Heule, Marijn J.H. and Schmidt, Renate A.}},
  isbn         = {{978-3-031-63498-7}},
  issn         = {{1611-3349}},
  language     = {{eng}},
  month        = {{07}},
  pages        = {{396--418}},
  publisher    = {{Springer}},
  series       = {{Lecture Notes in Computer Science}},
  title        = {{Certified MaxSAT Preprocessing}},
  url          = {{http://dx.doi.org/10.1007/978-3-031-63498-7_24}},
  doi          = {{10.1007/978-3-031-63498-7_24}},
  volume       = {{14739}},
  year         = {{2024}},
}