{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T04:15:28Z","timestamp":1749701728166,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319490519"},{"type":"electronic","value":"9783319490526"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-49052-6_1","type":"book-chapter","created":{"date-parts":[[2016,10,31]],"date-time":"2016-10-31T14:34:50Z","timestamp":1477924490000},"page":"1-17","source":"Crossref","is-referenced-by-count":4,"title":["SAT-Based Combinational and Sequential Dependency Computation"],"prefix":"10.1007","author":[{"given":"Mathias","family":"Soeken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Raiola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baruch","family":"Sterin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giovanni","family":"De Micheli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Sauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Design Automation Conference, pp. 317\u2013320 (1999)","DOI":"10.1109\/DAC.1999.781333"},{"key":"1_CR2","unstructured":"Albrecht, C.: IWLS 2005 benchmarks. In: International Workshop for Logic Synthesis (IWLS) (2005). http:\/\/www.iwls.org"},{"volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","key":"1_CR3","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_5"},{"issue":"8","key":"1_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Symposium on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"issue":"3","key":"1_CR7","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/54.867894","volume":"17","author":"F Corno","year":"2000","unstructured":"Corno, F., Reorda, M., Squillero, G.: RT-level ITC\u201999 benchmarks and first ATPG results. IEEE Des. Test Comput. 17(3), 44\u201353 (2000)","journal-title":"IEEE Des. Test Comput."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Saab, D.G., Abraham, J.A., Vedula, V.M.: Formal verification using bounded model checking: SAT versus sequential ATPG engines. In: VLSI Design, pp. 243\u2013248 (2003)","DOI":"10.1109\/ICVD.2003.1183144"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N Een","year":"2007","unstructured":"Een, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272\u2013286. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_26"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24605-3_37"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"van Eijk, C.A.J., Jess, J.A.G.: Exploiting functional dependencies in finite state machine verification. In: European Design and Test Conference, pp. 9\u201314 (1996)","DOI":"10.1109\/EDTC.1996.494119"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-27813-9_21","volume-title":"Computer Aided Verification","author":"J-HR Jiang","year":"2004","unstructured":"Jiang, J.-H.R., Brayton, R.K.: Functional dependency for verification reduction. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 268\u2013280. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_21"},{"issue":"4","key":"1_CR13","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1109\/TC.2010.12","volume":"59","author":"JR Jiang","year":"2010","unstructured":"Jiang, J.R., Lee, C., Mishchenko, A., Huang, C.: To SAT or not to SAT: scalable exploration of functional dependency. IEEE Trans. Comput. 59(4), 457\u2013467 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Katebi, H., Markov, I.L.: Large-scale Boolean matching. In: Design, Automation and Test in Europe, pp. 771\u2013776 (2010)","DOI":"10.1109\/DATE.2010.5456949"},{"issue":"1","key":"1_CR15","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee, T.: Test pattern generation using Boolean satisfiability. IEEE Trans. CAD Integr. Circuits Syst. 11(1), 4\u201315 (1992)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Lee, C., Jiang, J.R., Huang, C., Mishchenko, A.: Scalable exploration of functional dependency by interpolation and incremental SAT solving. In: International Conference on Computer-Aided Design, pp. 227\u2013233 (2007)","DOI":"10.1109\/ICCAD.2007.4397270"},{"issue":"3","key":"1_CR17","first-page":"115","volume":"9","author":"LA Levin","year":"1973","unstructured":"Levin, L.A.: Universal sequential search problems. Probl. Inf. Transm. 9(3), 115\u2013116 (1973)","journal-title":"Probl. Inf. Transm."},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). doi: 10.1007\/3-540-40922-X_8"},{"key":"1_CR19","unstructured":"Marh\u00f6fer, M.: An approach to modular test generation based on the transparency of modules. In: IEEE CompEuro 1987, pp. 403\u2013406 (1987)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_1"},{"issue":"1","key":"1_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TEC.1961.5219145","volume":"10","author":"R McNaughton","year":"1961","unstructured":"McNaughton, R.: Unate truth functions. IRE Trans. Electron. Comput. 10(1), 1\u20136 (1961)","journal-title":"IRE Trans. Electron. Comput."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to combinational equivalence checking. In: International Conference on Computer-Aided Design, pp. 836\u2013843 (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"issue":"2","key":"1_CR23","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1016091418702","volume":"21","author":"J Mohnke","year":"2002","unstructured":"Mohnke, J., Molitor, P., Malik, S.: Limits of using signatures for permutation independent Boolean comparison. Form. Methods Syst. Des. 21(2), 167\u2013191 (2002)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Murray, B.T., Hayes, J.P.: Test propagation through modules and circuits. In: International Test Conference, pp. 748\u2013757 (1991)","DOI":"10.1109\/TEST.1991.519740"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Reimer, S., Sauer, M., Schubert, T., Becker, B.: Using MaxBMC for pareto-optimal circuit initialization. In: Conference on Design, Automation and Test in Europe, pp. 1\u20136, March 2014","DOI":"10.7873\/DATE2014.161"},{"issue":"99","key":"1_CR26","first-page":"1","volume":"PP","author":"M Sauer","year":"2015","unstructured":"Sauer, M., Becker, B., Polian, I.: PHAETON: a SAT-based framework for timing-aware path sensitization. IEEE Trans. Comput. PP(99), 1 (2015)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Sauer, M., Reimer, S., Polian, I., Schubert, T., Becker, B.: Provably optimal test cube generation using quantified Boolean formula solving. In: ASP Design Automation Conference, pp. 533\u2013539 (2013)","DOI":"10.1109\/ASPDAC.2013.6509651"},{"key":"1_CR28","unstructured":"Schubert, T., Reimer, S.: antom (2013). https:\/\/projects.informatik.uni-freiburg.de\/projects\/antom"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Soeken, M., Sterin, B., Drechsler, R., Brayton, R.K.: Reverse engineering with simulation graphs. In: Formal Methods in Computer-Aided Design, pp. 152\u2013159 (2015)","DOI":"10.1109\/FMCAD.2015.7542265"},{"issue":"12\u201313","key":"1_CR30","doi-asserted-by":"crossref","first-page":"850","DOI":"10.1016\/j.artint.2010.05.002","volume":"174","author":"C Solnon","year":"2010","unstructured":"Solnon, C.: AllDifferent-based filtering for subgraph isomorphism. Artif. Intell. 174(12\u201313), 850\u2013864 (2010)","journal-title":"Artif. Intell."},{"issue":"9","key":"1_CR31","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P Stephan","year":"1996","unstructured":"Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Combinational test generation using satisfiability. IEEE Trans. CAD Integr. Circuits Syst. 15(9), 1167\u20131176 (1996)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"1_CR32","unstructured":"Tseytin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic (1968)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-49052-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T22:44:10Z","timestamp":1749681850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-49052-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319490519","9783319490526"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-49052-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}