Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Certifying combinatorial optimization using pseudo-Boolean reasoning

Oertel, Andy LU orcid (2025) In Licentiate thesis 6, 2025.
Abstract
Combinatorial optimization provides a powerful framework for solving complex optimization problems with general-purpose solvers by modelling the problem in an abstract language. Due to breakthroughs in algorithms to solve combinatorial optimization problems in last decades, combinatorial optimization has become a valid approach to solve many real world problems efficiently. Key application areas are planning, scheduling, computer-aided design, verification, and even theorem proving. However, the efficiency of the tools to solve these problems comes at the cost of increased complexity of the solvers. This makes it difficult to trust that the result computed by a combinatorial optimization solver is correct, which especially becomes a... (More)
Combinatorial optimization provides a powerful framework for solving complex optimization problems with general-purpose solvers by modelling the problem in an abstract language. Due to breakthroughs in algorithms to solve combinatorial optimization problems in last decades, combinatorial optimization has become a valid approach to solve many real world problems efficiently. Key application areas are planning, scheduling, computer-aided design, verification, and even theorem proving. However, the efficiency of the tools to solve these problems comes at the cost of increased complexity of the solvers. This makes it difficult to trust that the result computed by a combinatorial optimization solver is correct, which especially becomes a concern if the correctness of the result is mission-critical.

The main approach to address this issue is certifying algorithms, where an algorithm has to also generate a certificate that its result is correct, which can then be checked independently. This thesis demonstrates how pseudo-Boolean reasoning can be used to provide efficient certification of results returned by different kinds of combinatorial optimization solvers. We present a unified multipurpose certification system with a formally verified end-to-end verification toolchain, which guarantees that the combinatorial optimization problem was solved correctly. Developing a multipurpose certification system distinguishes this work from any prior work, which predominantly focused on very specialized approaches. We also present certification for many algorithms which, prior to our work, lacked any approach for certifying their result. (Less)
Please use this url to cite or link to this publication:
author
supervisor
organization
publishing date
type
Thesis
publication status
published
subject
in
Licentiate thesis
volume
6, 2025
pages
269 pages
publisher
Department of Computer Science, Lund University
ISSN
1652-4691
ISBN
978-91-8104-770-7
978-91-8104-769-1
project
Certified Linear Pseudo-Boolean Optimization
language
English
LU publication?
yes
id
10eec9f5-157f-4bab-8b73-c2a4281060f2
date added to LUP
2025-11-07 13:28:39
date last changed
2025-11-29 03:36:18
@misc{10eec9f5-157f-4bab-8b73-c2a4281060f2,
  abstract     = {{Combinatorial optimization provides a powerful framework for solving complex optimization problems with general-purpose solvers by modelling the problem in an abstract language. Due to breakthroughs in algorithms to solve combinatorial optimization problems in last decades, combinatorial optimization has become a valid approach to solve many real world problems efficiently. Key application areas are planning, scheduling, computer-aided design, verification, and even theorem proving. However, the efficiency of the tools to solve these problems comes at the cost of increased complexity of the solvers. This makes it difficult to trust that the result computed by a combinatorial optimization solver is correct, which especially becomes a concern if the correctness of the result is mission-critical.<br/><br/>The main approach to address this issue is certifying algorithms, where an algorithm has to also generate a certificate that its result is correct, which can then be checked independently. This thesis demonstrates how pseudo-Boolean reasoning can be used to provide efficient certification of results returned by different kinds of combinatorial optimization solvers. We present a unified multipurpose certification system with a formally verified end-to-end verification toolchain, which guarantees that the combinatorial optimization problem was solved correctly. Developing a multipurpose certification system distinguishes this work from any prior work, which predominantly focused on very specialized approaches. We also present certification for many algorithms which, prior to our work, lacked any approach for certifying their result.}},
  author       = {{Oertel, Andy}},
  isbn         = {{978-91-8104-770-7}},
  issn         = {{1652-4691}},
  language     = {{eng}},
  month        = {{11}},
  note         = {{Licentiate Thesis}},
  publisher    = {{Department of Computer Science, Lund University}},
  series       = {{Licentiate thesis}},
  title        = {{Certifying combinatorial optimization using pseudo-Boolean reasoning}},
  url          = {{https://lup.lub.lu.se/search/files/232407990/thesis.pdf}},
  volume       = {{6, 2025}},
  year         = {{2025}},
}