{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:40:05Z","timestamp":1750556405737,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_23","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"436-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Correct-by-Decision Solution for Simultaneous Place and Route"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Nadel","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"issue":"3","key":"23_CR1","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s00291-007-0080-9","volume":"30","author":"N Abboud","year":"2008","unstructured":"Abboud, N., Gr\u00f6tschel, M., Koch, T.: Mathematical methods for physical layout of printed circuit boards: an overview. OR Spectr. 30(3), 453\u2013468 (2008)","journal-title":"OR Spectr."},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39071-5_23"},{"issue":"3","key":"23_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":"23_CR4","doi-asserted-by":"crossref","unstructured":"Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: SAT modulo monotonic theories. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 25\u201330 January 2015, Austin, Texas, USA, pp. 3702\u20133709. AAAI Press, New York (2015)","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) [20], pp. 285\u2013301","DOI":"10.1007\/978-3-319-09284-3_22"},{"issue":"1\u20133","key":"23_CR6","first-page":"165","volume":"6","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. JSAT 6(1\u20133), 165\u2013201 (2009)","journal-title":"JSAT"},{"key":"23_CR7","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24605-3_37"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-21668-3_2","volume-title":"Computer Aided Verification","author":"A Erez","year":"2015","unstructured":"Erez, A., Nadel, A.: Finding bounded path in graph using SMT for automatic clock routing. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 20\u201336. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_2"},{"key":"23_CR9","unstructured":"Hadarean, L.: An efficient and trustworthy theory solver for bit-vectors in satisfiability modulo theories. Dissertation, New York University (2015)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-34188-5_9","volume-title":"Hardware and Software: Verification and Testing","author":"Z Khasidashvili","year":"2012","unstructured":"Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 66\u201379. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-34188-5_9"},{"key":"23_CR11","unstructured":"Nadel, A.: A correct-by-decision solution for simultaneous place and route: benchmarks and detailed results. https:\/\/goo.gl\/MNl1PE"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Nadel, A.: Routing under constraints. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 October 2016, pp. 125\u2013132. IEEE, Washington, D.C. (2016)","DOI":"10.1109\/FMCAD.2016.7886670"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242\u2013255. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31612-8_19"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) [20], pp. 206\u2013218","DOI":"10.1007\/978-3-319-09284-3_16"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Nag, S., Rutenbar, R.A.: Performance-driven simultaneous place and route for row-based FPGAs. In: DAC, pp. 301\u2013307 (1994)","DOI":"10.1145\/196244.196387"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Nag, S.K., Rutenbar, R.A.: Performance-driven simultaneous place and route for island-style FPGAs. In: Rudell, R.L., (eds.) Proceedings of the 1995 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, 5\u20139 November 1995, pp. 332\u2013338. IEEE Computer Society\/ACM, Washington, D.C. (1995)","DOI":"10.1109\/ICCAD.1995.480137"},{"issue":"2","key":"23_CR17","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1006\/jagm.1996.0046","volume":"21","author":"G Ramalingam","year":"1996","unstructured":"Ramalingam, G., Reps, T.W.: An incremental algorithm for a generalization of the shortest-path problem. J. Algorithms 21(2), 267\u2013305 (1996)","journal-title":"J. Algorithms"},{"key":"23_CR18","unstructured":"Sabharwal, A.: Symchaff: a structure-aware satisfiability solver. In: Veloso, M.M., Kambhampati, S. (eds.) Proceedings of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, 9\u201313 July 2005, Pittsburgh, Pennsylvania, USA, pp. 467\u2013474. AAAI Press\/The MIT Press, Austin (2005)"},{"key":"23_CR19","volume-title":"Algorithms for VLSI Physical Design Automation","author":"NA Sherwani","year":"1998","unstructured":"Sherwani, N.A.: Algorithms for VLSI Physical Design Automation, 3rd edn. Kluwer, Dordrecht (1998)","edition":"3"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","year":"2014","unstructured":"Sinz, C., Egly, U. (eds.): SAT 2014. LNCS, vol. 8561. Springer, Cham (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:10:19Z","timestamp":1750554619000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}