An Efficient and Flexible Approach to Resolution Proof Reduction

TitleAn Efficient and Flexible Approach to Resolution Proof Reduction
Publication TypeConference Paper
Year of Publication2010
AuthorsRollini, S.F., Bruttomesso R., and Sharygina Natasha
Conference NameHaifa Verification Conference (HVC)
Conference LocationHaifa, Israel

A propositional proof of unsatisfiability is a certificate of the unsatisfiability of a Boolean formula. Resolution proofs, as generated by modern SAT solvers, find application in many verification techniques where the size of the proofs considerably affects efficiency. This paper presents a new approach to proof reduction, situated among the purely post-processing methods. The main idea is to reduce the proof size by eliminating redundancies of occurrences of pivots along the proof paths. This is achieved by matching and rewriting local contexts into simpler ones. In our approach, rewriting can be easily customized in the way local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. We provide an extensive experimental evaluation of our technique on a set of SMT benchmarks, which shows considerable reduction in the proofs size.

Full Text