{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T05:10:01Z","timestamp":1748495401898,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_2","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"20-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Finding Bounded Path in Graph Using SMT for Automatic Clock Routing"],"prefix":"10.1007","author":[{"given":"Amit","family":"Erez","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Nadel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"2_CR1","unstructured":"Audemard, G., Simon, L.: The Glucose SAT Solver. http:\/\/www.labri.fr\/perso\/lsimon\/glucose\/ . Accessed: 05\u2013January\u20132015"},{"key":"2_CR2","unstructured":"Audemard, G., Simon, L.: GLUCOSE 2.1: aggressive, but reactive, clause database management, dynamic restarts (system description). In: Pragmatics of SAT 2012 (POS 2012), June 2012"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.09.042","volume":"125","author":"C Barrett","year":"2005","unstructured":"Barrett, C., Donham, J.: Combining SAT methods with non-clausal decision heuristics. Electr. Notes Theor. Comput. Sci. 125(3), 3\u201312 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: version 2.0. In: Gupta, A., Kroening, D., (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh (2010)"},{"key":"2_CR5","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling. http:\/\/fmv.jku.at\/lingeling\/ . Accessed: 05\u2013January\u20132015"},{"key":"2_CR6","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition. In: Proceedings of SAT Competition 2013, p. 51 (2013)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-319-09284-3_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Biere","year":"2014","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285\u2013301. Springer, Heidelberg (2014)"},{"key":"2_CR8","volume-title":"Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T.: Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"2_CR11","unstructured":"Erez, A., Nadel, A.: Finding bounded path in graph using SMT for automatic clock routing: Benchmarks and detailed results. http:\/\/goo.gl\/sM4xxz"},{"key":"2_CR12","unstructured":"Amit Erez and Alexander Nadel. Finding bounded path in graph using SMT for automatic clock routing: Extended version. https:\/\/goo.gl\/jtq669"},{"issue":"7","key":"2_CR13","doi-asserted-by":"publisher","first-page":"945","DOI":"10.1109\/12.55696","volume":"39","author":"JP Fishburn","year":"1990","unstructured":"Fishburn, J.P.: Clock skew optimization. IEEE Trans. Comput. 39(7), 945\u2013951 (1990)","journal-title":"IEEE Trans. Comput."},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Gao, Q., Yao, H., Zhou, Q., Cai, Y.: A novel detailed routing algorithm with exact matching constraint for analog and mixed signal circuits. In: Proceedings of the 12th International Symposium on Quality Electronic Design (ISQED 2011), pp. 36\u201341. IEEE, Santa Clara, 14\u201316 March 2011","DOI":"10.1109\/ISQED.2011.5770700"},{"key":"2_CR17","unstructured":"Hadarean, L.: An Efficient and Trustworthy Theory Solver for Bit-vectors in Satisfiability Modulo Theories. dissertation, New York University (2015)"},{"issue":"1","key":"2_CR18","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00453-011-9583-5","volume":"65","author":"K Ioannidou","year":"2013","unstructured":"Ioannidou, K., Nikolopoulos, S.D.: The longest path problem is polynomial on cocomparability graphs. Algorithmica 65(1), 177\u2013205 (2013)","journal-title":"Algorithmica"},{"issue":"4","key":"2_CR19","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1137\/0211056","volume":"11","author":"A Itai","year":"1982","unstructured":"Itai, A., Papadimitriou, C.H., Szwarcfiter, J.L.: Hamilton paths in grid graphs. SIAM J. Comput. 11(4), 676\u2013686 (1982)","journal-title":"SIAM J. Comput."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Chaff, S.M.: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM, Las Vegas, 18\u201322 June 2001","DOI":"10.1145\/378239.379017"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1007\/978-3-319-08867-9_44","volume-title":"Computer Aided Verification","author":"A Nadel","year":"2014","unstructured":"Nadel, A.: Bit-vector rewriting with automatic rule generation. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 663\u2013679. Springer, Heidelberg (2014)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Ozdal, M.M., Hentschke, R.F.: Maze routing algorithms with exact matching constraints for analog and mixed signal designs. In: 2012 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD 2012), pp. 130\u2013136. IEEE, San Jose, 5\u20138 November 2012","DOI":"10.1145\/2429384.2429409"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Ryzhenko, N., Burns, S.: Standard cell routing via boolean satisfiability. In: Groeneveld, P., Sciuto, D., Hassoun, S., (eds.) The 49th Annual Design Automation Conference DAC 2012, pp. 603\u2013612. ACM, San Francisco, 3\u20137 June 2012","DOI":"10.1145\/2228360.2228470"},{"key":"2_CR24","unstructured":"Sabharwal, A.: Symchaff: a structure-aware satisfiability solver. In: Veloso, M.M., Kambhampati, S., (eds.) Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, pp. 467\u2013474. AAAI Press \/ The MIT Press, Pittsburgh, 9\u201313 July 2005"},{"key":"2_CR25","volume-title":"Algorithms for VLSI Physical Design Automation, Chap. 8","author":"NA Sherwani","year":"1998","unstructured":"Sherwani, N.A.: Algorithms for VLSI Physical Design Automation, Chap. 8, 3rd edn. Kluwer, The Netherlands (1998)","edition":"3"},{"key":"2_CR26","volume-title":"Algorithms for VLSI Physical Design Automation, Chap. 11","author":"NA Sherwani","year":"1988","unstructured":"Sherwani, N.A.: Algorithms for VLSI Physical Design Automation, Chap. 11. Kluwer, The Netherlands (1988)"},{"issue":"5","key":"2_CR27","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1007\/978-3-319-13560-1_66","volume-title":"PRICAI 2014: Trends in Artificial Intelligence","author":"P Surynek","year":"2014","unstructured":"Surynek, P.: A simple approach to solving cooperative path-finding as propositional satisfiability works well. In: Pham, D.-N., Park, S.-B. (eds.) PRICAI 2014. LNCS, vol. 8862, pp. 827\u2013833. Springer, Heidelberg (2014)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Umans, C., Lenhart, W.: Hamiltonian cycles in solid grid graphs. In: Proceedings of the 38th Annual Symposium on Foundations of Computer Science 1997, pp. 496\u2013505, October 1997","DOI":"10.1109\/SFCS.1997.646138"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Wood, R.G., Rutenbar, R.A.: FPGA routing and routability estimation via Boolean satisfiability. pp. 222\u2013231 (1998)","DOI":"10.1109\/92.678873"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Wu, G., Jia, S., Wang, Y., Zhang, G.: An efficient clock tree synthesis method in physical design. In: IEEE International Conference of Electron Devices and Solid-State Circuits (EDSSC 2009), pp. 190\u2013193, December 2009","DOI":"10.1109\/EDSSC.2009.5394159"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:46:50Z","timestamp":1748494010000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}