Open Collections

Description

Interference-based certification methods for SAT solving, including the de facto standard DRAT, show intriguing and counter-intuitive non-monotonic properties. In particular, their proof rules depend not only on the claims that were previously derived, but also on not having derived some claims, complicating proof composition and trimming. Recent results, presented at SYNASC this year, show these properties are not inherent to the underlying reasoning, but rather artifacts of the way interference-based proofs are understood and presented. Through novel methods that interpret these proofs as programs, monotonicity and compositionality can be recovered. While this view paves the way for more usable proof formats for SAT and other combinatorial problems, it also suggests a framework to develop hardware and software certification methods, where proofs of programs may carry programs themselves. In this talk, I will explore what kinds of programs and properties this framework can handle.