Sammanfattning
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
stateoftheart techniques.
This work develops a new proof system building on the cutting planes
proof system and operating on pseudoBoolean constraints (01 linear
inequalities). We explain how such machineverifiable proofs can be
created for various problems, including parity reasoning, symmetry and
dominance breaking, constraint programming, subgraph isomorphism and
maximum common subgraph problems, and pseudoBoolean 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
pseudoBoolean optimisation, MaxSAT and beyond.
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
stateoftheart techniques.
This work develops a new proof system building on the cutting planes
proof system and operating on pseudoBoolean constraints (01 linear
inequalities). We explain how such machineverifiable proofs can be
created for various problems, including parity reasoning, symmetry and
dominance breaking, constraint programming, subgraph isomorphism and
maximum common subgraph problems, and pseudoBoolean 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
pseudoBoolean optimisation, MaxSAT and beyond.
Originalspråk  engelska 

Kvalifikation  Doktor 
Tilldelande institution 

Handledare 

Tilldelningsdatum  2022 juni 10 
Förlag  
ISBN (tryckt)  9789180392679 
ISBN (elektroniskt)  9789180392686 
Status  Published  2022 maj 13 
Bibliografisk information
Defence detailsDate: 20220610
Time: 14:15
Place: Lecture hall E:A, building E, Ole Römers väg 3, Faculty of Engineering LTH, Lund University, Lund.
External reviewer(s)
Name: Heule, Marijn
Title: Prof.
Affiliation: Carnegie Mellon University, USA.

Ämnesklassifikation (UKÄ)
 Datavetenskap (datalogi)