Abstract
Interpolation-based model checking (ITP) McMillan (in CAV, 2003) is an efficient and complete model checking procedure. However, for large problems, interpolants generated by ITP might become extremely large, rendering the procedure slow or even intractable. In this work we present a novel technique for interpolant generation in the context of model checking. The main novelty of our work is that we generate small interpolants in conjunctive normal form (CNF) using a twofold procedure: first we propose an algorithm that exploits resolution refutation properties to compute an interpolant approximation. Then we introduce an algorithm that takes advantage of inductive reasoning to turn the interpolant approximation into an interpolant. Unlike ITP, our approach maintains only the relevant subset of the resolution refutation. In addition, the second part of the procedure exploits the properties of the model checking problem at hand, in contrast to the general-purpose algorithm used in ITP. We developed a new interpolation-based model checking algorithm, called CNF-ITP. Our algorithm takes advantage of the smaller interpolants and exploits the fact that the interpolants are given in CNF. We integrated our method into a SAT-based model checker and experimented with a representative subset of the HWMCC’12 benchmark set. Our experiments show that, overall, the interpolants generated by our method are 117 times smaller than those generated by ITP. Our CNF-ITP algorithm outperforms ITP, and at times solves problems that ITP cannot solve. We also compared CNF-ITP to the successful IC3 Bradely (in VMCAI, volume 6538 of lecture notes in computer science, 2011) algorithm. We found that CNF-ITP outperforms IC3 Bradely (in VMCAI, volume 6538 of lecture notes in computer science, 2011) in a large number of cases.
Similar content being viewed by others
Notes
Variable elimination [7] is an operation that eliminates all occurrences of a variable \(v\) from a CNF formula by replacing clauses containing \(v\) with the result of pairwise resolutions between all clauses containing the literal \(v\) and those containing the literal \(\lnot v\).
Some works choose different ways of increasing \(k\). For example, \(k\) can be increased by the number of iterations executed in the inner loop: \(k=k+n\). In our experiments \(k=k+1\) yielded better results.
References
Bar-Ilan O, Fuhrmann O, Hoory S, Shacham O, Strichman O (2008) Linear-time reductions of resolution proofs. In: Chockler H, Hu Alan J (eds) Haifa verification conference, volume 5394 of lecture notes in computer science, Springer, Heidelberg, pp 114–128
Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117–148
Bradley AR (2011) Sat-based model checking without unrolling. In: Jhala R, Schmidt DA (eds.) VMCAI, volume 6538 of lecture notes in computer science, Springer, Heidelberg, pp 70–87
Cabodi G, Murciano M, Nocco S, Quer S (2006) Stepping forward with interpolants in unbounded model checking. In: Hassoun S (eds.) ICCAD, ACM, pp 772–778
Chockler H, Ivrii A, Matsliah A (2012) Computing interpolants without proofs. In: Biere A, Nahir A, Vos TEJ (eds.) Haifa verification conference, volume 7857 of lecture notes in computer science, Springer, pp 72–85
Craig W (1957) Linear reasoning. A new form of the herbrand-gentzen theorem. J Symb Log 22(3):250–268
Davis Martin, Putnam Hilary (1960) A computing procedure for quantification theory. J. ACM 7(3):201–215
D’Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In VMCAI, Springer, Heidelberg, pp 129–145
Eén N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: Bacchus F, Walsh T (eds.) SAT, volume 3569 of lecture notes in computer science, Springer, Heidelberg, pp 61–75
Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: Bjesse P, Slobodová A (eds) FMCAD. FMCAD Inc., Austin, pp 125–134
Goldberg E, Novikov Y (2003) Verification of proofs of unsatisfiability for CNF formulas. In DATE, IEEE Computer Society, p 886–891
Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In POPL, ACM, pp 232–244
Jhala R, McMillan KL (2005) Interpolant-based transition relation approximation. In CAV, Springer, Heidelberg, pp 39–51
Marques-Silva João (2007) Interpolant learning and reuse in SAT-based model checking. Electr Notes Theor Comput Sci 174(3):31–43
McMillan KL (2003) Interpolation and SAT-based Model Checking. In CAV, Springer, Heidelberg, pp 1–13
McMillan KL (2006) Lazy abstraction with interpolants. In CAV, Springer, Heidelberg, pp 123–136
McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In TACAS, Springer, Heidelberg, pp 2–17
Pudlák P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981–998
Rollini S, Bruttomesso R, Sharygina N (2010) An efficient and flexible approach to resolution proof reduction. In: Barner S, Harris IG, Kroening D, Raz O (eds.) Haifa verification conference, volume 6504 of lecture notes in computer science, Springer, Heidelberg, pp 182–196
Ryvchin V, Strichman O (2011) Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah KA, Simon L (eds.) SAT, volume 6695 of lecture notes in computer science, Springer, Heidelberg, pp 174–187
Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In FMCAD, IEEE, pp 1–8
Vizel Y, Grumberg O, Shoham S (2013) Intertwined forward-backward reachability analysis using interpolants. In: Piterman N, Smolka SA (eds.) TACAS, volume 7795 of lecture notes in computer science, Springer, Heidelberg, pp 308–323
Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability. In: Biere A, Bloem R (eds.) CAV, volume 8559 of lecture notes in computer science, Springer, Heidelberg, pp 260–276
Vizel Y, Ryvchin V, Nadel A (2013) Efficient generation of small interpolants in cnf. In: Sharygina N, Veith H (eds.) CAV, volume 8044 of lecture notes in computer science, Springer, Heidelberg, pp 330–346
Zhang L, Malik S (2003) Extracting small unsatisfiable cores from unsatisfiable Boolean formula. In SAT
Author information
Authors and Affiliations
Corresponding author
Additional information
A preliminary version of this work appeared in [24]. The authors would like to thank Håkan Hjort and Paul Inbar for their valuable comments.
Rights and permissions
About this article
Cite this article
Vizel, Y., Nadel, A. & Ryvchin, V. Efficient generation of small interpolants in CNF. Form Methods Syst Des 47, 51–74 (2015). https://doi.org/10.1007/s10703-015-0224-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-015-0224-5