{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T14:06:22Z","timestamp":1762956382822,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100010198","name":"Ministerio de Econom\u00eda, Industria y Competitividad, Gobierno de Espa\u00f1a","doi-asserted-by":"crossref","award":["TIN2017-86727-C2-1-R"],"award-info":[{"award-number":["TIN2017-86727-C2-1-R"]}],"id":[{"id":"10.13039\/501100010198","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1007\/s00607-020-00831-8","type":"journal-article","created":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T10:03:43Z","timestamp":1594202623000},"page":"29-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Optimized SAT encoding of conformance checking artefacts"],"prefix":"10.1007","volume":"103","author":[{"given":"Mathilde","family":"Boltenhagen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Chatain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9656-254X","authenticated-orcid":false,"given":"Josep","family":"Carmona","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"831_CR1","unstructured":"Adriansyah A (2014) Aligning observed and modeled behavior. PhD thesis, Department of Mathematics and Computer Science"},{"issue":"2","key":"831_CR2","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10115-018-1214-x","volume":"59","author":"A Augusto","year":"2019","unstructured":"Augusto A, Conforti R, Dumas M, La Rosa M, Polyvyanyy A (2019) Split miner: automated discovery of accurate and simple business process models from event logs. Knowl Inf Syst 59(2):251\u2013284","journal-title":"Knowl Inf Syst"},{"key":"831_CR3","unstructured":"Arturs B, Piotr I (2015) Edit distance cannot be computed in strongly subquadratic time (unless seth is false). In: Proceedings of the 47th annual ACM symposium on theory of computing. ACM, pp 51\u201358"},{"key":"831_CR4","doi-asserted-by":"crossref","unstructured":"Bauer M, van\u00a0der Aa H, Weidlich M (2019) Estimating process conformance by trace sampling and result approximation. In: Business process management- 17th international conference, BPM 2019, Vienna, Austria, 1\u20136 Sept 2019, Proceedings, pp 179\u2013197","DOI":"10.1007\/978-3-030-26619-6_13"},{"key":"831_CR5","unstructured":"Berti A, van Zelst Sebastiaan J, van\u00a0der Aalst W (2019) Process mining for python (PM4Py): bridging the gap between process-and data science, pp 13\u201316"},{"key":"831_CR6","doi-asserted-by":"crossref","unstructured":"Bloemen V, van\u00a0de Pol Jaco MP, van\u00a0der Aalst W (2018) Symbolically aligning observed and modelled behaviour. In: 18th international conference on application of concurrency to system design, ACSD, Bratislava, Slovakia, 25\u201329 June, pp 50\u201359","DOI":"10.1109\/ACSD.2018.00008"},{"key":"831_CR7","doi-asserted-by":"crossref","unstructured":"Boltenhagen M, Chatain T, Carmona J (2019) Encoding conformance checking artefacts in SAT. In: Business process management workshops. Springer","DOI":"10.1007\/978-3-030-37453-2_14"},{"key":"831_CR8","doi-asserted-by":"crossref","unstructured":"Boltenhagen M, Chatain T, Carmona J (2019) Generalized alignment-based trace clustering of process behavior. In: Proceedings of the 40th international conference on applications and theory of petri nets (ICATPN\u201919), number 11522 in Lecture Notes in Computer Science. Springer","DOI":"10.1007\/978-3-030-21571-2_14"},{"key":"831_CR9","unstructured":"Buijs JCAM (2013) Loan application example. 4TU. Centre for Research Data. Dataset. doi.org\/10.4121"},{"key":"831_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99414-7","volume-title":"Conformance checking\u2014relating processes and models","author":"J Carmona","year":"2018","unstructured":"Carmona J, van Dongen BF, Solti A, Weidlich M (2018) Conformance checking\u2014relating processes and models. Springer, Berlin"},{"key":"831_CR11","unstructured":"Chatain T, Boltenhagen M, Carmona J (2019) Anti-alignments\u2014measuring the precision of process models and event logs. Report hal-02383546: https:\/\/hal.inria.fr\/hal-02383546"},{"key":"831_CR12","doi-asserted-by":"crossref","unstructured":"Chatain T, Carmona J (2016) Anti-alignments in conformance checking\u2014the dark side of process models. In: International conference on application and theory of petri nets and concurrency. Springer, pp 240\u2013258","DOI":"10.1007\/978-3-319-39086-4_15"},{"key":"831_CR13","doi-asserted-by":"crossref","unstructured":"Chatain T, Carmona J, Van\u00a0Dongen B (2017) Alignment-based trace clustering. In: International conference on conceptual modeling. Springer, pp 295\u2013308","DOI":"10.1007\/978-3-319-69904-2_24"},{"key":"831_CR14","doi-asserted-by":"crossref","unstructured":"Davidson I, Ravi SS, Shamis L (2010) A sat-based framework for efficient constrained clustering. In: Proceedings of the 2010 SIAM international conference on data mining, pp 94\u2013105. SIAM","DOI":"10.1137\/1.9781611972801.9"},{"key":"831_CR15","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.eswa.2017.03.047","volume":"82","author":"M de Leoni","year":"2017","unstructured":"de Leoni M, Marrella A (2017) Aligning real process executions and prescriptive process models through automated planning. Expert Syst Appl 82:162\u2013183","journal-title":"Expert Syst Appl"},{"issue":"3","key":"831_CR16","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1109\/TSE.2017.2668418","volume":"44","author":"L Garc\u00eda-Ba\u00f1uelos","year":"2018","unstructured":"Garc\u00eda-Ba\u00f1uelos L, van Beest NRTP, Dumas M, La Rosa M, Mertens W (2018) Complete and interpretable conformance checking of business processes. IEEE Trans Softw Eng 44(3):262\u2013290","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"831_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-005-0202-0","volume":"8","author":"A Groce","year":"2006","unstructured":"Groce A, Chaki S, Kroening D, Strichman O (2006) Error explanation with distance metrics. Int J Softw Tools Technol Transf 8(3):229\u2013247","journal-title":"Int J Softw Tools Technol Transf"},{"key":"831_CR18","doi-asserted-by":"crossref","unstructured":"Ignatiev A, Morgado A, Marques-Silva J (2018) PySAT: a Python toolkit for prototyping with SAT oracles. In: SAT, pp 428\u2013437","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"831_CR19","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.ins.2018.07.026","volume":"466","author":"WLJ Lee","year":"2018","unstructured":"Lee WLJ, Verbeek HMW, Munoz-Gama J, van\u00a0der Aalst WMP, Sep\u00falveda M (2018) Recomposing conformance: closing the circle on decomposed alignment-based conformance checking in process mining. Inf Sci 466:55\u201391","journal-title":"Inf Sci"},{"issue":"2","key":"831_CR20","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/s10270-016-0545-x","volume":"17","author":"SJJ Leemans","year":"2018","unstructured":"Leemans SJJ, Fahland D, van\u00a0der Aalst WMP (2018) Scalable process discovery and conformance checking. Softw Syst Model 17(2):599\u2013631","journal-title":"Softw Syst Model"},{"key":"831_CR21","doi-asserted-by":"crossref","unstructured":"Leemans Sander\u00a0JJ, Fahland D, van\u00a0der Aalst WMP (2013) Discovering block-structured process models from event logs containing infrequent behaviour. In: International conference on business process management. Springer, pp 66\u201378","DOI":"10.1007\/978-3-319-06257-0_6"},{"key":"831_CR22","doi-asserted-by":"crossref","unstructured":"M\u00e9tivier J-P, Boizumault P, Cr\u00e9milleux B, Khiari M, Loudni S (2012) Constrained clustering using sat. In: International symposium on intelligent data analysis. Springer, pp 207\u2013218","DOI":"10.1007\/978-3-642-34156-4_20"},{"key":"831_CR23","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.is.2014.04.003","volume":"46","author":"J Munoz-Gama","year":"2014","unstructured":"Munoz-Gama J, Carmona J, Van Der Aalst WMP (2014) Single-entry single-exit decomposed conformance checking. Inf Syst 46:102\u2013122","journal-title":"Inf Syst"},{"issue":"4","key":"831_CR24","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541\u2013574","journal-title":"Proc IEEE"},{"key":"831_CR25","doi-asserted-by":"crossref","unstructured":"Rei\u00dfner D, Conforti R, Dumas M, La Rosa M, Armas-Cervantes A (2017) Scalable conformance checking of business processes. In: OTM CoopIS, Rhodes, Greece, pp 607\u2013627","DOI":"10.1007\/978-3-319-69462-7_38"},{"key":"831_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ipl.2018.01.013","volume":"135","author":"N Tax","year":"2018","unstructured":"Tax N, Xixi L, Sidorova N, Fahland D, van\u00a0der Aalst WMP (2018) The imprecisions of precision measures in process mining. Inf Process Lett 135:1\u20138","journal-title":"Inf Process Lett"},{"key":"831_CR27","unstructured":"Taymouri F, Carmona J (2016) Model and event log reductions to boost the computation of alignments. In: Proceedings of the 6th international symposium on data-driven process discovery and analysis (SIMPDA 2016), Graz, Austria, 15\u201316 Dec 2016, pp 50\u201362"},{"key":"831_CR28","doi-asserted-by":"crossref","unstructured":"Taymouri F, Carmona J (2016) A recursive paradigm for aligning observed behavior of large structured process models. In: 14th international conference of business process management (BPM), Rio de Janeiro, Brazil, Sept 18\u201322","DOI":"10.1007\/978-3-319-45348-4_12"},{"issue":"4","key":"831_CR29","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/s10619-013-7127-5","volume":"31","author":"WMP van\u00a0der Aalst","year":"2013","unstructured":"van\u00a0der Aalst WMP (2013) Decomposing petri nets for process mining: a generic approach. Distrib Parallel Databases 31(4):471\u2013507","journal-title":"Distrib Parallel Databases"},{"key":"831_CR30","doi-asserted-by":"crossref","unstructured":"van Dongen BF (2018) Efficiently computing alignments\u2014using the extended marking equation. In: Business process management\u201416th international conference, BPM 2018, Sydney, NSW, Australia, 9\u201314 Sept 2018, Proceedings, pp 197\u2013214","DOI":"10.1007\/978-3-319-98648-7_12"},{"key":"831_CR31","doi-asserted-by":"crossref","unstructured":"van Dongen BF, Carmona J, Chatain T (2016) A unified approach for measuring precision and generalization based on anti-alignments. In: Business process management\u201414th international conference, BPM 2016, Rio de Janeiro, Brazil, 18\u201322 Sept 2016. Proceedings, pp 39\u201356","DOI":"10.1007\/978-3-319-45348-4_3"},{"key":"831_CR32","doi-asserted-by":"crossref","unstructured":"van Dongen BF, Carmona J, Chatain T, Taymouri F (2017) Aligning modeled and observed behavior: a compromise between computation complexity and quality. In: Advanced information systems engineering\u201429th international conference, CAiSE 2017, Essen, Germany, 12\u201316 June 2017, Proceedings, pp 94\u2013109","DOI":"10.1007\/978-3-319-59536-8_7"},{"key":"831_CR33","first-page":"219","volume-title":"Merging alignments for decomposed replay","author":"HMW Verbeek","year":"2016","unstructured":"Verbeek HMW, van\u00a0der Aalst WMP (2016) Merging alignments for decomposed replay. Springer, Cham, pp 219\u2013239"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-020-00831-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00607-020-00831-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-020-00831-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T23:21:55Z","timestamp":1625700115000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00607-020-00831-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["831"],"URL":"https:\/\/doi.org\/10.1007\/s00607-020-00831-8","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"type":"print","value":"0010-485X"},{"type":"electronic","value":"1436-5057"}],"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"1 December 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}