Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Certifying Correctness for Combinatorial Algorithms : by Using Pseudo-Boolean Reasoning

Gocht, Stephan LU (2022)
Abstract
Over the last decades, dramatic improvements in combinatorial
optimisation algorithms have significantly impacted artificial
intelligence, operations research, and other areas. These advances,
however, are achieved through highly sophisticated algorithms that are
difficult to verify and prone to implementation errors that can cause
incorrect results. A promising approach to detect wrong results is to
use certifying algorithms that produce not only the desired output but
also a certificate or proof of correctness of the output. An external
tool can then verify the proof to determine that the given answer is
valid. In the Boolean satisfiability (SAT) community, this concept is
well established in the... (More)
Over the last decades, dramatic improvements in combinatorial
optimisation algorithms have significantly impacted artificial
intelligence, operations research, and other areas. These advances,
however, are achieved through highly sophisticated algorithms that are
difficult to verify and prone to implementation errors that can cause
incorrect results. A promising approach to detect wrong results is to
use certifying algorithms that produce not only the desired output but
also a certificate or proof of correctness of the output. An external
tool can then verify the proof to determine that the given answer is
valid. In the Boolean satisfiability (SAT) community, this concept is
well established in the form of proof logging, which has become the
standard solution for generating trustworthy outputs. The problem is
that there are still some SAT solving techniques for which proof
logging is challenging and not yet used in practice. Additionally,
there are many formalisms more expressive than SAT, such as constraint
programming, various graph problems and maximum satisfiability
(MaxSAT), for which efficient proof logging is out of reach for
state-of-the-art techniques.

This work develops a new proof system building on the cutting planes
proof system and operating on pseudo-Boolean constraints (0-1 linear
inequalities). We explain how such machine-verifiable proofs can be
created for various problems, including parity reasoning, symmetry and
dominance breaking, constraint programming, subgraph isomorphism and
maximum common subgraph problems, and pseudo-Boolean problems. We
implement and evaluate the resulting algorithms and a verifier for the
proof format, demonstrating that the approach is practical for a wide
range of problems. We are optimistic that the proposed proof system is
suitable for designing certifying variants of algorithms in
pseudo-Boolean optimisation, MaxSAT and beyond. (Less)
Please use this url to cite or link to this publication:
author
supervisor
opponent
  • Prof. Heule, Marijn, Carnegie Mellon University, USA.
organization
publishing date
type
Thesis
publication status
published
subject
keywords
certifying algorithms, 0-1 linear inequalities, combinatorial algorithms, proof logging
pages
228 pages
publisher
Department of Computer Science, Lund University
defense location
Lecture hall E:A, building E, Ole Römers väg 3, Faculty of Engineering LTH, Lund University, Lund.
defense date
2022-06-10 14:15:00
ISBN
978-91-8039-267-9
978-91-8039-268-6
language
English
LU publication?
yes
id
3550cb96-83d5-4fc7-9e62-190083a3c10a
date added to LUP
2022-05-10 12:05:45
date last changed
2022-05-12 11:40:11
@phdthesis{3550cb96-83d5-4fc7-9e62-190083a3c10a,
  abstract     = {{Over the last decades, dramatic improvements in combinatorial<br/>optimisation algorithms have significantly impacted artificial<br/>intelligence, operations research, and other areas. These advances,<br/>however, are achieved through highly sophisticated algorithms that are<br/>difficult to verify and prone to implementation errors that can cause<br/>incorrect results. A promising approach to detect wrong results is to<br/>use certifying algorithms that produce not only the desired output but<br/>also a certificate or proof of correctness of the output. An external<br/>tool can then verify the proof to determine that the given answer is<br/>valid. In the Boolean satisfiability (SAT) community, this concept is<br/>well established in the form of proof logging, which has become the<br/>standard solution for generating trustworthy outputs. The problem is<br/>that there are still some SAT solving techniques for which proof<br/>logging is challenging and not yet used in practice. Additionally,<br/>there are many formalisms more expressive than SAT, such as constraint<br/>programming, various graph problems and maximum satisfiability<br/>(MaxSAT), for which efficient proof logging is out of reach for<br/>state-of-the-art techniques.<br/><br/>This work develops a new proof system building on the cutting planes<br/>proof system and operating on pseudo-Boolean constraints (0-1 linear<br/>inequalities). We explain how such machine-verifiable proofs can be<br/>created for various problems, including parity reasoning, symmetry and<br/>dominance breaking, constraint programming, subgraph isomorphism and<br/>maximum common subgraph problems, and pseudo-Boolean problems. We<br/>implement and evaluate the resulting algorithms and a verifier for the<br/>proof format, demonstrating that the approach is practical for a wide<br/>range of problems. We are optimistic that the proposed proof system is<br/>suitable for designing certifying variants of algorithms in<br/>pseudo-Boolean optimisation, MaxSAT and beyond.}},
  author       = {{Gocht, Stephan}},
  isbn         = {{978-91-8039-267-9}},
  keywords     = {{certifying algorithms; 0-1 linear inequalities; combinatorial algorithms; proof logging}},
  language     = {{eng}},
  month        = {{05}},
  publisher    = {{Department of Computer Science, Lund University}},
  school       = {{Lund University}},
  title        = {{Certifying Correctness for Combinatorial Algorithms : by Using Pseudo-Boolean Reasoning}},
  url          = {{https://lup.lub.lu.se/search/files/117886509/thesis_final_pdf.pdf}},
  year         = {{2022}},
}