{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T18:25:59Z","timestamp":1760898359003,"version":"3.41.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,6,6]],"date-time":"2016-06-06T00:00:00Z","timestamp":1465171200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10270-016-0536-y","type":"journal-article","created":{"date-parts":[[2016,6,6]],"date-time":"2016-06-06T12:05:54Z","timestamp":1465214754000},"page":"1055-1078","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Encoding process discovery problems in SMT"],"prefix":"10.1007","volume":"17","author":[{"given":"Marc","family":"Sol\u00e9","sequence":"first","affiliation":[]},{"given":"Josep","family":"Carmona","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,6]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., Adriansyah, A., de Medeiros, A.K.A., Arcieri, F., Baier, T., Blickle, T., Bose, R.P.J.C., van den Brand, P., Brandtjen, R., Buijs, J., Burattin, A., Carmona, J., Castellanos, M., Claes, J., Cook, J., Costantini, N., Curbera, F., Damiani, E., de Leoni, M., Delias, P., van Dongen, B.F., Dumas, M., Dustdar, S., Fahland, D., Ferreira, D.R., Gaaloul, W., van Geffen, F., Goel, S., G\u00fcnther, C., Guzzo, A., Harmon, P., ter Hofstede, A., Hoogland, J., Ingvaldsen, J.E., Kato, K., Kuhn, R., Kumar, A., La Rosa, M., Maggi, F., Malerba, D., Mans, R.S., Manuel, A., McCreesh, M., Mello, P., Mendling, J., Montali, M., Motahari-Nezhad, H.R., zur Muehlen, M., Munoz-Gama, J., Pontieri, L., Ribeiro, J., Rozinat, A., P\u00e9rez, H.S., P\u00e9rez, R.S., Sep\u00falveda, M., Sinur, J., Soffer, P., Song, M., Sperduti, A., Stilo, G., Stoel, C., Swenson, K., Talamo, M., Tan, W., Turner, C., Vanthienen, J., Varvaressos, G., Verbeek, E., Verdonk, M., Vigo, R., Wang, J., Weber, B., Weidlich, M., Weijters, T., Wen, L., Westergaard, M., Wynn, M.: IEEE task force on process mining: process mining manifesto. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) Business Process Management Workshops (1), Lecture Notes in Business Information Processing, vol.\u00a099, pp. 169\u2013194. Springer, New York (2011)","key":"536_CR1","DOI":"10.1007\/978-3-642-28108-2_19"},{"key":"536_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19345-3","volume-title":"Process Mining\u2014Discovery, Conformance and Enhancement of Business Processes","author":"WMP Aalst van der","year":"2011","unstructured":"van der Aalst, W.M.P.: Process Mining\u2014Discovery, Conformance and Enhancement of Business Processes. Springer, New York (2011)"},{"doi-asserted-by":"crossref","unstructured":"Murata, T.: Petri Nets: properties, analysis and applications. In: Proceedings of the IEEE, pp. 541\u2013580 (1989)","key":"536_CR3","DOI":"10.1109\/5.24143"},{"issue":"6","key":"536_CR4","doi-asserted-by":"crossref","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"},{"key":"536_CR5","first-page":"702","volume-title":"CAV, Lecture Notes in Computer Science","author":"S Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: VS3: SMT solvers for program verification. In: Bouajjani, A., Maler, O. (eds.) CAV, Lecture Notes in Computer Science, vol. 5643, pp. 702\u2013708. Springer, New York (2009)"},{"issue":"4","key":"536_CR6","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/MS.2006.117","volume":"23","author":"N Tillmann","year":"2006","unstructured":"Tillmann, N., Schulte, W.: Unit tests reloaded: parameterized unit testing with symbolic execution. IEEE Softw. 23(4), 38\u201347 (2006)","journal-title":"IEEE Softw."},{"key":"536_CR7","first-page":"337","volume-title":"TACAS, Lecture Notes in Computer Science","author":"LM Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, New York (2008)"},{"doi-asserted-by":"crossref","unstructured":"Metzner, A., Fr\u00e4nzle, M., Herde, C., Stierand, I.: Scheduling distributed real-time systems by satisfiability checking. In: Ng, J.K., Sha, L., Lee, V.C.S., Takashio, K., Ryu, M., Ni, L. (eds.) RTCSA, pp. 409\u2013415. IEEE Computer Society, Los Alamitos (2005)","key":"536_CR8","DOI":"10.1109\/RTCSA.2005.90"},{"key":"536_CR9","first-page":"310","volume-title":"IJCAI","author":"SA Wolfman","year":"1999","unstructured":"Wolfman, S.A., Weld, D.S.: The LPSAT engine & its application to resource planning. In: Dean, T. (ed.) IJCAI, pp. 310\u2013317. Morgan Kaufmann, Los Altos (1999)"},{"issue":"9","key":"536_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"LM Moura de","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., Adriansyah, A., van Dongen, B.: Causal nets: a modeling language tailored towards process discovery. In: Katoen, J-.P., K\u00f6nig, B. (eds.) CONCUR 2011 \u2013 Concurrency Theory, Lecture Notes in Computer Science, vol. 6901, pp. 28\u201342. Springer, Berlin Heidelberg (2011) CONCUR, pp. 28\u201342 (2011)","key":"536_CR11","DOI":"10.1007\/978-3-642-23217-6_3"},{"doi-asserted-by":"crossref","unstructured":"Sol\u00e9, M., Carmona, J.: An SMT-based discovery algorithm for C-nets. In: Petri Nets, LNCS, vol. 7347, pp. 51\u201371 (2012)","key":"536_CR12","DOI":"10.1007\/978-3-642-31131-4_4"},{"doi-asserted-by":"publisher","unstructured":"Sol\u00e9, M., Carmona, J.: Amending C-net discovery algorithms. In: S.Y. Shin, J.C. Maldonado (eds.) Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC \u201913, Coimbra, Portugal, March 18\u201322, 2013, pp. 1418\u20131425. ACM (2013). doi: 10.1145\/2480362.2480628 . http:\/\/doi.acm.org\/10.1145\/2480362.2480628","key":"536_CR13","DOI":"10.1145\/2480362.2480628"},{"key":"536_CR14","first-page":"165","volume-title":"Business Process Management Workshops (1), Lecture Notes in Business Information Processing","author":"RPJC Bose","year":"2011","unstructured":"Bose, R.P.J.C., van der Aalst, W.M.P.: Analysis of patient treatment procedures. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) Business Process Management Workshops (1), Lecture Notes in Business Information Processing, vol. 99, pp. 165\u2013166. Springer, New York (2011)"},{"key":"536_CR15","first-page":"425","volume-title":"BIOSTEC (Selected Papers), Communications in Computer and Information Science","author":"Mans R.S","year":"2008","unstructured":"R.S, Mans, Schonenberg, H., Song, M., van der Aalst, W.M.P., Bakker, P.J.M.: Application of process mining in healthcare\u2014a case study in a Dutch hospital. In: Fred, A.L.N., Filipe, J., Gamboa, H. (eds.) BIOSTEC (Selected Papers), Communications in Computer and Information Science, vol. 25, pp. 425\u2013438. Springer, New York (2008)"},{"issue":"3","key":"536_CR16","first-page":"45","volume":"31","author":"WMP Aalst van der","year":"2008","unstructured":"van der Aalst, W.M.P., Verbeek, H.M.W.E.: Process mining in web services: the websphere case. IEEE Data Eng. Bull. 31(3), 45\u201348 (2008)","journal-title":"IEEE Data Eng. Bull."},{"issue":"4","key":"536_CR17","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1109\/TSMCC.2009.2014169","volume":"39","author":"A Rozinat","year":"2009","unstructured":"Rozinat, A., de Jong, I.S.M., G\u00fcnther, C.W., van der Aalst, W.M.P.: Process mining applied to the test process of wafer scanners in ASML. IEEE Trans. Syst. Man Cybern. Part C 39(4), 474\u2013479 (2009)","journal-title":"IEEE Trans. Syst. Man Cybern. Part C"},{"issue":"3","key":"536_CR18","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/MC.2010.61","volume":"43","author":"WMP Aalst van der","year":"2010","unstructured":"van der Aalst, W.M.P., van Hee, K.M., van der Werf, J.M.E.M., Verdonk, M.: Auditing 2.0: using process mining to support tomorrow\u2019s auditor. IEEE Comput. 43(3), 90\u201393 (2010)","journal-title":"IEEE Comput."},{"doi-asserted-by":"publisher","unstructured":"Buijs, J.C.A.M., van Dongen, B.F., van der Aalst, W.M.P.: Quality dimensions in process discovery: the importance of fitness, precision, generalization and simplicity. Int. J. Coop. Inf. Syst. 23(1) (2014). doi: 10.1142\/S0218843014400012","key":"536_CR19","DOI":"10.1142\/S0218843014400012"},{"doi-asserted-by":"crossref","unstructured":"Jha, S., Limaye, R., Seshia, S.: Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, pp. 668\u2013674. Springer, New York (2009)","key":"536_CR20","DOI":"10.1007\/978-3-642-02658-4_53"},{"issue":"9","key":"536_CR21","first-page":"1128","volume":"16","author":"WMP Aalst van der","year":"2004","unstructured":"van der Aalst, W.M.P., Weijters, T., Maruster, L.: Workflow mining: discovering process models from event logs. IEEE TKDE 16(9), 1128\u20131142 (2004)","journal-title":"IEEE TKDE"},{"key":"536_CR22","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF00264611","volume":"27","author":"A Ehrenfeucht","year":"1990","unstructured":"Ehrenfeucht, A., Rozenberg, G.: Partial (Set) 2-structures. Part I, II. Acta Inf. 27, 315\u2013368 (1990)","journal-title":"Acta Inf."},{"doi-asserted-by":"crossref","unstructured":"Badouel, E., Darondeau, P.: Theory of regions. In: Reisig, W., Rozenberg, G. (eds.) Petri Nets, LNCS 1491, pp. 529\u2013586. Springer, New York (1998)","key":"536_CR23","DOI":"10.1007\/3-540-65306-6_22"},{"issue":"3","key":"536_CR24","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1109\/TC.2009.131","volume":"59","author":"J Carmona","year":"2010","unstructured":"Carmona, J., Cortadella, J., Kishinevsky, M.: New region-based algorithms for deriving bounded Petri nets. IEEE Trans. Comput. 59(3), 371\u2013384 (2010)","journal-title":"IEEE Trans. Comput."},{"issue":"1","key":"536_CR25","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/s10270-008-0106-z","volume":"9","author":"WMP Aalst van der","year":"2009","unstructured":"van der Aalst, W.M.P., Rubin, V., Verbeek, H.M.W., van Dongen, B., Kindler, E., G\u00fcnther, C.: Process mining: a two-step approach to balance between underfitting and overfitting. Softw. Syst. Model. 9(1), 87\u2013111 (2009)","journal-title":"Softw. Syst. Model."},{"doi-asserted-by":"crossref","unstructured":"Sol\u00e9, M., Carmona, J.: Process mining from a basis of state regions. In: Lilius, J., Penczek, W. (eds.) Petri Nets, LNCS 6128, pp. 226\u2013245. Springer, New York (2010)","key":"536_CR26","DOI":"10.1007\/978-3-642-13675-7_14"},{"issue":"1","key":"536_CR27","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TKDE.2011.192","volume":"25","author":"M Sol\u00e9","year":"2013","unstructured":"Sol\u00e9, M., Carmona, J.: Region-based foldings in process discovery. IEEE Trans. Knowl. Data Eng. 25(1), 192\u2013205 (2013). doi: 10.1109\/TKDE.2011.192","journal-title":"IEEE Trans. Knowl. Data Eng."},{"doi-asserted-by":"crossref","unstructured":"Bernardinello, L.: Synthesis of net systems. In: Marsan, M.A. (ed.) Application and Theory of Petri Nets, LNCS, vol. 691, pp. 89\u2013105. Springer, New York (1993)","key":"536_CR28","DOI":"10.1007\/3-540-56863-8_42"},{"doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, pp. 524\u2013536. Springer, New York (2007)","key":"536_CR29","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"536_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-540-72200-7_23","volume-title":"LPNMR, Lecture Notes in Computer Science","author":"M Gebser","year":"2007","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J.S. (eds.) LPNMR, Lecture Notes in Computer Science. Lecture Notes in Computer Science, vol. 4483, pp. 260\u2013265. Springer, New York (2007)"},{"doi-asserted-by":"crossref","unstructured":"van\u00a0der Werf, J.M.E.M., van Dongen, B.F., Hurkens, C.A.J., Serebrenik, A.: Process discovery using integer linear programming. In: van Hee, K.M., Valk, R. (eds.) ATPN, pp. 368\u2013387. Springer, New York (2008)","key":"536_CR31","DOI":"10.1007\/978-3-540-68746-7_24"},{"doi-asserted-by":"crossref","unstructured":"Munoz-Gama, J., Carmona, J.: A Fresh look at precision in process conformance. In: Hull, R., Mendling, J., Tai, S. (eds.) Business Process Management (BPM). Springer, New York. (2010)","key":"536_CR32","DOI":"10.1007\/978-3-642-15618-2_16"},{"doi-asserted-by":"crossref","unstructured":"Weijters, A.J.M.M., Ribeiro, J.T.S.: Flexible heuristics miner (FHM). In: Chawla, N., King,I., Sperduti, A. (eds.) CIDM, pp. 310\u2013317. IEEE, Los Alamitos (2011)","key":"536_CR33","DOI":"10.1109\/CIDM.2011.5949453"},{"doi-asserted-by":"crossref","unstructured":"Guo, Q., Wen, L., Wang, J., Yan, Z., Yu, P.S.: Mining invisible tasks in non-free-choice constructs. In: Proceedings of Business Process Management\u201413th International Conference, BPM 2015, Innsbruck, Austria, August 31\u2013September 3, 2015, pp. 109\u2013125 (2015)","key":"536_CR34","DOI":"10.1007\/978-3-319-23063-4_7"},{"doi-asserted-by":"crossref","unstructured":"de\u00a0Medeiros, A.K.A., van\u00a0der Aalst, W.M.P., Weijters, A.J.M.M.: Workflow mining: current status and future directions. In: Meersman, R., Tari, Z., Schmidt, D.C. (eds.) CoopIS\/DOA\/ODBASE, pp. 389\u2013406. Springer, New York (2003)","key":"536_CR35","DOI":"10.1007\/978-3-540-39964-3_25"},{"issue":"2","key":"536_CR36","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/s10618-007-0065-y","volume":"15","author":"L Wen","year":"2007","unstructured":"Wen, L., van der Aalst, W.M.P., Wang, J., Sun, J.: Mining process models with non-free-choice constructs. Data Min. Knowl. Discov. 15(2), 145\u2013180 (2007)","journal-title":"Data Min. Knowl. Discov."},{"key":"536_CR37","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-3-642-00899-3_13","volume":"2","author":"BF Dongen van","year":"2009","unstructured":"van Dongen, B.F., de Medeiros, A.K.A., Wen, L.: Process mining: overview and outlook of petri net discovery algorithms. Trans. Petri Nets Other Models of Concurr. 2, 225\u2013242 (2009)","journal-title":"Trans. Petri Nets Other Models of Concurr."},{"unstructured":"Leemans, S.J.J., Fahland, D., van\u00a0der Aalst, W.M.P.: Discovering block-structured process models from event logs\u2014a constructive approach. In: Application and Theory of Petri Nets and Concurrency - 34th International Conference, PETRI NETS 2013, Milan, Italy, June 24\u201328, 2013. Proceedings, pp. 311\u2013329 (2013)","key":"536_CR38"},{"doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., de Medeiros, A.K.A., Weijters, A.J.M.M.: Genetic process mining. In: Ciardo, G., Darondeau, P. (eds.) CATPN, LNCS, vol. 3536, pp. 48\u201369. Springer, New York (2005)","key":"536_CR39","DOI":"10.1007\/11494744_5"},{"doi-asserted-by":"publisher","unstructured":"Buijs, J.C.A.M., van Dongen, B.F., van\u00a0der Aalst, W.M.P.: A genetic algorithm for discovering process trees. In: Proceedings of the IEEE Congress on Evolutionary Computation, CEC 2012, Brisbane, Australia, June 10\u201315, 2012, pp. 1\u20138 (2012). doi: 10.1109\/CEC.2012.6256458","key":"536_CR40","DOI":"10.1109\/CEC.2012.6256458"},{"doi-asserted-by":"crossref","unstructured":"Bergenthum, R., Desel, J., Lorenz, R., S.Mauser: Process mining based on regions of languages. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) Business Process Management, pp. 375\u2013383. Springer, New York (2007)","key":"536_CR41","DOI":"10.1007\/978-3-540-75183-0_27"},{"issue":"3\u20134","key":"536_CR42","doi-asserted-by":"crossref","first-page":"343","DOI":"10.3233\/FI-2011-612","volume":"113","author":"M Sol\u00e9","year":"2011","unstructured":"Sol\u00e9, M., Carmona, J.: Light region-based techniques for process discovery. Fundam. Inform. 113(3\u20134), 343\u2013376 (2011)","journal-title":"Fundam. Inform."},{"key":"536_CR43","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/s10732-006-7234-9","volume":"12","author":"J Argelich","year":"2006","unstructured":"Argelich, J., Many\u00e0, F.: Exact max-sat solvers for over-constrained problems. J. Heuristics 12, 375\u2013392 (2006)","journal-title":"J. Heuristics"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-016-0536-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0536-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0536-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0536-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T20:46:42Z","timestamp":1748983602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-016-0536-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,6]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["536"],"URL":"https:\/\/doi.org\/10.1007\/s10270-016-0536-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2016,6,6]]}}}