{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T22:46:30Z","timestamp":1747867590086},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"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-40970-2_14","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T07:14:55Z","timestamp":1465542895000},"page":"212-227","source":"Crossref","is-referenced-by-count":8,"title":["Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT"],"prefix":"10.1007","author":[{"given":"Mathias","family":"Soeken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Petkovska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baruch","family":"Sterin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Ienne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giovanni","family":"De Micheli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"issue":"3","key":"14_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/264995.264996","volume":"2","author":"L Benini","year":"1997","unstructured":"Benini, L., Micheli, G.D.: A survey of Boolean matching techniques for library binding. ACM Trans. Design Autom. Electr. Syst. 2(3), 193\u2013226 (1997)","journal-title":"ACM Trans. Design Autom. Electr. Syst."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Brand, D.: Verification of large synthesized designs. In: Proceedings of the International Conference on Computer Aided Design, pp. 534\u2013537 (1993)","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"12","key":"14_CR4","doi-asserted-by":"crossref","first-page":"2894","DOI":"10.1109\/TCAD.2006.882484","volume":"25","author":"S Chatterjee","year":"2006","unstructured":"Chatterjee, S., Mishchenko, A., Brayton, R.K., Wang, X., Kam, T.: Reducing structural bias in technology mapping. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 25(12), 2894\u20132903 (2006)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Debnath, D., Sasao, T.: Efficient computation of canonical form for Boolean matching in large libraries. In: Proceedings of the Asia and South Pacific Design Automation Conference, pp. 591\u201396 (2004)","DOI":"10.1109\/ASPDAC.2004.1337660"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 E\u00e9n","year":"2007","unstructured":"E\u00e9n, 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)"},{"key":"14_CR7","unstructured":"Goto, E., Takahasi, H.: Some theorems useful in threshold logic for enumerating Boolean functions. In: International Federation for Information Processing Congress, pp. 747\u201352 (1962)"},{"key":"14_CR8","volume-title":"Introduction to Switching and Automata Theory","author":"MA Harrison","year":"1965","unstructured":"Harrison, M.A.: Introduction to Switching and Automata Theory. McGraw-Hill, New York (1965)"},{"key":"14_CR9","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/PGEC.1963.263531","volume":"12","author":"L Hellerman","year":"1963","unstructured":"Hellerman, L.: A catalog of three-variable Or-inverter and And-inverter logical circuits. IEEE Trans. Electr. Comput. 12, 198\u2013223 (1963)","journal-title":"IEEE Trans. Electr. Comput."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Huang, Z., Wang, L., Nasikovskiy, Y., Mishchenko, A.: Fast Boolean matching based on NPN classification. In: Proceedings of the 2013 International Conference on Field Programmable Technology, pp. 310\u2013313 (2013)","DOI":"10.1109\/FPT.2013.6718374"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Katebi, H., Markov, I.L.: Large-scale Boolean matching. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 771\u201376 (2010)","DOI":"10.1109\/DATE.2010.5456949"},{"key":"14_CR12","volume-title":"The Art of Computer Programming","author":"DE Knuth","year":"2011","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol. 4A. Addison-Wesley, Reading, Massachusetts (2011)"},{"key":"14_CR13","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol. 4, Fascicle 6: Satisfiability. Addison-Wesley, Reading, Massachusetts (2015)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"MW Krentel","year":"1988","unstructured":"Krentel, M.W.: The complexity of optimization problems. J. Comput. Syst. Sci. 36(3), 490\u2013509 (1988)","journal-title":"J. Comput. Syst. Sci."},{"issue":"12","key":"14_CR15","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"5","key":"14_CR16","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1109\/43.277607","volume":"12","author":"F Mailhot","year":"1993","unstructured":"Mailhot, F., Micheli, G.D.: Algorithms for technology mapping based on binary decision diagrams and on Boolean operations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 12(5), 599\u2013620 (1993)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: a fresh look at combinational logic synthesis. In: Proceedings of the 43rd Design Automation Conference, pp. 532\u2013536 (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"14_CR18","volume-title":"Logic Design and Switching Theory","author":"S Muroga","year":"1979","unstructured":"Muroga, S.: Logic Design and Switching Theory. Wiley, New York (1979)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer Aided Design, pp. 42\u201347 (1993)","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Soeken, M., Amar\u00f9, L.G., Gaillardon, P., De Micheli, G.: Optimizing majority-inverter graphs with functional hashing. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 1030\u20131035 (2016)","DOI":"10.3850\/9783981537079_0281"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Tseytin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.P. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics, pp. 115\u2013125. Springer, NewYork (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"14_CR22","volume-title":"Hacker\u2019s Delight","author":"HS Warren","year":"2012","unstructured":"Warren, H.S.: Hacker\u2019s Delight, 2nd edn. Addison-Wesley, Reading (2012)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:06:03Z","timestamp":1498305963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}