{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T22:46:38Z","timestamp":1747867598341},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319672946"},{"type":"electronic","value":"9783319672953"}],"license":[{"start":{"date-parts":[[2017,11,16]],"date-time":"2017-11-16T00:00:00Z","timestamp":1510790400000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-67295-3_8","type":"book-chapter","created":{"date-parts":[[2017,11,15]],"date-time":"2017-11-15T12:36:44Z","timestamp":1510749404000},"page":"169-188","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Progressive Generation of Canonical Irredundant Sums of Products Using a SAT Solver"],"prefix":"10.1007","author":[{"given":"Ana","family":"Petkovska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Novo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muhsen","family":"Owaida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Ienne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,16]]},"reference":[{"key":"8_CR1","unstructured":"L. Amar\u00f9, P.E. Gaillardon, A. Burg, G. De Micheli, Data compression via logic synthesis, in Proceedings of the Asia and South Pacific Design Automation Conference, Yokohama (2014), pp. 628\u201333"},{"key":"8_CR2","unstructured":"Berkeley Logic Synthesis and Verification Group, Berkeley, Calif.: ABC: A system for sequential synthesis and verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"8_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"RK Brayton","year":"1984","unstructured":"R.K. Brayton, G.D. Hachtel, C.T. McMullen, A.L. Sangiovanni Vincentelli, Logic Minimization Algorithms for VLSI Synthesis (Kluwer Academic, Boston, 1984)"},{"issue":"3","key":"8_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1754405.1754411","volume":"15","author":"K Chang","year":"2010","unstructured":"K. Chang, V. Bertacco, I.L. Markov, A. Mishchenko, Logic synthesis and circuit customization using extensive external don\u2019t-cares. ACM Trans. Des. Autom. Electron. Syst. 15(3), 1\u201324 (2010)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"C. Condrat, P. Kalla, S. Blair, Logic synthesis for integrated optics, in Proceedings of the 21st ACM Great Lakes Symposium on VLSI, Lausanne (2011), pp. 13\u201318","DOI":"10.1145\/1973009.1973013"},{"issue":"2","key":"8_CR6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0167-9260(94)00007-7","volume":"17","author":"O Coudert","year":"1994","unstructured":"O. Coudert, Two-level logic minimization: An overview. Integr. VLSI J. 17(2), 97\u2013140 (1994)","journal-title":"Integr. VLSI J."},{"key":"8_CR7","volume-title":"Implicit prime cover computation: An overview, in Proceedings of the Synthesis and Simulation Meeting and International Interchange, Nara","author":"O Coudert","year":"1993","unstructured":"O. Coudert, J.C. Madre, H. Fraisse, H. Touati, Implicit prime cover computation: An overview, in Proceedings of the Synthesis and Simulation Meeting and International Interchange, Nara (1993)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"N. E\u00e9n, N. S\u00f6rensson, An extensible SAT-solver, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, vol. 2919 (Springer, Berlin, 2003), pp. 502\u201318","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"5","key":"8_CR9","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1109\/43.79502","volume":"10","author":"A Ghosh","year":"1991","unstructured":"A. Ghosh, S. Devadas, A.R. Newton, Test generation and verification for highly sequential circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 10(5), 652\u201367 (1991)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"3","key":"8_CR10","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1016\/j.ijar.2006.06.026","volume":"45","author":"AF Gobi","year":"2007","unstructured":"A.F. Gobi, W. Pedrycz, Fuzzy modelling through logic optimization. Int. J. Approx. Reason. 45(3), 488\u2013510 (2007)","journal-title":"Int. J. Approx. Reason."},{"issue":"4","key":"8_CR11","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1109\/TC.2010.12","volume":"C-59","author":"JHR Jiang","year":"2010","unstructured":"J.H.R. Jiang, C.C. Lee, A. Mishchenko, C.Y.R. Huang, To SAT or not to SAT: Scalable exploration of functional dependency. IEEE Trans. Comput. C-59(4), 457\u201367 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR12","unstructured":"D.E. Knuth, Fascicle 6: Satisfiability, in The Art of Computer Programming, vol. 19 (Addison-Wesley, Reading, 2015)"},{"issue":"11","key":"8_CR13","doi-asserted-by":"crossref","first-page":"2076","DOI":"10.1109\/JPROC.2015.2480891","volume":"103","author":"VN Kravets","year":"2015","unstructured":"V.N. Kravets, Application of a key-value paradigm to logic factoring. Proc. IEEE 103(11), 2076\u201392 (2015)","journal-title":"Proc. IEEE"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"R.R. Lee, J.H.R. Jiang, W.L. Hung, Bi-decomposing large Boolean functions via interpolation and satisfiability solving, in Proceedings of the 45th Design Automation Conference, Anaheim, CA (2008), pp. 636\u201341","DOI":"10.1145\/1391469.1391634"},{"key":"8_CR15","unstructured":"H.P. Lin, J.H.R. Jiang, R.R. Lee, To SAT or not to SAT: Ashenhurst decomposition in a large scale, in Proceedings of the International Conference on Computer Aided Design, San Jose, CA (2008), pp. 32\u201337"},{"issue":"6","key":"8_CR16","doi-asserted-by":"crossref","first-page":"1417","DOI":"10.1002\/j.1538-7305.1956.tb03835.x","volume":"35","author":"EJ McCluskey","year":"1956","unstructured":"E.J. McCluskey, Minimization of Boolean functions. Bell Syst. Tech. J. 35(6), 1417\u201344 (1956)","journal-title":"Bell Syst. Tech. J."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Interpolation and SAT-based model checking, in Proceedings of the International Conference on Computer Aided Verification, vol. 2725 (Springer, Berlin, 2003), pp. 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"8_CR18","unstructured":"S. Minato, Fast generation of irredundant sum-of-products forms from binary decision diagrams, in Proceedings of Synthesis and Simulation Meeting and International Interchange, Kobe (1992), pp. 64\u201373"},{"key":"8_CR19","unstructured":"A. Mishchenko, R.K. Brayton, SAT-based complete don\u2019t-care computation for network optimization, in Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, Munich (2005), pp. 412\u201317"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"A. Mishchenko, R. Brayton, S. Jang, V.N. Kravets, Delay optimization using SOP balancing, in Proceedings of the International Conference on Computer Aided Design, San Jose, CA (2011), pp. 375\u201382","DOI":"10.1109\/ICCAD.2011.6105357"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"A. Morgado, J.P.M. Silva, Good learning and implicit model enumeration, in Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence, Hong Kong (2005), pp. 131\u201336","DOI":"10.1109\/ICTAI.2005.69"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"A. Nadel, Generating diverse solutions in SAT, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, Ann Arbor, MI (2011), pp. 287\u2013301","DOI":"10.1007\/978-3-642-21581-0_23"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"A. Nadel, V. Ryvchin, Bit-vector optimization, in Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven (2016), pp. 851\u201367","DOI":"10.1007\/978-3-662-49674-9_53"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"A. Petkovska, A. Mishchenko, M. Soeken, G. De Micheli, R. Brayton, P. Ienne, Fast generation of lexicographic satisfiable assignments: Enabling canonicity in SAT-based applications, in Proceedings of the International Conference on Computer Aided Design, Austin, TX (2016)","DOI":"10.1145\/2966986.2967040"},{"issue":"6","key":"8_CR25","doi-asserted-by":"crossref","first-page":"778","DOI":"10.1109\/43.137523","volume":"11","author":"J Rajski","year":"1992","unstructured":"J. Rajski, J. Vasudevamurthy, The testability-preserving concurrent decomposition and factorization Boolean expressions. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 11(6), 778\u201393 (1992)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"5","key":"8_CR26","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1109\/TCAD.1987.1270318","volume":"6","author":"RL Rudell","year":"1987","unstructured":"R.L. Rudell, A.L. Sangiovanni-Vincentelli, Multiple-valued minimization for PLA optimization. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 6(5), 727\u201350 (1987)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"S. Sapra, M. Theobald, E.M. Clarke, SAT-based algorithms for logic minimization, in Proceedings of the 21st IEEE International Conference on Computer Design, San Jose, CA (2003), p. 510","DOI":"10.1109\/ICCD.2003.1240948"},{"key":"8_CR28","unstructured":"The EPFL Combinational Benchmark Suite, Multi-output PLA benchmarks, http:\/\/lsi.epfl.ch\/benchmarks"},{"key":"8_CR29","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970, Symbolic Computation","author":"GS Tseitin","year":"1983","unstructured":"G.S. Tseitin, On the complexity of derivation in propositional calculus, in Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970, Symbolic Computation, ed. by J. Siekmann, G. Wrightson (Springer, Berlin, 1983), pp. 466\u201383"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"A.K. Verma, P. Brisk, P. Ienne, Iterative layering: Optimizing arithmetic circuits by structuring the information flow, in Proceedings of the International Conference on Computer Aided Design, San Jose, CA (2009), pp. 797\u2013804","DOI":"10.1145\/1687399.1687547"},{"issue":"3","key":"8_CR31","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1109\/TCAD.2004.823348","volume":"23","author":"J Yuan","year":"2004","unstructured":"J. Yuan, A. Aziz, C. Pixley, K. Albin, Simplifying Boolean constraint solving for random simulation-vector generation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(3), 412\u2013420 (2004)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."}],"container-title":["Advanced Logic Synthesis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67295-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T05:19:21Z","timestamp":1570339161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67295-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,16]]},"ISBN":["9783319672946","9783319672953"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67295-3_8","relation":{},"subject":[],"published":{"date-parts":[[2017,11,16]]}}}