{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T05:02:52Z","timestamp":1780981372717,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642390708","type":"print"},{"value":"9783642390715","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_16","type":"book-chapter","created":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T21:23:17Z","timestamp":1372022597000},"page":"208-223","source":"Crossref","is-referenced-by-count":10,"title":["A Constraint Satisfaction Approach for Programmable Logic Detailed Placement"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Mihal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Teig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: National Conference on Artificial Intelligence, pp. 613\u2013619 (July 2002)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-63465-7_226","volume-title":"Field Programmable Logic and Applications","author":"V. Betz","year":"1997","unstructured":"Betz, V., Rose, J.: VPR: A new packing, placement, and routing tool for FPGA research. In: Glesner, M., Luk, W. (eds.) FPL 1997. LNCS, vol.\u00a01304, pp. 213\u2013222. Springer, Heidelberg (1997)"},{"issue":"3","key":"16_CR3","first-page":"195","volume":"1","author":"D. Chen","year":"2006","unstructured":"Chen, D., Cong, J., Pan, P.: FPGA design automation: A survey. Foundations and Trends in Electronic Design Automation\u00a01(3), 195\u2013330 (2006)","journal-title":"Foundations and Trends in Electronic Design Automation"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Devadas, S.: Optimal layout via Boolean satisfiability. In: IEEE International Conference on Computer-Aided Design, pp. 294\u2013297 (November 1989)","DOI":"10.1109\/ICCAD.1989.76956"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Drechsler, R., Eggersgl\u00fc\u00df, S., Fey, G., Tille, D.: Test Pattern Generation using Boolean Proof Engines. Springer (2009)","DOI":"10.1007\/978-90-481-2360-5"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: First Intl. Workshop on Bounded Model Checking, vol.\u00a089, pp. 543\u2013560 (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31612-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"V. Ganesh","year":"2012","unstructured":"Ganesh, V., O\u2019Donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: A programmatic SAT solver for the RNA-folding problem. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 143\u2013156. Springer, Heidelberg (2012)"},{"issue":"2","key":"16_CR9","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1147\/rd.102.0135","volume":"10","author":"T.I. Kirkpatrick","year":"1966","unstructured":"Kirkpatrick, T.I., Clark, N.R.: PERT as an aid to logic design. IBM Journal of Research and Development\u00a010(2), 135\u2013141 (1966)","journal-title":"IBM Journal of Research and Development"},{"issue":"12","key":"16_CR10","doi-asserted-by":"publisher","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.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: International Conference on Computer-Aided Design, pp. 50\u201357 (2004)","DOI":"10.1109\/ICCAD.2004.1382542"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1561\/1000000005","volume":"2","author":"I. Kuon","year":"2008","unstructured":"Kuon, I., Tessier, R., Rose, J.: FPGA architecture: Survey and challenges. Foundations and Trends in Electronic Design Automation\u00a02(2), 135\u2013253 (2008)","journal-title":"Foundations and Trends in Electronic Design Automation"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-31612-8_47","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M.H. Liffiton","year":"2012","unstructured":"Liffiton, M.H., Maglalang, J.C.: A cardinality solver: More expressive constraints for free. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 485\u2013486. Springer, Heidelberg (2012)"},{"key":"16_CR14","unstructured":"Mishchenko, A., Brayton, R., Jiang, J.R., Jang, S.: SAT-based logic optimization and resynthesis. In: Intl. Workshop on Logic and Synthesis, pp. 358\u2013364 (May 2007)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Nam, G., Aloul, F., Sakallah, K., Rutenbar, R.: A comparative study of two Boolean formulations of FPGA detailed routing constraints. IEEE Transactions on Computers 53(6) (June 2004)","DOI":"10.1109\/TC.2004.1"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Nam, G., Sakallah, K., Rutenbar, R.: Satisfiability-based layout revisited: Detailed routing of complex FPGAs via search-based Boolean SAT. In: Intl. Symposium on Field Programmable Gate Arrays, pp. 167\u2013175 (1999)","DOI":"10.1145\/296399.296450"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O. Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via lazy clause generation. Constraints\u00a014(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"16_CR19","unstructured":"Seshia, S.: Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. PhD thesis, Carnegie Mellon University (2005)"},{"key":"16_CR20","unstructured":"Various. OpenCores open source hardware IP cores (April 2013), \nhttp:\/\/opencores.org"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Glenn Wood, R., Rutenbar, R.: FPGA routing and routability estimation via Boolean satisfiability. IEEE Transactions on VLSI 6(2) (June 1998)","DOI":"10.1109\/92.678873"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T04:46:20Z","timestamp":1780980380000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}