×

Incremental preprocessing methods for use in BMC. (English) Zbl 1247.68167

Summary: Traditional incremental SAT solvers have achieved great success in the domain of bounded model checking (BMC). Recently, modern solvers have introduced advanced preprocessing procedures that have allowed them to obtain high levels of performance. Unfortunately, many preprocessing techniques such as variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be integrated into other SAT based BMC tools to achieve similar speedups.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

NiVER; MiniSat
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader F, Snyder W (2001) Unification theory. In: Handbook of automated reasoning. Amsterdam, Elsevier · Zbl 1011.68126
[2] Biere A (2004) Resolve and expand. In: International conference on theory and applications of satisfiability testing · Zbl 1122.68585
[3] Biere A (2008) Hardware model checking competition. URL http://fmv.jku.at/hwmcc08/ · Zbl 1171.68546
[4] Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Design automation conference
[5] Brayton R, Case M, Hurst A, Mishchenko A (2008) ABC and ABmC entering HWMCC’08. In: Hardware model checking competition solver description
[6] Cabodi G, Quer S, Nocco S (2010) Politecnico di Torino reachability analysis and verification tool. URL http://fmgroup.polito.it/quer/research/tool/tool.htm
[7] Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. J Form Methods Syst Des · Zbl 0985.68038
[8] Craig W (1957) Linear reasoning: a new form of the Herbrand-Gentzen theorem. J Symb Log · Zbl 0081.24402
[9] Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM · Zbl 0212.34203
[10] D’Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In: International conference on verification, model checking, and abstract interpretation · Zbl 1273.68225
[11] Eén N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: International conference on theory and applications of satisfiability testing · Zbl 1128.68463
[12] Eén N, Sörensson N (2003) Temporal induction by incremental SAT solving. In: International workshop on bounded model checking · Zbl 1271.68215
[13] Eén N, Srensson N (2003) An extensible SAT-solver. In: International conference on theory and applications of satisfiability testing
[14] Herbstritt M, Becker B, Scholl C (2006) Advanced SAT-techniques for bounded model checking of blackbox designs. In: Microprocessor test and verification workshop
[15] Järvisalo M, Biere A, Heule M (2010) Blocked clause elimination. In: International conference on tools and algorithms for the construction and analysis of systems
[16] Kullmann O (1997) On a generalization of extended resolution. Discrete Appl Math · Zbl 0941.68126
[17] Lewis M, Schubert T, Becker B (2007) Multithreaded SAT solving. In: Asia and South Pacific design automation conference
[18] McMillan KL (2003) Interpolation and SAT-based model checking. In: International conference computer aided verification · Zbl 1278.68184
[19] Pigorsch F, Scholl C, Disch S (2006) Advanced unbounded model checking based on AIGs, BDD sweeping, and quantifier scheduling. In: Conference on formal methods in computer aided design
[20] Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT-solver. In: International conference on formal methods in computer-aided design
[21] Strichman O (2004) Accelerating bounded model checking of safety properties. J Form Methods Syst Des · Zbl 1073.68054
[22] Subbarayan S, Pradhan D (2004) NiVER: Non Increasing Variable Elimination Resolution for preprocessing SAT instances. In: International conference on theory and applications of satisfiability testing · Zbl 1122.68618
[23] The VIS Group (1996) VIS: A system for verification and synthesis. In: International conference on computer aided verification
[24] Tseitin G (1968) On the complexity of derivation in propositional calculus. In: Studies in constructive mathematics and mathematical logic
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.