Resolution Proof Transformation for Compression and Interpolation

TL;DR

This paper presents methods for compressing and manipulating resolution proofs of unsatisfiability using local rewriting rules, improving efficiency in proof processing for SAT, SMT, and theorem proving applications.

Contribution

It introduces a proof transformation framework with local rewriting rules for effective proof compression and manipulation, enhancing proof handling in verification workflows.

Findings

Proof compression reduces proof size significantly.

Proof manipulation facilitates better interpolant computation.

Heuristics improve proof simplification across various test cases.

Abstract

Verification methods based on SAT, SMT, and Theorem Proving often rely on proofs of unsatisfiability as a powerful tool to extract information in order to reduce the overall effort. For example a proof may be traversed to identify a minimal reason that led to unsatisfiability, for computing abstractions, or for deriving Craig interpolants. In this paper we focus on two important aspects that concern efficient handling of proofs of unsatisfiability: compression and manipulation. First of all, since the proof size can be very large in general (exponential in the size of the input problem), it is indeed beneficial to adopt techniques to compress it for further processing. Secondly, proofs can be manipulated as a flexible preprocessing step in preparation for interpolant computation. Both these techniques are implemented in a framework that makes use of local rewriting rules to transform the proofs. We show that a careful use of the rules, combined with existing algorithms, can result in an effective simplification of the original proofs. We have evaluated several heuristics on a wide range of unsatisfiable problems deriving from SAT and SMT test cases.