Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2012: Theory and Applications of Satisfiability Testing – SAT 2012 pp 312–326Cite as

Interpolant Strength Revisited

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7317))

Abstract

Craig’s interpolation theorem has numerous applications in model checking, automated reasoning, and synthesis. There is a variety of interpolation systems which derive interpolants from refutation proofs; these systems are ad-hoc and rigid in the sense that they provide exactly one interpolant for a given proof. In previous work, we introduced a parametrised interpolation system which subsumes existing interpolation methods for propositional resolution proofs and enables the systematic variation of the logical strength and the elimination of non-essential variables in interpolants. In this paper, we generalise this system to propositional hyper-resolution proofs and discuss its application to proofs generated by contemporary SAT solvers. Finally, we show that, when applied to local (or split) proofs, our extension generalises two existing interpolation systems for first-order logic and relates them in logical strength.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.B.: Resolution with merging. J. ACM 15, 367–381 (1968)

    Article  MATH  Google Scholar 

  2. Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: IAAI, pp. 613–619. AAAI Press / MIT Press (2002)

    Google Scholar 

  3. Bonacina, M.P., Johansson, M.: On Interpolation in Decision Procedures. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 1–16. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. In: TOCL (2010)

    Google Scholar 

  5. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic 22, 250–268 (1957)

    Article  MathSciNet  MATH  Google Scholar 

  6. D’Silva, V.: Propositional Interpolation and Abstract Interpretation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 185–204. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground Interpolation for the Theory of Equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 413–427. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Gershman, R., Strichman, O.: Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 423–429. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)

    Google Scholar 

  12. Huang, G.: Constructing Craig Interpolation Formulas. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol. 959, pp. 181–190. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  13. Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating functions from large Boolean relations. In: ICCAD, pp. 779–784. ACM (2009)

    Google Scholar 

  15. Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 199–213. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symbolic Logic 62, 457–486 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Maehara, S.: On the interpolation theorem of Craig. Sûgaku 12, 235–237 (1961)

    MathSciNet  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. McMillan, K.L.: An interpolating theorem prover. TCS 345(1), 101–121 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  20. McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62, 981–998 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  22. Robinson, J.: Automatic deduction with hyper-resolution. J. Comp. Math. 1 (1965)

    Google Scholar 

  23. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. STTT 12, 319–335 (2010)

    Article  Google Scholar 

  25. Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Oxford (2010)

    Google Scholar 

  26. Yorsh, G., Musuvathi, M.: A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Princeton University, USA

    Georg Weissenbacher

  2. Vienna University of Technology, Austria

    Georg Weissenbacher

Authors
  1. Georg Weissenbacher
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Center for Information Technology, Fondazione Bruno Kessler, via Sommarive 18, Povo, 38123, Trento, Italy

    Alessandro Cimatti

  2. Department of Information Engineering and Computer Science, University of Trento, via Sommarive 14, Povo, 38123, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Weissenbacher, G. (2012). Interpolant Strength Revisited. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31612-8_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31611-1

  • Online ISBN: 978-3-642-31612-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation