An Efficient and Flexible Approach to Resolution Proof Reduction

Abstract:

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 per-
formed, 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.
 

Notes:

• BibTex

@inproceedings { RBS10,
	title = {An Efficient and Flexible Approach to Resolution Proof Reduction},
	booktitle = {Haifa Verification Conference (HVC)},
	year = {2010},
	note = {to appear},
	publisher = {Springer},
	organization = {Springer},
	address = {Haifa, Israel},
	author = {Simone Fulvio Rollini and  Roberto Bruttomesso and  Natasha Sharygina}
}