An Efficient and Flexible Approach to Resolution Proof Reduction
A resoution proof is a certificate of the unsatisfiability of a Boolean formula. Resolution proofs, as generated by modern SAT solvers, find application in many verification techniques. For efficiency smaller proofs are preferable over larger ones. 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 benchmarks, which shows considerable reduction in the proofs size.
KeywordsModel Check Flexible Approach Reduction Rule Resolution Step Empty Clause
Unable to display preview. Download preview PDF.
- 1.Amjad, H.: Compressing Propositional Refutations. In: AVoCS, pp. 7–18 (2006)Google Scholar
- 2.Amjad, H.: Data Compression for Proof Replay. J. Autom. Reasoning 41(3/4) (2008)Google Scholar
- 5.Bruttomesso, R., Rollini, S.,Sharygina, N., Tsitovich, A.: Flexible Interpolation with Local Proof Transformations. In: ICCAD (2010), http://www.inf.usi.ch/postdoc/bruttomesso/ICCAD2010 (to appear)
- 7.D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Restructuring Resolution Refutations for Interpolation. Technical report, ETH (2008)Google Scholar
- 9.Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL (2004)Google Scholar
- 15.Sinz, C., Kaiser, A., Kuchlin, W.: Formal Methods for the Validation of Automotive Product Configuration Data. AI EDAM 17(1), 75–97 (2003)Google Scholar
- 16.Tseitin, G.: On the Complexity of Proofs in Propositional Logic. Automation of Reasoning: Classical Papers in Computational Logic 2, 1967–1970 (1983)Google Scholar
- 17.Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: DATE (2003)Google Scholar