{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:08:49Z","timestamp":1725566929317},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340611"},{"type":"electronic","value":"9783642340628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34062-8_80","type":"book-chapter","created":{"date-parts":[[2012,9,7]],"date-time":"2012-09-07T08:52:58Z","timestamp":1347007978000},"page":"616-623","source":"Crossref","is-referenced-by-count":0,"title":["Complete SAT Solver Based on Set Theory"],"prefix":"10.1007","author":[{"given":"Wensheng","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guowu","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qianqi","family":"Le","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William N. N.","family":"Hung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"80_CR1","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\u00a011(1), 4\u201315 (1992)","journal-title":"IEEE Trans. CAD"},{"key":"80_CR2","first-page":"119","volume-title":"International Symposium on Field-programmable Gate Arrays","author":"R.G. Wood","year":"1997","unstructured":"Wood, R.G., Rutenbar, R.A.: FPGA routing and routability estimation via Boolean satisfiability. In: International Symposium on Field-programmable Gate Arrays, Monterey, California, United States, pp. 119\u2013125. ACM, New York (1997)"},{"key":"80_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., et al.: Symbolic Model Checking using SAT procedures instead of BDDs. In: Proc. Design Automation Conference ACM\/IEEE, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"80_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 454\u2013464. Springer, Heidelberg (2001)"},{"issue":"3","key":"80_CR5","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1109\/TVLSI.2003.812322","volume":"11","author":"X. Song","year":"2003","unstructured":"Song, X., et al.: Board-Level Multiterminal Net Assignment for the Partial Cross-Bar Architecture. IEEE Trans. VLSI Systems\u00a011(3), 511\u2013514 (2003)","journal-title":"IEEE Trans. VLSI Systems"},{"key":"80_CR6","doi-asserted-by":"crossref","unstructured":"Hung, W.N.N., Narasimhan, N.: Reference Model Based RTL Verification: An Integrated Approach. In: Proc. IEEE International High Level Design Validation and Test Workshop (HLDVT), pp. 9\u201313. IEEE (November 2004)","DOI":"10.1109\/HLDVT.2004.1431221"},{"issue":"4","key":"80_CR7","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/1027084.1027090","volume":"9","author":"W.N.N. Hung","year":"2004","unstructured":"Hung, W.N.N., et al.: Segmented channel routability via satisfiability. ACM Transactions on Design Automation of Electronic Systems\u00a09(4), 517\u2013528 (2004a)","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"issue":"12","key":"80_CR8","doi-asserted-by":"publisher","first-page":"1398","DOI":"10.1109\/TVLSI.2004.837999","volume":"12","author":"W.N.N. Hung","year":"2004","unstructured":"Hung, W.N.N., et al.: Routability Checking for Three-Dimensional Architectures. IEEE Trans. VLSI Systems\u00a012(12), 1398\u20131401 (2004b)","journal-title":"IEEE Trans. VLSI Systems"},{"issue":"9","key":"80_CR9","doi-asserted-by":"crossref","first-page":"1652","DOI":"10.1109\/TCAD.2005.858352","volume":"25","author":"W.N.N. Hung","year":"2006","unstructured":"Hung, W.N.N., et al.: Optimal Synthesis of Multiple Output Boolean Functions using a Set of Quantum Gates by Symbolic Reachability Analysis. IEEE Trans. CAD\u00a025(9), 1652\u20131663 (2006)","journal-title":"IEEE Trans. CAD"},{"issue":"9","key":"80_CR10","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1080\/00207210701650661","volume":"94","author":"F. He","year":"2007","unstructured":"He, F., et al.: A satisfiability formulation for FPGA routing with pin rearrangements. International Journal of Electronics\u00a094(9), 857\u2013868 (2007)","journal-title":"International Journal of Electronics"},{"issue":"6","key":"80_CR11","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1109\/JSEN.2008.923261","volume":"8","author":"W.N.N. Hung","year":"2008","unstructured":"Hung, W.N.N., et al.: Defect Tolerant CMOL Cell Assignment via Satisfiability. IEEE Sensors Journal\u00a08(6), 823\u2013830 (2008)","journal-title":"IEEE Sensors Journal"},{"key":"80_CR12","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F., Jin, H.: Making Deduction More Effective in SAT Solvers. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1271\u20131284 (2010)","DOI":"10.1109\/TCAD.2010.2049135"},{"key":"80_CR13","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Proceedings of the 24th AAAI Conference on Artificial Intelligence, AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"80_CR14","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J. Franco","year":"1983","unstructured":"Franco, J., Paull, M.: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics\u00a05, 77\u201387 (1983)","journal-title":"Discrete Applied Mathematics"},{"key":"80_CR15","unstructured":"Mendonca, M., Wasowski, A., Czarnecki, K.: SAT-based Analysis of Feature Models is Easy. In: Proceedings of the International Software Product Line Conference (SPLC). Software Engineering Institute, Carnegie Mellon University (2009)"},{"key":"80_CR16","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.10.027","volume":"255","author":"S. Kemper","year":"2009","unstructured":"Kemper, S.: SAT-based verification for timed component connectors. Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0255, 103\u2013118 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"80_CR17","doi-asserted-by":"crossref","unstructured":"Zhou, M., He, F., Gu, M.: An Efficient Resolution Based Algorithm for SAT. In: 2011 Fifth International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 60\u201367 (2011)","DOI":"10.1109\/TASE.2011.23"},{"key":"80_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"80_CR19","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Comms. ACM\u00a05, 394\u2013397 (1962)","journal-title":"Comms. ACM"},{"key":"80_CR20","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1613\/jair.696","volume":"12","author":"K. Xu","year":"2000","unstructured":"Xu, K., Li, W.: Exact Phase Transitions in Random Constraint Satisfaction Problems. Journal of Artificial Intelligence Research\u00a012, 93\u2013103 (2000)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"80_CR21","unstructured":"http:\/\/www.nlsde.buaa.edu.cn\/~kexu\/benchmarks\/benchmarks.html"}],"container-title":["Lecture Notes in Computer Science","Information Computing and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34062-8_80.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,25]],"date-time":"2023-06-25T16:27:40Z","timestamp":1687710460000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34062-8_80"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340611","9783642340628"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34062-8_80","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}