{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:02:28Z","timestamp":1777125748157,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_5","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"32-44","source":"Crossref","is-referenced-by-count":24,"title":["Finding Efficient Circuits Using SAT-Solvers"],"prefix":"10.1007","author":[{"given":"Arist","family":"Kojevnikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander S.","family":"Kulikov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigory","family":"Yaroslavtsev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/0020-0190(90)90036-W","volume":"35","author":"A. Chin","year":"1990","unstructured":"Chin, A.: On the depth complexity of the counting functions. Information Processing Letters\u00a035, 325\u2013328 (1990)","journal-title":"Information Processing Letters"},{"key":"5_CR2","unstructured":"E\u00e9n, N.: Practical SAT\u00a0\u2014 a tutorial on applied satisfiability solving. Slides of invited talk at FMCAD (2007)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-36553-2_37","volume-title":"Evolvable Systems: From Biology to Hardware","author":"G.G. Estrada","year":"2003","unstructured":"Estrada, G.G.: A note on designing logical circuits using SAT. In: Tyrrell, A.M., Haddow, P.C., Torresen, J. (eds.) ICES 2003. LNCS, vol.\u00a02606, pp. 410\u2013421. Springer, Heidelberg (2003)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1137\/0211033","volume":"11","author":"M.J. Fischer","year":"1982","unstructured":"Fischer, M.J., Meyer, A.R., Paterson, M.S.: \u03a9(n logn) lower bounds on length of Boolean formulas. SIAM Journal on Computing\u00a011, 416\u2013427 (1982)","journal-title":"SIAM Journal on Computing"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1109\/9780470544600","volume-title":"Evolutionary computation: The fossil record","author":"D.B. Fogel","year":"1998","unstructured":"Fogel, D.B.: Evolutionary computation: The fossil record. IEEE Press, New York (1998)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Kamath, A.P., Karmarkar, N.K., Ramakrishnan, K.G., Resende, M.G.C.: An interior point approach to boolean vector function synthesis. In: Proceedings of the 36th International Midwest Symposium on Circuits and Systems (MSCAS 1993), pp. 185\u2013189 (1993)","DOI":"10.1109\/MWSCAS.1993.343098"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Khatri, S., Shenoy, N.: Logic synthesis. In: Scheffer, L., Lavagno, L., Martin, G. (eds.) Electronic Design Automation For Integrated Circuits Handbook. CRC Press, Taylor & Francis Group (2006)","DOI":"10.1201\/9781420007954.ch2"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF01405045","volume":"9","author":"V.M. Khrapchenko","year":"1971","unstructured":"Khrapchenko, V.M.: Complexity of the realization of a linear function in the case of \u03a0-circuits. Math. Notes Acad. Sciences\u00a09, 21\u201323 (1971)","journal-title":"Math. Notes Acad. Sciences"},{"key":"5_CR9","volume-title":"Computer Arithmetic Algorithms","author":"I. Koren","year":"1993","unstructured":"Koren, I.: Computer Arithmetic Algorithms. Prentice Hall, Englewood Cliffs (1993)"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell Systems Technical Journal\u00a038, 985\u2013999 (1959)","journal-title":"Bell Systems Technical Journal"},{"key":"5_CR11","unstructured":"Massey, J.L.: The difficulty with difficulty. In: A Guide to the Transparencies from the EUROCRYPT 1996 IACR Distinguished Lecture (1996)"},{"key":"5_CR12","volume-title":"Logic Design Principles: with emphasis on testable semicustom circuits","author":"E.J. McCluskey","year":"1986","unstructured":"McCluskey, E.J.: Logic Design Principles: with emphasis on testable semicustom circuits. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"5_CR13","volume-title":"Slognost\u2019 bulevikh funktsii","author":"R.G. Nigmatullin","year":"1991","unstructured":"Nigmatullin, R.G.: Slognost\u2019 bulevikh funktsii. Moskva, Nauka (1991) (in Russian)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/BF01271371","volume":"3","author":"M.S. Paterson","year":"1993","unstructured":"Paterson, M.S., Zwick, U.: Shallow circuits and concise formulae for multiple addition and multiplication. Computational Complexity\u00a03, 262\u2013291 (1993)","journal-title":"Computational Complexity"},{"issue":"2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Aarti, G.: A survey of recent advances in SAT-based formal verification. International Journal on Software Tools for Technology Transfer\u00a07(2), 156\u2013173 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"5_CR16","first-page":"354","volume":"31","author":"A.A. Razborov","year":"1985","unstructured":"Razborov, A.A.: Lower bounds for the monotone complexity of some Boolean functions. Soviet Math. Doklady\u00a031, 354\u2013357 (1985)","journal-title":"Soviet Math. Doklady"},{"issue":"4598","key":"5_CR17","first-page":"671","volume":"220","author":"C.D. Gelatt","year":"1983","unstructured":"Gelatt, C.D., Kirkpatrick, S., Vecchi, M.P.: Optimization by simulated annealing. Science, New Series\u00a0220(4598), 671\u2013680 (1983)","journal-title":"Science, New Series"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/BF02246615","volume":"13","author":"C. Schnorr","year":"1974","unstructured":"Schnorr, C.: Zwei lineare untere Schranken f\u00fcr die Komplexit\u00e4t Boolescher Funktionen. Computing\u00a013, 155\u2013171 (1974)","journal-title":"Computing"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/BF01683282","volume":"10","author":"L.J. Stockmeyer","year":"1977","unstructured":"Stockmeyer, L.J.: On the combinational complexity of certain symmetric Boolean functions. Mathematical Systems Theory\u00a010, 323\u2013336 (1977)","journal-title":"Mathematical Systems Theory"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0020-0190(87)90137-2","volume":"24","author":"D.C. Leijenhorst van","year":"1987","unstructured":"van Leijenhorst, D.C.: A note on the formula size of the \u201cmod k\u201d functions. Information Processing Letters\u00a024, 223\u2013224 (1987)","journal-title":"Information Processing Letters"},{"issue":"4","key":"5_CR21","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/1466390.1466401","volume":"39","author":"R. Williams","year":"2008","unstructured":"Williams, R.: Applying practice to theory. ACM SIGACT News\u00a039(4), 37\u201352 (2008)","journal-title":"ACM SIGACT News"},{"key":"5_CR22","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1137\/0220032","volume":"20","author":"U. Zwick","year":"1991","unstructured":"Zwick, U.: A 4n lower bound on the combinational complexity of certain symmetric boolean functions over the basis of unate dyadic Boolean functions. SIAM Journal on Computing\u00a020, 499\u2013505 (1991)","journal-title":"SIAM Journal on Computing"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T20:10:08Z","timestamp":1552075808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}