{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,22]],"date-time":"2026-02-22T05:28:19Z","timestamp":1771738099643,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030349677","type":"print"},{"value":"9783030349684","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_19","type":"book-chapter","created":{"date-parts":[[2019,11,22]],"date-time":"2019-11-22T00:14:54Z","timestamp":1574381694000},"page":"341-359","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Automated Drawing of Railway Schematics Using Numerical Optimization in SAT"],"prefix":"10.1007","author":[{"given":"Bj\u00f8rnar","family":"Luteberget","sequence":"first","affiliation":[]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Johansen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"19_CR1","unstructured":"IRS 30100: RailTopoModel - railway infrastructure topological model. The International Union of Railways (UIC) (2016)"},{"key":"19_CR2","unstructured":"Avelar, S.: Schematic maps on demand - design, modeling and visualization. Ph.D. thesis, ETH Z\u00fcrich (2002)"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"issue":"4","key":"19_CR4","first-page":"189","volume":"7","author":"M Bj\u00f6rk","year":"2011","unstructured":"Bj\u00f6rk, M.: Successful SAT encoding techniques. JSAT 7(4), 189\u2013201 (2011)","journal-title":"JSAT"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bozzano","year":"2005","unstructured":"Bozzano, M., et al.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 317\u2013333. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31980-1_21"},{"key":"19_CR6","unstructured":"Brands, A.: Automatic generation of schematic diagrams of the Dutch railway network. M.Sc. thesis, Radboud University (2016)"},{"issue":"3","key":"19_CR7","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/j.comgeo.2004.11.002","volume":"30","author":"S Cabello","year":"2005","unstructured":"Cabello, S., de Berg, M., van Kreveld, M.J.: Schematization of networks. Comput. Geom. 30(3), 223\u2013228 (2005)","journal-title":"Comput. Geom."},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0925-7721(94)00014-X","volume":"4","author":"G Battista Di","year":"1994","unstructured":"Di Battista, G., Eades, P., Tamassia, R., Tollis, I.G.: Algorithms for drawing graphs: an annotated bibliography. Comput. Geom. 4, 235\u2013282 (1994)","journal-title":"Comput. Geom."},{"key":"19_CR9","volume-title":"Graph Drawing: Algorithms for the Visualization of Graphs","author":"G Battista Di","year":"1999","unstructured":"Di Battista, G., Eades, P., Tamassia, R., Tollis, I.G.: Graph Drawing: Algorithms for the Visualization of Graphs. Prentice-Hall, Upper Saddle River (1999)"},{"key":"19_CR10","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"19_CR11","unstructured":"H\u00fcrlimann, D.: Objektorientierte Modellierung von Infrastrukturelementen und Betriebsvorg\u00e4ngen im Eisenbahnwesen. Ph.D. thesis, ETH Zurich (2002)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Luteberget, B., Claessen, K., Johansen, C.: Design-time railway capacity verification using SAT modulo discrete event simulation. In: FMCAD. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603003"},{"issue":"6","key":"19_CR13","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"5","key":"19_CR14","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1109\/TVCG.2010.81","volume":"17","author":"M N\u00f6llenburg","year":"2011","unstructured":"N\u00f6llenburg, M., Wolff, A.: Drawing and labeling high-quality metro maps by mixed-integer programming. IEEE Trans. Vis. Comput. Graph. 17(5), 626\u2013641 (2011)","journal-title":"IEEE Trans. Vis. Comput. Graph."},{"key":"19_CR15","unstructured":"N\u00f6llenburg, M.: Automated drawing of metro maps. Technical report 25, Universit\u00e4t Karlsruhe, Karlsruhe (2005)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.cor.2015.02.010","volume":"61","author":"O Oke","year":"2015","unstructured":"Oke, O., Siddiqui, S.: Efficient automated schematic map drawing using multiobjective mixed integer programming. Comput. OR 61, 1\u201317 (2015)","journal-title":"Comput. OR"},{"key":"19_CR17","unstructured":"Ozdal, M.M.: Routing algorithms for high-performance VLSI packaging. Ph.D. thesis (2005)"},{"issue":"1\u20132","key":"19_CR18","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0925-7721(97)00017-5","volume":"9","author":"A Papakostas","year":"1998","unstructured":"Papakostas, A., Tollis, I.G.: Algorithms for area-efficient orthogonal drawings. Comput. Geom. 9(1\u20132), 83\u2013110 (1998)","journal-title":"Comput. Geom."},{"key":"19_CR19","unstructured":"Bane NOR: Model of the Norwegian rail network (2016). \nhttp:\/\/www.banenor.no\/en\/startpage1\/Market1\/Model-of-the-national-rail-network\/"},{"key":"19_CR20","unstructured":"Seyedi-Shandiz, S.: Schematic representation of the geographical railway network used by the Swedish transport administration. M.Sc. thesis, Lund University (2014)"},{"issue":"3","key":"19_CR21","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1137\/0216030","volume":"16","author":"R Tamassia","year":"1987","unstructured":"Tamassia, R.: On embedding a graph in the grid with the minimum number of bends. SIAM J. Comput. 16(3), 421\u2013444 (1987)","journal-title":"SIAM J. Comput."},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-73915-1_29","volume-title":"Graph Drawing and Network Visualization","author":"TC Dijk van","year":"2018","unstructured":"van Dijk, T.C., Lipp, F., Markfelder, P., Wolff, A.: Computing storyline visualizations with few block crossings. In: Frati, F., Ma, K.-L. (eds.) GD 2017. LNCS, vol. 10692, pp. 365\u2013378. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73915-1_29"},{"issue":"1","key":"19_CR23","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s00450-007-0036-y","volume":"22","author":"A Wolff","year":"2007","unstructured":"Wolff, A.: Drawing subway maps: a survey. Inf. Forsc. Entwick. 22(1), 23\u201344 (2007)","journal-title":"Inf. Forsc. Entwick."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,22]],"date-time":"2019-11-22T00:18:47Z","timestamp":1574381927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}