Advertisement

An Efficient and Flexible Approach to Resolution Proof Reduction

  • Simone Fulvio Rollini
  • Roberto Bruttomesso
  • Natasha Sharygina
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)

Abstract

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.

Keywords

Model Check Flexible Approach Reduction Rule Resolution Step Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Amjad, H.: Compressing Propositional Refutations. In: AVoCS, pp. 7–18 (2006)Google Scholar
  2. 2.
    Amjad, H.: Data Compression for Proof Replay. J. Autom. Reasoning 41(3/4) (2008)Google Scholar
  3. 3.
    Amla, N., McMillan, K.: Automatic Abstraction Without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-Time Reductions of Resolution Proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 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)
  6. 6.
    Cotton, S.: Two Techniques for Minimizing Resolution Proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306–312. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Restructuring Resolution Refutations for Interpolation. Technical report, ETH (2008)Google Scholar
  8. 8.
    D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant Strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL (2004)Google Scholar
  10. 10.
    Jhala, R., McMillan, K.L.: Interpolant-Based Transition Relation Approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    McMillan, K.L.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Sinz, C.: Compressing Propositional Proofs by Common Subproof Extraction. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 547–555. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 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. 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. 17.
    Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: DATE (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Simone Fulvio Rollini
    • 1
  • Roberto Bruttomesso
    • 1
  • Natasha Sharygina
    • 1
  1. 1.Formal Verification GroupUniversity of LuganoLuganoSwitzerland

Personalised recommendations