Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
We provide in this section an informal and high-level description of CNF encoding techniques, we refer the interested reader to the more rigorous and detailed description provided in [17].
References
Cabodi G, Mishchenko A, Palena M (2013) Trading-off incrementality and dynamic restart of multiple solvers in IC3. DIFTS, Portland
Bradley AR (2011) SAT-based model checking without unrolling. VMCAI, Austin
Biere A, Jussila T (2008) The model checking competition web page. http://fmv.jku.at/hwmcc. Accessed Feb 2017
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
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
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
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
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
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
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
Mishchenko A (2007) ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/~alanmi/abc/. Accessed Feb 2017
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
Hassan Z, Bradley AR, Somenzi F (2013) Better generalization in IC3. FMCAD, Portland, pp 57–164
Vizel Y, Grumberg O, Shoham S (2012) Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD, Cambridge, pp 173–181
Chockler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. FMCAD, Austin, pp 135–143
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
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
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
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
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
Eén N, Sörensson N (2016) The minisat SAT solver. http://minisat.se. Accessed Feb 2017
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
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
Björk M (2009) Successful SAT encoding techniques. In: Journal on satisability, boolean modeling and computation. Addendum, IOS Press
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
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
Nadel A, Ryvchin V, Strichman O (2013) Efficient MUS extraction with resolution. FMCAD, Portland, pp 197–200
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
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Cabodi, G., Camurati, P.E., Mishchenko, A. et al. SAT solver management strategies in IC3: an experimental approach. Form Methods Syst Des 50, 39–74 (2017). https://doi.org/10.1007/s10703-017-0272-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-017-0272-0