Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Berg, Jeremias ; Bogaerts, Bart ; Nordström, Jakob LU ; Oertel, Andy LU orcid ; Paxian, Tobias and Vandesande, Dieter (2024) 30th International Conference on Principles and Practice of Constraint Programming, CP 2024 In Leibniz International Proceedings in Informatics (LIPIcs) 307.
Abstract
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of... (More)
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving. (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
30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
series title
Leibniz International Proceedings in Informatics (LIPIcs)
editor
Shaw, Paul
volume
307
article number
4
pages
28 pages
publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
conference name
30th International Conference on Principles and Practice of Constraint Programming, CP 2024
conference location
Girona, Spain
conference dates
2024-09-02 - 2024-09-06
external identifiers
  • scopus:85203681562
ISSN
1868-8969
ISBN
978-3-95977-336-2
DOI
10.4230/LIPIcs.CP.2024.4
language
English
LU publication?
yes
id
1db54cf4-755f-48c1-bc46-4086acc5891e
date added to LUP
2024-09-09 10:45:25
date last changed
2025-04-04 14:15:45
@inproceedings{1db54cf4-755f-48c1-bc46-4086acc5891e,
  abstract     = {{Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.}},
  author       = {{Berg, Jeremias and Bogaerts, Bart and Nordström, Jakob and Oertel, Andy and Paxian, Tobias and Vandesande, Dieter}},
  booktitle    = {{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}},
  editor       = {{Shaw, Paul}},
  isbn         = {{978-3-95977-336-2}},
  issn         = {{1868-8969}},
  language     = {{eng}},
  month        = {{08}},
  publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
  series       = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
  title        = {{Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability}},
  url          = {{http://dx.doi.org/10.4230/LIPIcs.CP.2024.4}},
  doi          = {{10.4230/LIPIcs.CP.2024.4}},
  volume       = {{307}},
  year         = {{2024}},
}