×

SAT solver management strategies in IC3: an experimental approach. (English) Zbl 1360.68580

Summary: This paper addresses the problem of handling SAT solving in IC3. SAT queries posed by IC3 significantly differ in both character and number from those posed by other SAT-based model checking algorithms. In addition, IC3 has proven to be highly sensitive to the way its SAT solving requirements are handled at the implementation level. The scenario pictured above poses serious challenges for any implementation of the algorithm. Deciding how to manage the SAT solving work required by the algorithm is key to IC3 performance. The purpose of this paper is to determine the best way to handle SAT solving in IC3. First we provide an in-depth characterization of the SAT solving work required by IC3 in order to gain useful insights into how to best handle its queries. Then we propose an experimental comparison of different strategies for the allocation, loading and clean-up of SAT solvers in IC3. Among the compared strategies we include the ones typically used in state-of-the-art model checking tools as well as some novel ones. Alongside comparing multiple versus single SAT solver implementations of IC3, we propose the use of secondary SAT solvers dedicated to handling certain types of queries. Different heuristics for SAT solver clean-up are evaluated, including new ones that follow the locality of the verification process. We also address clause database minimality, comparing different CNF encoding techniques. Though not finding a clear winner among the different sets of strategies compared, we outline several potential improvements for portfolio-based verification tools with multiple engines and tunings.

MSC:

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

Software:

CirCUs; MiniSat; Chaff; nuXmv
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Cabodi G, Mishchenko A, Palena M (2013) Trading-off incrementality and dynamic restart of multiple solvers in IC3. DIFTS, Portland
[2] Bradley AR (2011) SAT-based model checking without unrolling. VMCAI, Austin · Zbl 1317.68109 · doi:10.1007/978-3-642-18275-4_7
[3] Biere A, Jussila T (2008) The model checking competition web page. http://fmv.jku.at/hwmcc. Accessed Feb 2017
[4] Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. FMCAD, Austin, pp. 125-134. ISBN:978-0-9835678-1-3
[5] Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic Model Checking using SAT procedures instead of BDDs. In: Proceedings of the 36th design automation conference on New Orleans, Louisiana. IEEE Computer Society, June 1999, pp 317-320. DOI:10.1145/309847.309942 · Zbl 0636.68119
[6] Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT solver. In: Hunt WA, Johnson SD (eds) Proceedings of the formal methods in computer-aided design series, LNCS, vol 1954. Springer, Austin, November 2000, pp 108-125. ISBN:3-540-41219-0
[7] Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Proceedings of the formal methods in computer-aided design, series, LNCS, vol 1954. Springer, Austin, pp 372-389. ISBN:3-540-41219-0
[8] McMillan KL (2003) Interpolation and SAT-based model checking. In: Proceedings of the computer aided verification, series. LNCS, vol 2725. Springer, Boulder, pp 1-13. doi:10.1007/978-3-540-45069-6_1 · Zbl 1278.68184
[9] Bradley AR (2012) Understanding IC3. In: Cimatti A, Sebastiani R (eds) SAT series Lecture Notes in Computer Science, vol 7317. Springer, pp. 1-14. doi:10.1007/978-3-642-31612-8_1 · Zbl 1273.68222
[10] Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Form Methods Syst Des 39(2):205-227. doi:10.1007/s10703-011-0123-3 · Zbl 1247.68160 · doi:10.1007/s10703-011-0123-3
[11] Mishchenko A (2007) ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/ alanmi/abc/. Accessed Feb 2017
[12] Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuxmv symbolic model checker. In: Biere A, Bloem R (eds) Proceedings of the computer aided verification, series. Lecture Notes in Computer Science, vol 8559. Springer International Publishing, pp 334-342. doi:10.1007/978-3-319-08867-9_22 · Zbl 1267.94144
[13] Hassan Z, Bradley AR, Somenzi F (2013) Better generalization in IC3. FMCAD, Portland, pp 57-164
[14] Vizel Y, Grumberg O, Shoham S (2012) Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD, Cambridge, pp 173-181
[15] Chockler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. FMCAD, Austin, pp 135-143
[16] Griggio A, Roveri M (2015) Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans Comput Aided Des. doi:10.1109/TCAD.2015.2481869 · doi:10.1109/TCAD.2015.2481869
[17] Järvisalo M, Biere A, Heule M (2012) Simulating circuit-level simplifications on CNF. J Autom Reason 49(4):583-619. doi:10.1007/s10817-011-9239-9 · Zbl 1267.94144 · doi:10.1007/s10817-011-9239-9
[18] Tseitin GS (1983) On the complexity of derivation in propositional calculus. In: Automation of reasoning: 2: classical papers on computational logic 1967-1970. pp 466-483. doi:10.1007/978-3-642-81955-1_28
[19] Eén N, Mishchenko A, Sörensson N (2007) Applying logic synthesis for speeding up SAT. Theory and applications of satisfiability testing, series, LNCS, vol 4501. Springer, Lisbon, May 28-31 2007, pp 272-286. doi:10.1007/978-3-540-72788-0_26 · Zbl 1214.68351
[20] Bradley AR, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. FMCAD, Austin, pp 173-180. doi:10.1109/FAMCAD.2007.15
[21] Eén N, Sörensson N (2016) The minisat SAT solver. http://minisat.se. Accessed Feb 2017 · Zbl 1204.68191
[22] Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th design automation Conference on Las Vegas, Nevada. IEEE Computer Society, June 2001. doi:10.1145/378239.379017
[23] Eén N, Sörensson N (2003) Temporal induction by incremental sat solving. Electron Notes Theor Comput Sci 89(4):543-560. doi:10.1016/S1571-0661(05)82542-3 · Zbl 1271.68215 · doi:10.1016/S1571-0661(05)82542-3
[24] Björk M (2009) Successful SAT encoding techniques. In: Journal on satisability, boolean modeling and computation. Addendum, IOS Press
[25] Plaisted DA, Greenbaum S (1986) A structure-preserving clause form translation. J Symb Comput 2(3):293-304. doi:10.1016/S0747-7171(86)80028-1 · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1
[26] Eén N (2007) Practical sat: a tutorial on applied satisfiability solving. Slides of invited talk at FMCAD, 2007. www.cs.utexas.edu/users/hunt/FMCAD/2007/presentations/practicalsat.html. Accessed 02 May 2016
[27] Nadel A, Ryvchin V, Strichman O (2013) Efficient MUS extraction with resolution. FMCAD, Portland, pp 197-200
[28] Jin H, Somenzi F (2005) CirCUs: a hybrid satisfiability solver. In: Theory and applications of satisfiability testing. Vancouver, BC, Canada, 2005. pp 211-223. doi:10.1007/11527695_17 · Zbl 1122.68606
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.