{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:51:22Z","timestamp":1778082682837,"version":"3.51.4"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T00:00:00Z","timestamp":1487980800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10703-017-0272-0","type":"journal-article","created":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T04:58:00Z","timestamp":1487998680000},"page":"39-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["SAT solver management strategies in IC3: an experimental approach"],"prefix":"10.1007","volume":"50","author":[{"given":"G.","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. E.","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0605-9014","authenticated-orcid":false,"given":"M.","family":"Palena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Pasini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,25]]},"reference":[{"key":"272_CR1","volume-title":"Trading-off incrementality and dynamic restart of multiple solvers in IC3","author":"G Cabodi","year":"2013","unstructured":"Cabodi G, Mishchenko A, Palena M (2013) Trading-off incrementality and dynamic restart of multiple solvers in IC3. DIFTS, Portland"},{"key":"272_CR2","volume-title":"SAT-based model checking without unrolling","author":"AR Bradley","year":"2011","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. VMCAI, Austin"},{"key":"272_CR3","unstructured":"Biere A, Jussila T (2008) The model checking competition web page. http:\/\/fmv.jku.at\/hwmcc . Accessed Feb 2017"},{"key":"272_CR4","unstructured":"E\u00e9n N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. FMCAD, Austin, pp. 125\u2013134. ISBN:978-0-9835678-1-3"},{"key":"272_CR5","doi-asserted-by":"publisher","unstructured":"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\u2013320. DOI: 10.1145\/309847.309942","DOI":"10.1145\/309847.309942"},{"key":"272_CR6","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck 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\u2013125. ISBN:3-540-41219-0","DOI":"10.1007\/3-540-40922-X_8"},{"key":"272_CR7","doi-asserted-by":"crossref","unstructured":"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\u2013389. ISBN:3-540-41219-0","DOI":"10.1007\/3-540-40922-X_23"},{"key":"272_CR8","doi-asserted-by":"publisher","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Proceedings of the computer aided verification, series. LNCS, vol 2725. Springer, Boulder, pp 1\u201313. doi: 10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"272_CR9","doi-asserted-by":"publisher","unstructured":"Bradley AR (2012) Understanding IC3. In: Cimatti A, Sebastiani R (eds) SAT series Lecture Notes in Computer Science, vol 7317. Springer, pp. 1\u201314. doi: 10.1007\/978-3-642-31612-8_1","DOI":"10.1007\/978-3-642-31612-8_1"},{"issue":"2","key":"272_CR10","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"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\u2013227. doi: 10.1007\/s10703-011-0123-3","journal-title":"Form Methods Syst Des"},{"key":"272_CR11","unstructured":"Mishchenko A (2007) ABC: a system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/ . Accessed Feb 2017"},{"key":"272_CR12","doi-asserted-by":"publisher","unstructured":"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\u2013342. doi: 10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"272_CR13","first-page":"57","volume-title":"Better generalization in IC3","author":"Z Hassan","year":"2013","unstructured":"Hassan Z, Bradley AR, Somenzi F (2013) Better generalization in IC3. FMCAD, Portland, pp 57\u2013164"},{"key":"272_CR14","first-page":"173","volume-title":"Lazy abstraction and SAT-based reachability in hardware model checking","author":"Y Vizel","year":"2012","unstructured":"Vizel Y, Grumberg O, Shoham S (2012) Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD, Cambridge, pp 173\u2013181"},{"key":"272_CR15","first-page":"135","volume-title":"Incremental formal verification of hardware","author":"H Chockler","year":"2011","unstructured":"Chockler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. FMCAD, Austin, pp 135\u2013143"},{"key":"272_CR16","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2481869","author":"A Griggio","year":"2015","unstructured":"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","journal-title":"IEEE Trans Comput Aided Des"},{"issue":"4","key":"272_CR17","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo M, Biere A, Heule M (2012) Simulating circuit-level simplifications on CNF. J Autom Reason 49(4):583\u2013619. doi: 10.1007\/s10817-011-9239-9","journal-title":"J Autom Reason"},{"key":"272_CR18","doi-asserted-by":"publisher","unstructured":"Tseitin GS (1983) On the complexity of derivation in propositional calculus. In: Automation of reasoning: 2: classical papers on computational logic 1967\u20131970. pp 466\u2013483. doi: 10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"272_CR19","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, Mishchenko A, S\u00f6rensson N (2007) Applying logic synthesis for speeding up SAT. Theory and applications of satisfiability testing, series, LNCS, vol 4501. Springer, Lisbon, May 28\u201331 2007, pp 272\u2013286. doi: 10.1007\/978-3-540-72788-0_26","DOI":"10.1007\/978-3-540-72788-0_26"},{"key":"272_CR20","doi-asserted-by":"publisher","unstructured":"Bradley AR, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. FMCAD, Austin, pp 173\u2013180. doi: 10.1109\/FAMCAD.2007.15","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"272_CR21","unstructured":"E\u00e9n N, S\u00f6rensson N (2016) The minisat SAT solver. http:\/\/minisat.se . Accessed Feb 2017"},{"key":"272_CR22","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1145\/378239.379017"},{"issue":"4","key":"272_CR23","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) Temporal induction by incremental sat solving. Electron Notes Theor Comput Sci 89(4):543\u2013560. doi: 10.1016\/S1571-0661(05)82542-3","journal-title":"Electron Notes Theor Comput Sci"},{"key":"272_CR24","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rk M (2009) Successful SAT encoding techniques. In: Journal on satisability, boolean modeling and computation. Addendum, IOS Press","DOI":"10.3233\/SAT190085"},{"issue":"3","key":"272_CR25","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted DA, Greenbaum S (1986) A structure-preserving clause form translation. J Symb Comput 2(3):293\u2013304. doi: 10.1016\/S0747-7171(86)80028-1","journal-title":"J Symb Comput"},{"key":"272_CR26","unstructured":"E\u00e9n 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"},{"key":"272_CR27","first-page":"197","volume-title":"Efficient MUS extraction with resolution","author":"A Nadel","year":"2013","unstructured":"Nadel A, Ryvchin V, Strichman O (2013) Efficient MUS extraction with resolution. FMCAD, Portland, pp 197\u2013200"},{"key":"272_CR28","doi-asserted-by":"publisher","unstructured":"Jin H, Somenzi F (2005) CirCUs: a hybrid satisfiability solver. In: Theory and applications of satisfiability testing. Vancouver, BC, Canada, 2005. pp 211\u2013223. doi: 10.1007\/11527695_17","DOI":"10.1007\/11527695_17"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0272-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0272-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0272-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,3]],"date-time":"2020-10-03T03:09:52Z","timestamp":1601694592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0272-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,25]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["272"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0272-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,25]]}}}